Towards understanding the costs of avoiding out-of-thin-air results
Towards understanding the costs of avoiding out-of-thin-air results
复制标题
了解避免无中生有的结果的成本
DOI：
10.1145/3276506
复制
发表时间：
2018
影响因子：
--
通讯作者：
Demsky, Brian
中科院分区：
文献类型：
--
作者：
Ou, Peizhao;Demsky, Brian
消除所谓的“凭空”（out-of-thin-air，OOTA）结果是许多现有编程语言内存模型（包括Java、C和C++）的一个公开问题。OOTA行为是有问题的，因为它们破坏了关于程序行为的正式和非正式的模块化推理。定义易于理解的内存模型语义，允许现有的优化，并禁止OOTA结果仍然是一个悬而未决的问题。本文探讨了两个简单的解决方案，这个问题，禁止OOTA的结果。一种解决方案针对C/C++类内存模型，其中竞争操作被明确标记为原子操作，第二种解决方案针对Java类语言，其中所有内存操作都可以创建OOTA执行。我们的解决方案提供了一个每个候选人的执行标准，使它能够检查一个单一的执行，并确定内存模型是否允许执行。我们在LLVM编译器框架中实现并评估了这两种解决方案。我们的研究结果表明，在ARMv 8处理器上，第一种解决方案在43个并发数据结构上平均没有开销，最大开销为6.3%，而第二种解决方案在SPEC CPU 2006 C/C++基准测试中平均开销为3.1%，最大开销为17.6%。
Eliminating so-called “out-of-thin-air” (OOTA) results is an open problem with many existing programming language memory models including Java, C, and C++. OOTA behaviors are problematic in that they break both formal and informal modular reasoning about program behavior. Defining memory model semantics that are easily understood, allow existing optimizations, and forbid OOTA results remains an open problem. This paper explores two simple solutions to this problem that forbid OOTA results. One solution is targeted towards C/C++-like memory models in which racing operations are explicitly labeled as atomic operations and a second solution is targeted towards Java-like languages in which all memory operations may create OOTA executions. Our solutions provide a per-candidate execution criterion that makes it possible to examine a single execution and determine whether the memory model permits the execution. We implemented and evaluated both solutions in the LLVM compiler framework. Our results show that on an ARMv8 processor the first solution has no overhead on average and a maximum overhead of 6.3% on 43 concurrent data structures, and that the second solution has an average overhead of 3.1% and a maximum overhead of 17.6% on the SPEC CPU2006 C/C++ benchmarks.
登录
查看更多内容
DOI：
--
发表时间：
2015
期刊：
European Symposium on Programming
影响因子：
--
作者：
Mark Batty;Kayvan Memarian;Kyndylan Nienhuis;Jean Pichon;Peter Sewell
通讯作者：
Peter Sewell
Java 内存模型中因果关系要求的验证是不可判定的
DOI：
--
发表时间：
2009
期刊：
Parallel Processing and Applied Mathematics
影响因子：
--
作者：
M. Botincan;Paola Glavan;D. Runje
通讯作者：
D. Runje
与事件计数和排序器同步
DOI：
--
发表时间：
1979
期刊：
CACM
影响因子：
--
作者：
D. Reed;R. Kanodia
通讯作者：
R. Kanodia
AutoMO：自动推断 C/C 11 的内存顺序参数
DOI：
--
发表时间：
2015
期刊：
Conference on Object-Oriented Programming Systems, Languages, and Applications
影响因子：
--
作者：
Peizhao Ou;Brian Demsky
通讯作者：
Brian Demsky
影响因子：
1.8
作者：
Kokologiannakis, Michalis;Lahav, Ori;Vafeiadis, Viktor
通讯作者：
Vafeiadis, Viktor