Relaxed Memory Model Zoo

Ordering relationships

Strictly weaker than

• Ou–Demsky Dependency-Preserving Criterion (OD-Dep) — Ou & Demsky 2018, §6: both approaches 'explore stronger memory models than the existing C/C++ memory model' — they forbid the OOTA/thin-air executions C11 permits while retaining ordinary relaxed-atomics reordering.
• 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

• C++17 Memory Model — C++17 narrows release sequences relative to C++11/14: only RMWs continue a release sequence, no longer later same-thread relaxed stores. That removes happens-before edges, so C++17 admits a non-synchronising message-passing outcome C++11 forbids and forbids nothing C++11 allows (the narrowing is monotone by construction). Mechanised: the all-atomic mp-rs-st-eadd-atomics is Never under cpp11.cat (C++11) and Sometimes under cpp17.cat (C++17). Models vendored from gonzalobg/cpp_memory_model; see litmus/strictly-weaker/C11-vs-C++17.
• 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.

Compiles correctly to

• WebAssembly Memory Model (Wasm) — Watt et al. 2019 §7.2 / Fig. 20 give the compilation of C/C++11 accesses to Wasm memory accesses, mapping all C/C++ atomics (relaxed, acquire/release, seq_cst) onto Wasm seqcst atomics; the sketch shows the compiled program is SC-DRF and thus behaviourally correct at the level of memory accesses.

Incomparable with

• C++20 Memory Model — Two-sided, both directions mechanised under herd7. C++20's repaired seq_cst (P0668) forbids the IRIW/SC-fence behaviour C11/C++11/14/17 allow (rc11.cat Never vs c11_orig.cat Sometimes). C++20's weakened release sequences (P0982 — only RMWs continue a release sequence) make the models incomparable on the release axis too: the all-atomic mp-rs-add-est-atomic is allowed under C++11/17 but forbidden under C++20 (cpp11/cpp17 Sometimes vs cpp2w Never), while the original RS pattern flips the other way (cpp11 Never vs cpp2w Sometimes, the C++20 outcome now a data race). Checked against the cpp11/cpp17/cpp2w cat models in litmus/models/cpp, vendored from gonzalobg/cpp_memory_model. 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.