Relaxed Memory Model Zoo

Ordering relationships

Strictly weaker than

• Strong Release-Acquire (SRA) — 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.

Strictly stronger than

• Weak Release-Acquire (WRA) — WRA drops modification order entirely, replacing RA's write-coherence and read-coherence with weak-read-coherence over hb|loc; Lahav & Boker note that write-coherence implies [W];hb|loc;[W] subset of mo, so read-coherence implies weak-read-coherence and RA contains WRA (Prop. 3.2). Strictness is Ex. 3.7, three single-location programs (WW, Oscillating, SF) allowed by WRA and forbidden by RA: WRA does not provide SC-per-location, so even one-location programs may behave non-sequentially.

Equivalent to

• Repaired C11 (RC11) — RA is the release/acquire fragment of the C/C++11 model — release stores, acquire reads, acquire-release RMWs (Lahav & Boker, §3.1). RC11's repairs concern the SC axioms and the relaxed/thin-air fragment, none of which this fragment contains, so RC11 and C11 coincide on it. Drawn against RC11 rather than C11 to match the existing PSI and SI compilation notes, which target 'the release-acquire (RA) fragment of RC11'.

Compilation target of

• Parallel Snapshot Isolation (PSI) — Raad, Lahav & Vafeiadis (ESOP 2018) give PSI a lock-based reference implementation built on the release-acquire (RA) fragment of the C/C++11 memory model, proved sound and complete against the declarative PSI specification (and likewise Robust PSI). Retargeted from RC11 onto RA in 1.4.1: the target has always been the release-acquire fragment, as this note already said, and RA became a node in 1.4.0.
• Snapshot Isolation (SI) — Raad, Lahav & Vafeiadis (VMCAI 2019) give SI two timestamp-free lock-based (MRSW) reference implementations built on the release-acquire (RA) fragment of C/C++11, proved sound and complete against the declarative SI specification (and likewise Robust SI). Retargeted from RC11 onto RA in 1.4.1: the target has always been the release-acquire fragment, as this note already said, and RA became a node in 1.4.0.