C/C++ 到 POWER 与 ARMv7 尾同步编译器映射的反例与证明漏洞
编程语言
2016-11-18 v2
摘要
C 和 C++ 高级语言为程序员提供原子操作以编写高性能并发代码。在汇编语言层面，C 和 C++ 原子操作由编译器映射为单条指令或指令组合，具体取决于底层架构提供的顺序保证与同步指令。这些编译器映射必须维护 C/C++ 原子操作所提供的顺序保证，否则编译后的程序将不按 C/C++ 内存模型行为。本文讨论了针对 Power 与 ARMv7 架构的著名尾同步(trailing-sync)编译器映射的两个反例，这些映射先前被认为已被证明正确。除反例外，我们还讨论了这些映射证明中的漏洞，该漏洞使得错误映射被证明为正确。我们还讨论了与这一缺陷相关的编译器和架构的现状。
引用
@article{arxiv.1611.01507,
title = {Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings},
author = {Yatin A. Manerkar and Caroline Trippel and Daniel Lustig and Michael Pellauer and Margaret Martonosi},
journal= {arXiv preprint arXiv:1611.01507},
year = {2016}
}