Reasoning About the ARM Weakly Consistent Memory Model

  • Nathan Chong ,
  • Samin Ishtiaq

ACM SIGPLAN Workshop on Memory Systems Performance and Correctness |

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.