Relaxed Memory Model Zoo

Ordering relationships

Strictly weaker than

• Sequential Consistency (SC) — DRF-SC: SC-annotated programs behave as SC, but C11 allows weaker behaviours for non-SC atomics.
• Repaired C11 (RC11) — RC11 is strictly stronger than C11: it fixes SC axioms and eliminates thin-air. All RC11 behaviours are C11 behaviours but not vice versa.
• Modular Relaxed Dependencies (MRD) — MRD is a proposed replacement for C11 relaxed atomics, forbidding thin-air reads that C11 allows.
• Symbolic MRD (sMRD) — Like MRD, Symbolic MRD repairs the C/C++ thin-air problem: it forbids the out-of-thin-air reads C11 permits while preserving the standard atomics compilation mappings, and it matches the ISO C/C++ semantic-dependency desiderata.
• Compositional Relaxed Concurrency (CRC) — CRC is a compositional semantics for a thin-air-free fragment of C11 (non-atomics with catch-fire, release-acquire, SC fences); by omitting relaxed atomics it forbids the out-of-thin-air behaviours plain C11 permits.
• Weakestmo (Event-Structure Model) (WMO) — Weakestmo grounds thin-air reads with event structures and is, in the authors' words, 'stronger than C11 (which allows OOTA) and weaker than RC11': every separating outcome (the OOTA load-buffering test and the 'RNG' bogus-value example) is allowed by C11 and forbidden by Weakestmo, with no behaviour Weakestmo allows that C11 forbids. So C11 is strictly weaker. (Reclassified from incomparable; see litmus/strictly-weaker/Weakestmo-vs-C11.)
• Concurrency Semantics for Relaxed Atomics (CSRA) — CSRA pairs a POWER-inspired memory subsystem with per-thread event structures and permits optimisation while avoiding thin-air. Its authors state CSRA is a subset of C/C++11 by design ('the converse is not to be expected ... the point of our model is to exclude the thin-air executions that C/C++11 allows'): only out-of-thin-air outcomes separate them, all allowed by C11 and forbidden by CSRA. So C11 is strictly weaker. (Reclassified from incomparable; see litmus/strictly-weaker/CSRA-vs-C11.)

Strictly stronger than

• OpenCL 2.0 Memory Model — OpenCL 2.0 extends C11 with memory scopes; at all-SVM-devices scope it coincides with C11, but narrower scopes (work-group, device) permit synchronisation-free weak behaviours that flat C11 forbids. See Batty, Donaldson & Wickerson (POPL 2016).
• CUDA C++ Memory Model — CUDA's cuda::atomic mirrors C++11 atomics but adds thread scopes (block, device, system); sub-system scopes admit behaviours C11 forbids.
• Heterogeneous-Race-Free (HRF) — HRF generalises DRF to a scope hierarchy; restricted to a single global scope it matches C11's DRF-SC guarantee, while sub-global scopes admit additional weak behaviours.

Incomparable with

• C++20 Memory Model — Two-sided: C++20's repaired seq_cst (P0668) forbids the IRIW/SC-fence behaviour that C11/C++11/14/17 allow, while C++20's weakened release sequences (P0982 — only RMWs continue a release sequence) allow a synchronisation outcome C11 forbids. Neither contains the other.
• Promising Semantics (PS) — Promising Semantics is an alternative to C11 at a similar level, not a direct subset/superset.
• Linux Kernel Memory Model (LKMM) — Neither contains the other: LKMM provides RCU grace-period ordering and the smp_* barrier family with no C11 counterpart, while C11 offers per-object seq_cst atomics LKMM does not model. The incomparability is at the level of primitives, not reorderings of shared operations. See litmus/incomparable/C11-vs-LKMM.
• Well-Justified Event Structures (WJES) — WJES uses a game-semantics-inspired notion of well-justification to forbid thin-air and prove external DRF. A load→load reordering counterexample shows its mappings to ARMv7/ARMv8/POWER are not optimal, so it is incomparable with C11.
• Generative Operational Semantics (GOS) — GOS gives a generative operational semantics with stratification constraints on speculation to rule out thin-air values and prove external DRF; it forbids thin-air reads C11 permits but is not a strict subset.
• JavaScript Memory Model (JSMM) — The JavaScript model is based on C11 and shares its thin-air problem (only internal DRF), but — unlike C11 — it does not treat racy non-atomic accesses as undefined behaviour and it natively supports mixed-size accesses over SharedArrayBuffer. Neither contains the other.
• Relaxed Memory Calculus (RMC) — The Relaxed Memory Calculus specifies ordering constraints directly in source code rather than deriving them from access annotations. It is very weak and permits thin-air values (only internal DRF is proved); its primitives differ from C11's, so the two are incomparable.
• Relaxed Atomic + Ordering (RAO) — RAO explains relaxed behaviour via transformations over an SC execution. Its authors claim external DRF while still permitting thin-air values — two properties known to be incompatible in general (Batty et al., ESOP 2015) — which the survey attributes to restrictions on the input language (no general conditionals). Incomparable with C11.
• Theory of Speculative Computation (TSC) — TSC is a general framework for the effects of speculative execution. Under unrestricted speculation the external DRF theorem fails (only internal DRF holds) and thin-air values appear; it studies speculation abstractly rather than refining C11, so the two are incomparable.