Clarifying and compiling C/C++ concurrency
Clarifying and compiling C/C++ concurrency
复制标题
澄清和编译C/C并发
DOI：
10.1145/2103656.2103717
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Batty M
中科院分区：
文献类型：
--
作者：
Batty M
即将到来的C和C++修订标准第一次以微妙的 * 放松内存模型 *（*C++11模型 *）的形式为语言增加了并发性。这旨在允许编译器优化并适应主流多处理器的不同松弛内存行为，将大多数代码的简单语义与并发库的高性能 * 低级原子 * 相结合。在本文中，我们首先建立了两个简单但可证明等价的C++11模型，一个是完整的语言，另一个是没有消费操作的子集。进一步子集化没有低级原子的片段，我们发现了原子初始化产生的微妙之处，并证明在附加条件下，该模型等效于无竞争程序的顺序一致性。然后，我们证明了我们的主要结果，即针对C++11加载和存储并发原语到Power汇编的两个拟议编译方案的正确性，并指出早期的提案有缺陷。(The主要思想也适用于ARM，它有一个类似的宽松的存储器架构。这将为C++11和C1x的生产编译器的持续开发提供信息，阐明机器架构需要哪些属性，并建立对C++11和Power语义的信心。
The upcoming C and C++ revised standards add concurrency to the languages, for the first time, in the form of a subtle *relaxed memory model* (the *C++11 model*). This aims to permit compiler optimisation and to accommodate the differing relaxed-memory behaviours of mainstream multiprocessors, combining simple semantics for most code with high-performance *low-level atomics* for concurrency libraries. In this paper, we first establish two simpler but provably equivalent models for C++11, one for the full language and another for the subset without consume operations. Subsetting further to the fragment without low-level atomics, we identify a subtlety arising from atomic initialisation and prove that, under an additional condition, the model is equivalent to sequential consistency for race-free programs.We then prove our main result, the correctness of two proposed compilation schemes for the C++11 load and store concurrency primitives to Power assembly, having noted that an earlier proposal was flawed. (The main ideas apply also to ARM, which has a similar relaxed memory architecture.)This should inform the ongoing development of production compilers for C++11 and C1x, clarifies what properties of the machine architecture are required, and builds confidence in the C++11 and Power semantics.