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.
• 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).
• 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.

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). The target is the RA fragment of RC11.
• 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). The target is the RA fragment of RC11.

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.