Relaxed Memory Model Zoo

Ordering relationships

Strictly stronger than

• Ou–Demsky Load-Store-Ordering Criterion (OD-LSO) — Ou & Demsky 2018, §6: 'the constraints we impose in general are much weaker than the sequential consistency memory model.' The load-store-ordering criterion permits relaxed-atomics reorderings SC forbids while ruling out OOTA.
• 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.
• Processor Consistency (PC) — Sequential consistency is strictly stronger than processor consistency (Goodman 1989; Steinke & Nutt 2004).
• Causal Consistency — Causal memory is strictly weaker than sequential consistency (Ahamad et al. 1995; Steinke & Nutt 2004).

Equivalent to

• SC + DJR Transactions (SC+DJR) — Dongol, Jagadeesan & Riely (POPL 2018) give a transactional framework parametric in the base architecture and instantiate it at SC; its added transactional axioms only constrain transactional events, so on programs with no transactions the SC instance coincides with SC by construction. fragment_restricted: they coincide only on the non-transactional fragment — the framework adds an orthogonal transactional layer with observable-serializability guarantees.
• 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.
• DeNovo — The paper states DeNovo provides sequential consistency for data-race-free programs, so on the race-free fragment it admits exactly the SC outcomes. Unlike DRFx it assumes race-freedom is supplied by the disciplined language (Deterministic Parallel Java) rather than detected at runtime, and defines no behaviour for racy programs.
• DeNovoND — Sung, Komuravelli & Adve (DeNovoND, ASPLOS 2013) state their disciplined-non-determinism (lock-based) design guarantees sequential consistency, so on the data-race-free fragment it admits exactly the SC outcomes. Like DeNovo it assumes software supplies race-freedom and defines no behaviour for racy programs; the value-add over DeNovo is the coherence design (locks / access signatures), not the consistency class.
• DeNovoSync — Sung & Adve (DeNovoSync, ASPLOS 2015) adopt the standard C++/Java data-race-free memory model, which defines sequentially consistent semantics for data-race-free programs (SC is used as the correctness criterion for synchronization accesses), so on the race-free fragment it admits exactly the SC outcomes. It extends DeNovo to arbitrary synchronization while keeping this SC-for-DRF contract.
• Spandex — Alsop, Sinclair & Adve (Spandex, ISCA 2018) state they assume a sequential-consistency-for-data-race-free (SC-for-DRF) model, so on the race-free fragment it admits exactly the SC outcomes; the flexible coherence request types affect only performance, not the consistency guarantee.