科研之友
微信
新浪微博
Facebook
分享链接
摘要
We propose a new approach to programming multi-core, relaxed-memory architectures in imperative, portable programming languages. Our memory model is based on explicit, programmerspecified 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.
- 出版日期2015-1
