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

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

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.