Relaxed Memory Model Zoo

Ordering relationships

Strictly stronger than

• Total Store Order (TSO) — TSO allows store-load reordering; SC does not.
• x86-TSO — x86-TSO is the formal model equivalent of TSO for x86.
• C11/C++11 Memory Model — DRF-SC: SC-annotated programs behave as SC, but C11 allows weaker behaviours for non-SC atomics.
• Java Memory Model (JMM) — JMM guarantees SC for data-race-free programs but allows reordering for racy accesses.
• Linux Kernel Memory Model (LKMM) — LKMM permits reorderings of plain and *_ONCE accesses (e.g. store-buffering, SB) that SC forbids; DRF-style synchronisation must be requested explicitly with smp_mb() and friends. See litmus/strictly-weaker/SC-vs-LKMM.
• Buffered Memory Model (BMM) — BMM equips each thread with a store buffer, so the store→load (SB) outcome becomes observable; SC forbids it.

Equivalent to

• DRFx Memory Model — Both yield only sequentially consistent outcomes for data-race-free programs. DRFx additionally gives racy programs catch-fire semantics — a runtime raises an exception when it detects a region-bounded data race — so the survey groups it with SC rather than weakening the behaviour of well-synchronised code.
• End-to-End Sequential Consistency (EtE-SC) — EtE-SC restores end-to-end sequential consistency via an SC-preserving LLVM compiler and modified x86 hardware; it admits exactly the SC outcomes, differing from SC only in enforcement mechanism and performance, not in allowed behaviours.
• Volatile-by-Default (VbD) — Volatile-by-default makes every Java access sequentially consistent, so it admits exactly the SC outcomes; it differs from SC only in enforcement mechanism (speculative JIT recompilation) and performance.
• SC-Haskell (SC-Hs) — SC-Haskell preserves sequential consistency using Haskell's type system to separate thread-local from shared mutable state; it admits exactly the SC outcomes, differing from SC only in mechanism and performance.