Relaxed Memory Model Zoo

Ordering relationships

Strictly weaker than

• Sequential Consistency (SC) — TSO allows store-load reordering; SC does not. Containment is machine-checked: kater decides tso ⊆ sc⁺ over kater's sc.kat and tso.kat, so every SC-consistent execution is TSO-consistent — unbounded, not up to a bound (litmus/kater/queries/strictly-weaker-SC-vs-TSO.kat). Strictness is the SB witness in litmus/strictly-weaker/SC-vs-TSO/.

Strictly stronger than

• Partial Store Order (PSO) — PSO additionally allows store-store reordering to different addresses.
• ARMv8 / AArch64 Memory Model — Both halves decided by memalloy over the common Basic_HW fragment — the vocabulary the two ISAs share, with no fences and no acquire/release annotations, where every arch-specific term of the shipped models is empty rather than dropped (litmus/memalloy/derive-hw-fragment.sh derives the operands and records the restriction exactly). Witness: a 4-event MP, ARMv8-allowed and TSO-forbidden. Containment: no execution ARMv8 forbids and TSO allows, exhaustively to 7 events; the search does find witnesses at those bounds, so it is not vacuously clean. Bounded evidence, not a theorem: the Mador-Haim small-model result would need arguing for this pair rather than assuming it. The earlier reading — a one-sided witness plus a cross-ISA monotonicity argument — is superseded, but the fragment is the scope: this decides the edge over the common vocabulary, not over the full ISAs.
• RISC-V Weak Memory Ordering (RVWMO) — Both halves decided by memalloy over the common Basic_HW fragment, as for TSO → ARMv8. memalloy ships no RISC-V model, so the operand is litmus/memalloy/models/zoo_hw_rvwmo.cat, authored here directly from the thirteen ppo rules of the RVWMO chapter of the RISC-V unprivileged spec; the file annotates each rule it renders and each that is empty on the fragment. Witness at 4 events; containment clean exhaustively to 7. Independent check on the rendering: over the same fragment it is contained in the ARMv8 operand and ARMv8 is not contained in it, which is the direction the same-address ppo rules predict. Bounded evidence about that rendering, not a theorem about RVWMO.
• Relaxed Memory Models: an Operational Approach (RMMOA) — Like PSO, RMMOA's hierarchical store buffers additionally permit store→store reordering to distinct addresses, which TSO forbids.

Equivalent to

• x86-TSO — x86-TSO formalises TSO for x86; behaviourally equivalent for standard operations.
• Buffered Memory Model (BMM) — BMM is a pragmatic TSO-style buffered model proposed as a candidate Java memory model; on the store-buffer relaxations it coincides with TSO.

Compilation target of

• WebAssembly Memory Model (Wasm) — Watt et al. 2019 Fig. 19 tabulates the compilation of Wasm memory accesses to x86 (whose ISA model is TSO), 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).