From Total Store Order to Sequential Consistency: A Practical Reduction Theorem
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem
复制标题
从总存储顺序到顺序一致性：实用的归约定理
DOI：
10.1007/978-3-642-14052-5_28
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Norbert Schirmer
中科院分区：
文献类型：
--
作者：
Ernie Cohen;Norbert Schirmer
在验证并发程序时，通常假设内存是顺序一致的。然而，大多数现代的多处理器缓冲其存储，提供本地顺序一致性，只有在相当大的性能损失。为了重新获得顺序一致性，程序员必须遵循适当的编程原则。然而，现有的朴素的纪律，如保护所有共享访问锁，以避免数据竞争，或根据协议，允许任意数据竞争刷新存储缓冲区，是不够灵活的构建高性能的多处理器软件。我们提出了一个新的纪律下TSO（总存储顺序，存储缓冲区转发）的并发编程。它不使用并发原语（如锁），而是基于在ghost状态下维护所有权信息，允许将纪律表示为状态不变并通过常规程序推理进行验证。如果在没有存储缓冲区的系统中程序的每次执行都遵循该原则，则在具有存储缓冲区的系统中程序的每次执行都是顺序一致的。
When verifying a concurrent program, it is usual to assume sequentially consistent memory. However, most modern multiprocessors buffer their stores, providing native sequential consistency only at a substantial performance penalty. To regain sequential consistency, a programmer has to follow an appropriate programming discipline. However, existing naive disciplines, such as protecting all shared accesses with locks to avoid data races, or flushing store buffers according to a protocol that allows arbitrary data races, are not flexible enough for building high-performance multiprocessor software. We present a new discipline for concurrent programming under TSO (total store order, with store buffer forwarding). Instead of using concurrency primitives, such as locks, it is based on maintaining ownership information in ghost state, allowing the discipline to be expressed as a state invariant and verified through conventional program reasoning. If every execution of a program in a system without store buffers follows the discipline, then every execution of the program in a system with store buffers is sequentially consistent.