Reasoning about the ARM weakly consistent memory model

Citations Over TimeTop 10% of 2008 papers

Abstract

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.

Related Papers

• → Shared memory vs. message passing in shared-memory multiprocessors(2003)35 cited
• → A model for parallel simulation of distributed shared memory(2002)1 cited
• → Supporting Multiple Memory Consistency Models on a Shared Virtual Memory Parallel Programming Environment(1997)