A relaxed memory model — also called a weak memory model — specifies which results a concurrent program may observe when threads share memory. Sequential consistency, the strongest model, requires every operation to appear in a single global order matching each thread's program order. Real hardware and programming languages relax that guarantee: CPUs (x86-TSO, ARMv8, Power, RISC-V) and languages (C/C++11, Java, LLVM) reorder reads and writes to run faster, so they admit more behaviours than sequential consistency allows.
The Relaxed Memory Model Zoo maps these models against one another, ordered by the inclusion of their allowed execution behaviours: an arrow from A to B means B is strictly weaker than A (it permits everything A does, and more). Explore the interactive map above, or browse the full catalogue of memory models below.
A text index of all 49 hardware and programming-language memory consistency models in the zoo — from Sequential Consistency, x86-TSO, ARMv8, Power, RISC-V, C/C++11, Java and LLVM — with their defining references. Each links to its own page; the interactive map above orders them by the inclusion of their allowed execution behaviours.
The strongest model. All operations appear to execute in a single global total order consistent with each thread's program order. No reordering of any kind is permitted.
The minimal requirement that writes to a single address are seen in the same order by all processors. Implied by virtually all hardware models. Stronger than nothing, but much weaker than SC.
Extends TSO by additionally allowing store-store reordering to different addresses. A thread's writes to distinct locations may become visible to other threads out of program order.
The weakest SPARC model. Allows all four reorderings (load-load, load-store, store-load, store-store) between independent memory operations.
A write goes into a per-thread FIFO store buffer before becoming globally visible. Reads can observe a thread's own buffered write before others can. Store-load reordering is the principal relaxation over SC.
Formalised in JSR-133. Defines happens-before (HB) based on synchronisation actions. Provides DRF-SC guarantee. Known for complexities around causality and out-of-thin-air values.
The 'Relaxed Atomic + Ordering' model, in which relaxed behaviours are explained through transformations applied over a sequentially consistent execution. The authors claim the external DRF guarantee 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 supported input language (for example, the absence of general conditional statements).
An operational approach to the semantics of relaxed memory, built on an abstract machine with a main memory and a hierarchical structure of store buffers in which writes to different locations may propagate to memory out of order — the same store→store relaxation as PSO. The authors prove the external DRF theorem.
An SC-preserving model with catch-fire semantics. A runtime is guaranteed to raise an exception if a program has a data race, and otherwise yields only sequentially consistent outcomes; the data-race detection is made practical through region-bounded checks with some hardware support. Any sequentially valid optimisation (instruction reordering, common-subexpression elimination) is sound within compiler-designated regions, but transformations that introduce speculative reads or writes are unsound. An efficient hardware-assisted implementation is reported at roughly 3.25% average overhead.
A generative operational semantics that attempts to fix the JMM by constraining speculative execution with stratification conditions to rule out thin-air values. The authors prove the external DRF theorem and verify a few program transformations (store→store reordering, load/load elimination, and roach-motel reordering), though the overall study of transformations is not systematic.
A general framework for studying the effects of speculative computation in a shared-memory setting. The authors observe that under unrestricted speculation the external DRF theorem fails, while the internal DRF theorem can still be proved; the framework analyses speculation abstractly rather than proposing a concrete language model.
A rigorous formal model for x86 multiprocessor memory, validated against AMD and Intel hardware. Captures FIFO store buffers, lock prefixes, and MFENCE barriers precisely.
The ARMv7/v8 model is similar to POWER in permitting non-MCA behaviour and extensive reorderings. ARMv8 was later strengthened to be multi-copy atomic. Barriers: DMB, DSB, ISB.
The first standardised memory model for C and C++. Introduces a hierarchy of atomic operations (relaxed, acquire, release, acq_rel, seq_cst) and defines data-race-free (DRF) programs. Formally specified by Batty et al. Contains the notorious 'thin-air' problem for relaxed atomics.
The POWER architecture model allows extensive reorderings and non-multi-copy-atomic (non-MCA) behaviour: a store can be visible to one thread before others. Requires explicit barriers (sync, lwsync, isync) or dependencies for ordering.
An approach to providing end-to-end sequential consistency for a language, enforced jointly by an SC-preserving variant of the LLVM compiler and modified x86 hardware. To curb the overhead it enforces SC only for accesses to shared mutable variables, classifying memory regions as thread-local, shared-immutable, or shared-mutable via a combination of static compiler analysis and hardware-assisted dynamic analysis. Reported overhead is 6.2% on average (17% maximum) versus stock LLVM and x86. Like the other SC-preserving designs it admits exactly the SC behaviours.
A pragmatic, TSO-style buffered memory model proposed as a candidate for Java, motivated by building a verified JVM in the spirit of CompCertTSO rather than fully replacing the JMM. Each thread has a store buffer, so the principal relaxation over SC is store→load reordering. The authors proved the external DRF theorem and the soundness of several program transformations, and modified an open-source JVM to preserve BMM at roughly 1% average overhead on x86.
The foundational framework that introduced scoped synchronisation. It generalises data-race-free (DRF) to a scope hierarchy, distinguishing HRF-direct (scopes must match exactly) and HRF-indirect (transitive scope chains). Heterogeneous-race-free programs get an SC-like guarantee; using sub-global scopes admits behaviours flat DRF forbids. Most subsequent GPU models build on it.
The memory model underlying AMD's GCN, CDNA and RDNA GPUs, built on the HSA heterogeneous, scoped, release-consistency framework. Memory operations carry explicit scope qualifiers (work-group, agent/device, system) and cache-control hints; ordering between threads holds only within a shared scope.
The Relaxed Memory Calculus, an alternative approach in which ordering constraints between memory accesses are specified directly in the source code rather than derived from per-access annotations. The approach is highly generic and subsumes the traditional annotation style of C11. The resulting model is very weak and permits thin-air values, but the authors prove the internal DRF theorem.
A generalisation of the C11 DRF framework with a scope hierarchy, relaxing HRF-direct/indirect's strict scope-matching to suit industrial heterogeneous models. It underpins the scoped-atomics designs adopted by OpenCL, HSA and the GPU vendor models.
A concurrency semantics for relaxed atomics that permits optimisation while avoiding thin-air executions. It pairs a memory subsystem inspired by the POWER model with a thread subsystem in which each thread is represented as an event structure; at each step the machine may either commit an event to memory or transform one of the event structures. Soundness of the optimal compilation mappings to x86 and POWER was shown, though the mappings to ARMv7/ARMv8 were later revealed to be non-optimal.
A scoped extension of the C11 model for heterogeneous compute, adding memory scopes (work-item, work-group, device, all-SVM-devices) on top of C11's atomic orderings. At all-devices scope it coincides with C11; narrower scopes permit additional weak behaviours. Formalised and repaired alongside C11 by Batty, Donaldson & Wickerson (POPL 2016).
An operational happens-before model proposed to repair the Java Memory Model. Its abstract machine uses a global event buffer, where events may be reordered before propagating to a global history main memory, together with a replay mechanism to simulate speculative executions. To avoid thin-air outcomes it tracks syntactic dependencies between events and forbids reordering dependent events. The authors proved the external DRF theorem and the soundness of several transformations.
A model based on event structures with a notion of well-justification — inspired by game semantics — used to forbid thin-air values and prove the external DRF guarantee. The authors do not study the soundness of program transformations, but exhibit a load→load reordering counterexample, which also implies that the compilation mappings to ARMv7, ARMv8, and POWER are not optimal.
Apple's GPU programming model provides a relaxed memory model with atomics (relaxed/acquire/release) and threadgroup/device barriers in the Metal Shading Language. It is less formally specified in public than the other GPU models here.
The host/device-coherent, C++-style scoped memory model exposed by CUDA since version 9 (cuda::atomic with thread-scope template parameters). It mirrors the C++11 atomics interface and is layered on, and lowered to, the PTX memory model.
An operational model for relaxed memory based on the notion of thread-local 'promises': a thread may promise a future write and later fulfil it. Eliminates thin-air values, supports DRF-SC, and can express optimisation-friendly behaviour. Extended to PS 2.0 for mixed-size and non-atomic accesses.
A repaired version of C11 that fixes the SC axioms, eliminates the 'out-of-thin-air' problem for SC and release-acquire accesses, and supports DRF-SC. Fully compositional and supports modular reasoning.
An SC-preserving model for Haskell that separates thread-local from shared mutable memory using Haskell's strong type system, so the type checker enforces the discipline needed to preserve SC. A modified GHC was measured on 1,279 benchmarks with only a 0.4% geometric-mean slowdown (just 12 benchmarks above 10%), helped by Haskell's purely functional style minimising shared mutable state. It admits exactly the SC behaviours.
A volatile-by-default semantics for Java in which every memory access is treated as volatile (sequentially consistent) by default. Bare VbD carries a considerable penalty (28% average / 81% maximum on x86; 57% / 157% on Armv8), so the authors add a just-in-time technique that speculatively treats each object as thread-local and compiles its accesses without fences, recompiling to insert fences once concurrent access is detected — bringing the Armv8 overhead down to 37% average / 73% maximum. It admits exactly the SC behaviours.
A strengthened, formally specified model for ARMv8. Multi-copy atomic (stores become visible to all threads simultaneously). Introduces the LDAR/STLR acquire-release instructions. Strictly stronger than ARMv7.
A compositional relaxed-concurrency semantics for a fragment of the C11 model — non-atomic accesses with catch-fire semantics, release-acquire accesses, and sequentially-consistent fences. Because the relaxed fragment is excluded, the model sidesteps the thin-air problem. The authors built a tool for automatic verification of program transformations in this fragment.
An axiomatic (cat/herd7) model for the Linux kernel's own concurrency primitives — READ_ONCE/WRITE_ONCE, smp_mb()/smp_rmb()/smp_wmb()/smp_store_release()/smp_load_acquire(), RCU, and locking. Deliberately defined as a weak 'virtual architecture' so that code verified against it is sound on every CPU the kernel supports (x86, ARM, POWER, RISC-V, …). Notably formalises RCU grace-period ordering, which language standards such as C11 do not express.
Memory model for OCaml multicore. Based on a 'local DRF' guarantee. Provides strong guarantees for well-typed programs without data races, and well-defined (though weak) semantics for racy accesses.
Khronos's formal, relaxed, scoped memory model for the Vulkan GPU API. Ordering is expressed through scoped synchronisation plus explicit availability and visibility operations that move writes through the cache hierarchy. Specified executably in Alloy, with the formalisation led largely by Jade Alglave and collaborators.
Bridging model between high-level language models and hardware. Correctly compiles to x86-TSO, ARMv8, and POWER. Supports DRF-SC and eliminates thin-air reads. Serves as a compilation target and proof intermediate.
A formalisation of a revised Java Memory Model built on the 'Java Access Modes' (plain, opaque, release/acquire, volatile) introduced with VarHandles in JDK 9. Inspired by RC11, it adopts RC11's solution to the out-of-thin-air problem and forbids load/store reorderings for opaque or stronger accesses, but it deliberately does not tackle thin-air on the level of plain (non-atomic) accesses.
A scoped, relaxed model for NVIDIA's PTX virtual ISA, with relaxed/acquire/release atomics and explicit thread scopes (CTA, GPU, system). Synchronisation only takes effect between threads that share the named scope, so narrower scopes admit weak behaviours a flat model forbids. Formalised and machine-checked by Lustig et al. (ASPLOS 2019) and the foundation for CUDA's cuda::atomic semantics.
An operational version of RC11 (Operational RC11) developed for the RustBelt project. It underpins a program logic that was used to prove the soundness of several synchronisation primitives from the Rust standard library against the relaxed-memory semantics. Being equivalent to RC11, ORC11 is strictly stronger than the C++20 model Rust normatively ships (it forbids the out-of-thin-air, plain load-buffering and broken-release-sequence behaviours C++20 leaves open): it is the verification model RustBelt reasons against, a sound over-approximation of shipped Rust, not a model of its exact semantics.
An operational reformulation of RC11 supporting release-acquire and relaxed accesses (hence RAR), on top of which the authors build a proof calculus for invariant-based reasoning and mechanically verify mutual-exclusion algorithms.
The official memory model for RISC-V. A carefully designed relaxed model weaker than TSO but stronger than POWER/ARM. Defines ordering via FENCE instructions and load-reserved/store-conditional pairs. Formally specified in the RISC-V ISA manual.
A semantic-dependency-preserving model that grounds thin-air reads using event structures, which can simultaneously encode multiple conflicting executions in order to model speculation. It admits the optimal compilation mappings, many program transformations, and the external DRF guarantee, and — unlike the Promising semantics — it also supports sequentially consistent accesses. It descends from a formalisation of an LLVM concurrency fragment by the same authors.
The C++ memory model as revised for C++20. It adopts the repaired sequential-consistency semantics of Lahav et al. (P0668), strengthening seq_cst atomics and fences so the broken IRIW / SC-fence behaviours of C++11/14/17 become forbidden; and it weakens release sequences (P0982) so that only RMWs — not later relaxed stores by the same thread — continue them. It still does not resolve the thin-air problem, so out-of-thin-air reads remain (unlike RC11). The seq_cst strengthening and the release-sequence weakening pull in opposite directions, leaving C++20 incomparable with the original C11/C++11 model and strictly weaker than RC11. This is also the model Rust normatively adopts for core::sync::atomic: the shipped Rust atomics model is C++20 (not full RC11 — see ORC11, the stronger operational RC11 used to verify Rust's standard library).
The memory model of JavaScript, based on the C11 model. Like C11 it suffers from the thin-air problem and so provides only the internal DRF guarantee, but — unlike C11 — it does not treat racy non-atomic accesses as undefined behaviour. Because its main shared primitive is the SharedArrayBuffer, a linear mutable byte buffer, the model naturally supports mixed-size accesses. It was repaired and mechanised by Watt et al.
Resolves the thin-air problem by tracking syntactic dependencies modularly, using a denotational semantics. Intended as a sound and compositional replacement for relaxed C11 atomics.
A variant of RC11 — the operational RC11-RAR fragment with relaxed and release-acquire accesses — extended with an explicit model of pointers and memory allocation, developed to verify safe memory reclamation (Read-Copy-Update, RCU) under weak memory. Allocation and deallocation are modelled as ordinary write events in the same memory state; a read that takes its value from an allocation or deallocation event therefore surfaces as a read-from-uninitialised or use-after-free error, making the ABA / reclamation hazards of lock-free code visible to the model. Combined with an ownership discipline and an Owicki-Gries logic, and mechanised in Isabelle/HOL. Locally dubbed RC11z, the 'z' standing for the zeroing allocation/deallocation events.
A relaxed, scoped memory model for portable GPU compute in the browser, derived closely from Vulkan's. WGSL provides relaxed atomics, work-group barriers and storage/work-group address spaces; implementations lower it to Vulkan, Metal or Direct3D 12.
A successor to Modular Relaxed Dependencies (MRD) and the first thin-air-free memory model to admit compiler optimisations that aggressively leverage alias analysis, an assumption of freedom from undefined behaviour, and the extrinsic choices of real implementations (e.g. over-alignment). Built on symbolic execution, it models dynamic memory — allocation, dereferencing, and reclamation — rather than only concrete locations, and exports a semantic-dependency relation that integrates with the C/C++ memory model, preserving the standard compilation mappings for atomics. It matches every test in the recently published ISO C/C++ semantic-dependency desiderata, and its tooling runs orders of magnitude faster than other executable thin-air-free semantics.