Relaxed Memory Model Zoo

Ordering relationships

Strictly stronger than

• C11/C++11 Memory Model — RC11 is strictly stronger than C11: it fixes SC axioms and eliminates thin-air. All RC11 behaviours are C11 behaviours but not vice versa. Containment is machine-checked: kater derives C11's psc-acyclicity and coherence from RC11's acyclic(ar) over kater's rc11.kat and c11-old.kat (litmus/kater/queries/strictly-weaker-RC11-vs-C11.kat). Strictness is the witness in litmus/strictly-weaker/RC11-vs-C11/.
• C++20 Memory Model — C++20 adopts RC11's repaired SC (P0668) but, unlike RC11, does not adopt the no-thin-air axiom acyclic(po ∪ rf): it still permits out-of-thin-air / plain load-buffering reads that RC11 forbids. So RC11 is strictly stronger.
• Repaired C11 with C++17 release sequences (RC17) — RC17 is RC11 with the C++17 release-sequence narrowing (RMWs only). Like the C11→C++17 case the narrowing is monotone — it only removes synchronisation — so RC17 admits an outcome RC11 forbids and forbids nothing RC11 allows. Mechanised: mp-rs-add-est-atomic is Never under rc11.cat and Sometimes under rc17.cat. Models vendored from gonzalobg/cpp_memory_model; see litmus/strictly-weaker/RC11-vs-RC17.
• Modular Relaxed Dependencies (MRD) — Paviotti et al. (Modular Relaxed Dependencies in Weak Memory Concurrency, ESOP 2020) relax the RC11 axiomatic model with their MRD dependency model to form MRD-C11. Lemma 3 (Implementability of MRD-C11): for all programs P, ⟦P⟧MRD-C11 ⊇ ⟦P⟧RC11 — MRD-C11 is strictly weaker than RC11, admitting the false-dependency-eliminating load→store reorderings RC11 forbids while still forbidding out-of-thin-air. (The MRD+IMM instantiation of Theorem 3, ⟦P⟧MRD+IMM ⊇ ⟦P⟧IMM, is a distinct model and is not represented by this node.)
• Symbolic MRD (sMRD) — Symbolic MRD interfaces with an RC11-style axiomatic model but refines its dependency relation (dp), removing false dependencies so that load→store reorderings in load-buffering shapes — e.g. the LB+UB+data outcome RC11 forbids because of a cycle in ⊑∪rf — become allowed, while genuine out-of-thin-air cycles stay forbidden. It therefore admits strictly more behaviours than RC11.
• Java Access Modes (JAM) — JAM borrows RC11's OOTA fix for opaque and stronger accesses, but unlike RC11 it does not tackle thin-air for plain (non-atomic) accesses, so it permits more behaviours.

Equivalent to

• C++ Transactional Memory Extension (C++TM) — Chong, Sorensen & Wickerson (PLDI 2018, §7) build the C++ TM model on the baseline C++ model of Lahav et al. (RC11), making only two amendments (an unchanged race definition and transactional synchronisation folded into happens-before) that vanish when there are no transactions. On the non-transactional fragment it coincides with RC11 by construction.
• RC11z (Allocation-Aware RC11) — RC11z extends the operational RC11-RAR semantics so that allocation and deallocation are explicit write events; a read taking its value from such an event surfaces as a read-from-uninitialised or use-after-free error. On the concurrency behaviours of well-allocated programs it coincides with RC11 — the added allocation layer exists to verify safe memory reclamation (RCU).
• Release-Acquire (C/C++11 RA fragment) — 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'.
• Operational Release-Acquire/Relaxed RC11 (RAR) — RAR is an operational reformulation of RC11's release-acquire and relaxed fragment, used as the basis for an invariant-based proof calculus.
• Operational RC11 (ORC11) — ORC11 is an operational version of RC11 developed for RustBelt to verify Rust standard-library synchronisation primitives against a program logic.

Incomparable with

• Intermediate Memory Model (IMM) — IMM is designed to compile correctly to hardware; it is related to RC11 but targets a different point in the design space.
• Pomsets with Predicate Transformers (The Leaky Semicolon) (PwT) — Leaky Semicolon §9: 'PwT-mca is incomparable to both RC11 ... and the promising semantics'. RC11 allows non-multi-copy-atomic behaviours that PwT-mca disallows, while PwT-mca allows optimisations that RC11's No-Thin-Air axiom forbids.