Reasoning about the ARM weakly consistent memory model
Reasoning about the ARM weakly consistent memory model
复制标题
ARM弱一致内存模型的推理
DOI：
10.1145/1353522.1353528
复制
发表时间：
2008
期刊：
影响因子：
3.6
通讯作者：
Samin S. Ishtiaq
中科院分区：
文献类型：
--
作者：
Nathan Chong;Samin S. Ishtiaq
本文描述了ARM弱一致的内存模型的形式化：并行程序和共享内存多处理器实现之间的架构合同。我们声称，对于建筑师，微观架构和程序员来说，干净，明确且具有机械可验证的规范是一种宝贵的资源。它允许实施者锻造激进的静态（编译器）和动态（JIT，微构造）机器以运行代码。我们讨论了ARM内存模型的关键构造，可观察性 - 在共享内存多处理器系统中可见内存访问的顺序 - 并检查其在LITMUS测试中的使用。
This paper describes a formalization of the ARM weakly consistent memory model: the architectural contract between parallel programs and shared memory multiprocessor implementations. We claim that a clean, unambiguous, and mechanically verifiable specification is a valuable resource for architects, micro-architects and programmers; it allows implementors to forge aggressive static (compiler) and dynamic (JIT, micro-architecture) machines to run code. We discuss the key construct of the ARM memory model, observability -- the order in which memory accesses become visible to processors in a shared memory multiprocessor system -- and examine its use in litmus tests.