Relaxed Memory Model Zoo

Ordering relationships

Strictly weaker than

• Sequential Consistency (SC) — SRA is the strongest of the release-acquire family and is still strictly weaker than SC: Lahav & Boker Ex. 3.5 marks the IRIW outcome allowed under WRA, RA and SRA alike, and SC forbids it. Store buffering is likewise allowed — SRA's compilation to x86-TSO uses plain accesses. The SRA paper supplies fences that restore sequential consistency, which is only meaningful because the model without them is weaker.

Strictly stronger than

• Release-Acquire (C/C++11 RA fragment) — SRA replaces RA's write-coherence (mo;hb irreflexive — a local agreement between modification order and happens-before) with strong-write-coherence ((hb ∪ mo)+ irreflexive — a global one), keeping RA's other axioms (Lahav & Boker, Table 1); containment is immediate. Strictness is the 2+2W program of Lahav et al. 2016, Lahav & Boker Ex. 3.6: x:=1; y:=2; a:=y || y:=1; x:=2; b:=x with a=b=1. The outcome forces mo edges W(y,2) -> W(y,1) and W(x,2) -> W(x,1), closing an (hb ∪ mo) cycle that SRA forbids while each mo;hb step alone satisfies write-coherence, so RA allows it. Machine-checked: litmus/models/ra.cat and litmus/models/sra.cat are authored for this dataset and differ in that one axiom, and litmus/strictly-weaker/SRA-vs-RA/ runs 2+2W under both (Sometimes 1 8 vs Never 0 5). Because both cat models are hand-written rather than vendored, the directory also carries controls run by run.sh: MP+relacq must be forbidden by both, and IRIW must be allowed by both — the latter checked against Lahav & Boker Ex. 3.5, which marks IRIW allowed under RA and SRA alike. Containment remains the cited one-axiom argument; herd7 decides the strictness half only.

Equivalent to

• Causal Convergence (CCv) — Lahav & Boker, §3.1: ignoring RMWs, SRA is equivalent to the causal convergence model CCv of Bouajjani et al., applied to the standard sequential specification of a read/write key-value store (and to the causal consistency of Cerone et al. restricted to single-instruction transactions). fragment_restricted because the equivalence is stated modulo RMWs: SRA's atomicity axiom has no counterpart in a model over a sequential key-value specification. This edge is the bridge between the C11 family and the distributed causal-consistency cluster.

Compiles correctly to

• x86-TSO — Lahav, Giannarakis & Vafeiadis, POPL 2016: SRA has exactly the same compilation scheme to x86-TSO as the RA fragment it strengthens — plain loads and stores, no fences — so the strengthening carries no implementation cost on x86.
• IBM POWER Memory Model — Lahav, Giannarakis & Vafeiadis, POPL 2016: SRA compiles to POWER by the standard RA scheme (lwsync before every store, ctrl+isync after every load), and the mapping is complete as well as sound — the compiled program exhibits exactly the behaviours of the source. Lahav & Boker restate it as SRA precisely coinciding with the POWER model of Alglave et al. restricted to programs compiled from the RA fragment. Completeness is what makes SRA maximal: it cannot be strengthened further without an implementation cost on POWER.