ARM Memory Model
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.
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes Load→Store
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic Pulte et al. 2018
Ordering relationships
- Strictly weaker than
- ARMv8 / AArch64 Memory Model — ARMv7 is non-MCA and weaker than ARMv8.
- Strictly stronger than
- Cache Coherence — ARM enforces coherence (per-address total order) as a baseline.
- Compilation target of
- WebAssembly Memory Model (Wasm) — Watt et al. 2019 Fig. 19 gives the compilation of Wasm memory accesses to ARMv7, following the established C/C++11 SC-atomic schemes [Sewell & Sevcik 2016]; full mixed-size correctness is flagged as an open problem (§7.1.1).
- 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