Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings
Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings
复制标题
C/C 到 POWER 和 ARMv7 Trailing-Sync 编译器映射的反例和漏洞证明
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
M. Martonosi
中科院分区：
文献类型：
--
作者：
Yatin A. Manerkar;Caroline Trippel;Daniel Lustig;Michael Pellauer;M. Martonosi
C和C ++高级语言为程序员提供了用于编写高性能并发代码的原子操作。在集会语言级别，C和C ++原子会根据编译器的单个说明或指令的组合，具体取决于基础体系结构提供的订购保证和同步指令。这些编译器映射必须维护C/C ++原子提供的订购保证，或者编译程序不会根据C/C ++内存模型行为。在本文中，我们讨论了两个反示例，以提供众所周知的Tailting-Sync编译器映射，以获取功率和ARMV7架构，这些架构以前被认为是正确的。除了反例外，我们还讨论了映射证据中的漏洞，该映射使错误的映射被证明是正确的。我们还讨论了与该错误有关的编译器和架构的当前状态。
The C and C++ high-level languages provide programmers with atomic operations for writing high-performance concurrent code. At the assembly language level, C and C++ atomics get mapped down to individual instructions or combinations of instructions by compilers, depending on the ordering guarantees and synchronization instructions provided by the underlying architecture. These compiler mappings must uphold the ordering guarantees provided by C/C++ atomics or the compiled program will not behave according to the C/C++ memory model. In this paper we discuss two counterexamples to the well-known trailing-sync compiler mappings for the Power and ARMv7 architectures that were previously thought to be proven correct. In addition to the counterexamples, we discuss the loophole in the proof of the mappings that allowed the incorrect mappings to be proven correct. We also discuss the current state of compilers and architectures in relation to the bug.
彻底修改 C11 和 OpenCL 中的 SC 原子
DOI：
10.1145/2837614.2837637
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M
了解 POWER 多处理器
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S