Relaxed Memory Model Zoo

Ordering relationships

Strictly weaker than

• Total Store Order (TSO) — ARMv8 allows more reorderings than TSO though it is multi-copy-atomic. The TSO ⊆ ARMv8 containment is a model-level monotonicity argument over different instruction sets, not a cited theorem, so the edge is recorded as litmus-grade: the strict order is argued (monotonicity) and corroborated by the sweep, not independently proven — a genuine strict order, drawn lighter than a literature-backed one, not an edge that might be incomparable.

Strictly stronger than

• ARM Memory Model — ARMv7 is non-MCA and weaker than ARMv8.

Equivalent to

• Persistent ARMv8 (PARMv8) — Raad, Wickerson & Vafeiadis (OOPSLA 2019): PARMv8's crash-free behaviour coincides with ARMv8. fragment_restricted because the equivalence holds only on the crash-free fragment; the persist-order axiom is orthogonal.
• ARMv8 + DJR Transactions (ARMv8+DJR) — Dongol, Jagadeesan & Riely (POPL 2018) instantiate their transactional framework at ARMv8; the added transactional axioms only constrain transactional events, so on programs with no transactions the ARMv8 instance coincides with ARMv8 by construction. fragment_restricted: the coincidence holds only on the non-transactional fragment.
• Armv8-A Relaxed Virtual Memory (ArmVM) — 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.
• Armv8-A System Semantics: Instruction Fetch (ArmIF) — Simner et al., ESOP 2020: the instruction-fetch system-semantics model is built by extending the base Armv8-A user-mode concurrency (Flat) model with instruction-fetch and IC/DC cache-maintenance events (Sec. 4-5, 'extending previous work on user-mode concurrency'). Validation (Sec. 6) reports the model's results are identical to the base model over all 8950 non-instruction-fetch Flat regression tests, so on the fragment with no instruction fetch or cache maintenance it coincides with base ARMv8; outside that fragment (self-modifying code, IC/DC) it admits additional relaxed executions, hence the equivalence is fragment-restricted.
• Promising-ARM/RISC-V (P-ARM/RV) — Pulte et al. (PLDI 2019), Appendix D, Theorem D.1: the operational Promising-ARM model is proven equivalent in Coq to the axiomatic ARMv8 model for finite executions.

Compilation target of

• Intermediate Memory Model (IMM) — IMM compiles correctly to ARMv8.
• Linux Kernel Memory Model (LKMM) — Linux kernel primitives compile correctly to ARMv8/AArch64.
• WebAssembly Memory Model (Wasm) — Watt et al. 2019 Fig. 19 gives the compilation of Wasm memory accesses to AArch64/ARMv8 (LDR/STR, LDAR/STLR), 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

• RISC-V Weak Memory Ordering (RVWMO) — Both are multi-copy atomic and coincide on every standard litmus family over the common instruction set (verified against herd7's aarch64.cat and riscv.cat). The incomparability is instruction-level: RISC-V's fence.tso (which allows SB) and the RCsc/RCpc atomics differ from ARMv8's. See litmus/incomparable/ARMv8-vs-RVWMO.