Relaxed Memory Model Zoo

Memory model
← Back to the map

ARM Memory Model

2011 · Alglave, Maranget, Sarkar, Sewell · hardware, formal

The ARMv7/v8 model is similar to POWER in permitting non-MCA behaviour and extensive reorderings. ARMv8 was later strengthened to be multi-copy atomic. Barriers: DMB, DSB, ISB.

Ordering relationships

Strictly weaker than
Strictly stronger than
  • Cache Coherence — ARM enforces coherence (per-address total order) as a baseline.
Incomparable with
  • IBM POWER Memory Model — Over the common instruction set ARMv7 and POWER coincide on every standard litmus family (verified against herd7's arm.cat and ppc.cat). Their incomparability is instruction-level: POWER's lightweight cumulative barrier lwsync (which allows SB) has no ARMv7 counterpart. See litmus/incomparable/ARM-vs-POWER.

References

  • Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli. Semantics of Power and ARM Multiprocessor Machine Code. DAMP 2009, 2009. doi:10.1145/1481839.1481842
  • Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. POPL 2018, 2018. doi:10.1145/3158107