A Calculus for Relaxed Memory
A Calculus for Relaxed Memory
复制标题
放松记忆的微积分
DOI：
10.1145/2775051.2676984
复制
发表时间：
2015
影响因子：
--
通讯作者：
Michael J. Sullivan
中科院分区：
文献类型：
--
作者：
Karl Crary;Michael J. Sullivan
我们提出了一种用命令式、可移植编程语言对多核、宽松内存架构进行编程的新方法。我们的内存模型基于明确的、程序员指定的执行顺序和写入可见性要求。然后编译器以最有效的方式实现这些要求。这与现有的内存模型形成鲜明对比，现有的内存模型（如果它们允许程序员控制同步）基于推断代码中同步操作或注释的执行和可见性结果。我们在称为 RMC\@ 的核心演算中形式化我们的内存模型。除了程序员指定的要求之外，RMC 的设计比现有架构更加宽松。它采用了一种积极的非确定性表达式语义，其中操作几乎可以以任何顺序执行，并且存储语义概括了 Sarkar 等人和 Alglave 等人的 Power 架构模型。我们为 RMC 建立了多个结果，包括两个编程规则的顺序一致性以及适当的类型安全概念。我们所有的结果都在 Coq 中形式化。
We propose a new approach to programming multi-core, relaxed-memory architectures in imperative, portable programming languages. Our memory model is based on explicit, programmer-specified requirements for order of execution and the visibility of writes. The compiler then realizes those requirements in the most efficient manner it can. This is in contrast to existing memory models, which---if they allow programmer control over synchronization at all---are based on inferring the execution and visibility consequences of synchronization operations or annotations in the code. We formalize our memory model in a core calculus called RMC\@. Outside of the programmer's specified requirements, RMC is designed to be strictly more relaxed than existing architectures. It employs an aggressively nondeterministic semantics for expressions, in which actions can be executed in nearly any order, and a store semantics that generalizes Sarkar et al.'s and Alglave et al.'s models of the Power architecture. We establish several results for RMC, including sequential consistency for two programming disciplines, and an appropriate notion of type safety. All our results are formalized in Coq.
了解 POWER 多处理器
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S
C/C 并发的库抽象
DOI：
10.1145/2429069.2429099
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M