An operational semantics for C/C++11 concurrency
An operational semantics for C/C++11 concurrency
复制标题
C/C 11 并发的操作语义
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Peter Sewell
中科院分区：
文献类型：
--
作者：
Kyndylan Nienhuis;Kayvan Memarian;Peter Sewell
C/C++11并发模型平衡了两个目标：它足够宽松，可以有效地实现，并且（撇开“稀薄空气”问题不谈）它足够强大，可以为程序员提供有用的保证。它在数学上很精确，已用于验证研究和编译器测试。然而，该模型是以公理化的风格表示的，作为对完整候选执行的谓词。这足以计算一个小的石蕊测试允许执行的集合，但它不直接支持更大程序执行的增量构造。它也与传统的操作语义不一致，在C/C++标准的其余部分中隐式使用。我们的主要贡献是开发了一个C/C++11并发操作模型。这涵盖了以前的形式化公理模型的所有功能，我们有一个机械化的证明，这两个是等价的，在伊莎贝尔/HOL。我们还将此语义与顺序C的操作语义（在其他地方描述）集成在一起;组合语义可以在一小段C中增量执行程序。这样做揭示了C/C++11模型的几个新方面：我们表明，不能建立一个等效的操作模型，简单地遵循程序顺序，顺序一致的顺序，或同步顺序。第一个负面结果是由硬件可观察行为造成的，但后两个不是，因此可以通过更改C/C++11来改善。更一般地说，我们希望这项工作，其重点是执行的增量建设，将通知未来的设计新的并发模型。
The C/C++11 concurrency model balances two goals: it is relaxed enough to be efficiently implementable and (leaving aside the ``thin-air'' problem) it is strong enough to give useful guarantees to programmers. It is mathematically precise and has been used in verification research and compiler testing. However, the model is expressed in an axiomatic style, as predicates on complete candidate executions. This suffices for computing the set of allowed executions of a small litmus test, but it does not directly support the incremental construction of executions of larger programs. It is also at odds with conventional operational semantics, as used implicitly in the rest of the C/C++ standards. Our main contribution is the development of an operational model for C/C++11 concurrency. This covers all the features of the previous formalised axiomatic model, and we have a mechanised proof that the two are equivalent, in Isabelle/HOL. We also integrate this semantics with an operational semantics for sequential C (described elsewhere); the combined semantics can incrementally execute programs in a small fragment of C. Doing this uncovered several new aspects of the C/C++11 model: we show that one cannot build an equivalent operational model that simply follows program order, sequential consistent order, or the synchronises-with order. The first negative result is forced by hardware-observable behaviour, but the latter two are not, and so might be ameliorated by changing C/C++11. More generally, we hope that this work, with its focus on incremental construction of executions, will inform the future design of new concurrency models.
吹毛求疵的c并发
DOI：
10.1145/2003476.2003493
发表时间：
2011
期刊：
--
影响因子：
--
作者：
Blanchette J
通讯作者：
Blanchette J
C/C 并发的库抽象
DOI：
10.1145/2429069.2429099
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M