Armv8-A Relaxed Virtual Memory ArmVM
A Herd-style axiomatic concurrency model extending the base Armv8-A user model with virtual-memory and address-translation events (T translation-reads, TLBI, TE, ERET, MSR, DSB) and new relations (trf, tfr, iio, tob, obtlbi, ctxob, wco), in Strong and Weak variants, with soundness/metatheory proofs. For programs with stable, injectively-mapped address spaces it collapses exactly to the base Armv8-A user-mode concurrency model (Sec. 6); outside that fragment it admits additional executions arising from translation-table manipulation and TLB maintenance.
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
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Equivalent to
- ARMv8 / AArch64 Memory Model — Simner et al., ESOP 2022, Sec. 6 (metatheorems 1–2): for programs with stable, injectively-mapped address spaces the relaxed virtual-memory model collapses exactly to the base Armv8-A user-mode concurrency model. The model is built as an extension of that base model; outside this fragment (translation-table manipulation, TLBI) it admits additional executions not expressible in base ARMv8, so the equivalence is fragment-restricted to static/injective mappings.
References
- Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell. Relaxed virtual memory in Armv8-A. ESOP 2022, 2022. doi:10.1007/978-3-030-99336-8_6