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 101 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.
Writes performed by a single process are seen by all other processes in the order they were issued, but writes from different processes may be seen in different orders by different processes. Strictly weaker than processor and causal consistency; incomparable to cache consistency; strictly stronger than slow consistency.
Goodman's processor consistency: PRAM consistency together with cache consistency — writes by each process are seen by all processes in the order issued, and all writes to a single location are seen in one sequential order. Strictly weaker than SC; strictly stronger than both PRAM and cache consistency; incomparable to causal consistency.
The minimal requirement that writes to a single address are seen in the same order by all processors. Implied by virtually all hardware models, and identical to Goodman's cache consistency in the Steinke–Nutt lattice. Much weaker than SC; incomparable to PRAM and causal consistency; strictly weaker than processor consistency and strictly stronger than slow consistency.
A read must return some value previously written to the location, and once a value has been read no earlier write to that location by the same writer may be returned; a process sees its own writes immediately. Strictly weaker than both PRAM and cache consistency; strictly stronger than local consistency.
DEC's Alpha is widely regarded as the weakest mainstream hardware memory model. It permits all four load/store reorderings and, distinctively, does not preserve dependent (address- or data-dependent) load ordering without an explicit memory barrier (mb) — behaviour no other mainstream ISA exhibits, and the historical case that motivated Linux's smp_read_barrier_depends()/RCU barrier machinery. Non-multi-copy-atomic.
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.
Monotonic reads session guarantee of Terry et al. (PDIS 1994): successive reads within a session reflect a non-decreasing set of writes, i.e. a session never observes an earlier state after observing a later one. One of the four session guarantees. Brzezinski et al. (2003) proved PRAM = read-your-writes ∧ monotonic reads ∧ monotonic writes (Viotti & Vukolić 2016, Eq. 20), so monotonic reads alone is strictly weaker than PRAM.
Monotonic writes session guarantee of Terry et al. (PDIS 1994): a replica applies a write from a session only after it has applied all previous writes of that same session, so writes of a session take effect in the order issued. One of the four session guarantees. Brzezinski et al. (2003) proved PRAM = read-your-writes ∧ monotonic reads ∧ monotonic writes (Viotti & Vukolić 2016, Eq. 20), so monotonic writes alone is strictly weaker than PRAM.
Read-your-writes (a.k.a. read-my-writes) session guarantee of Terry et al. (PDIS 1994): a read carried out on behalf of a session only reflects a state that has already applied all writes previously issued in that same session. On its own it is one of the four session guarantees. Brzezinski et al. (2003) proved PRAM consistency holds iff a system provides read-your-writes together with monotonic reads and monotonic writes (Viotti & Vukolić 2016, Eq. 20), so read-your-writes alone is strictly weaker than PRAM.
The weakest SPARC model. Allows all four reorderings (load-load, load-store, store-load, store-store) between independent memory operations.
Writes-follow-reads session guarantee of Terry et al. (PDIS 1994), sometimes called session causality: writes issued in a session are ordered after any writes whose effects were observed by earlier reads in that session (Viotti & Vukolić 2016, Eq. 25). One of the four session guarantees. Brzezinski et al. (2004) proved that causal consistency requires and includes all four session guarantees (so causal = PRAM ∧ writes-follow-reads), hence writes-follow-reads is strictly weaker than causal consistency.
Causal memory: for each process, its own operations plus all writes known to it appear in a total order that respects Lamport's potential causality (writes as sends, reads as receives). Strictly weaker than SC; strictly stronger than PRAM; incomparable to processor and cache consistency.
The weakest consistency model: each process's own operations appear in its program order, with no constraint on the order in which writes by other processes become visible, and different processes may see different orders. The bottom of the Steinke–Nutt lattice.
The memory-ordering model of the Intel Itanium (IA-64) architecture. Ordinary loads and stores are 'unordered' and may be reordered in all four directions; ordering is imposed explicitly by acquire loads (ld.acq), release stores (st.rel) and the memory fence (mf) — a ld.acq is ordered before every following memory operation and a st.rel after every preceding one. This ISA-level acquire/release design is closer in spirit to ARMv8's LDAR/STLR than to a bare relaxed-plus-barrier model like POWER/ARMv7. Cache coherence (a per-location total order on writes) is guaranteed. Two independent academic formalizations exist: Yang et al. (CHARME 2003), a logic-programming/SAT axiomatization of the ordering rules, and Higham, Jackson & Kawash (2007), a programmer-centric 'views' characterization which finds the vendor specification not fully tight (the model lies between two closely related definitions). Neither formalization nor the vendor manual states a machine-checked containment or incomparability against another model in this dataset, so no strength edge is drawn.
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.
Convergent causal consistency, introduced with the COPS wide-area store. It augments causal consistency with strong convergence: replicas that have applied the same set of writes have equivalent state, so concurrent (causally unrelated) conflicting writes are resolved identically at every replica via commutative/associative handler functions. Viotti & Vukolić (ACM Computing Surveys 2016, Eq. 27) express it as Causal+ = Causality ∧ StrongConvergence, i.e. causal+ strengthens causal consistency exactly as strong eventual consistency strengthens eventual consistency, so it is strictly stronger than causal consistency. Incomparable to real-time causal consistency.
A hardware/software co-designed cache-coherence protocol that exploits a disciplined parallel programming model (Deterministic Parallel Java) — structured parallel control, data-race freedom, and deterministic semantics — to simplify the memory hierarchy. By assuming race-free code the protocol eliminates transient coherence states (model checking finds 15x fewer reachable states than a conventional MESI protocol) and guarantees sequential consistency for data-race-free programs, while improving cache hit rates, network traffic, performance, and energy.
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.
A strengthening of causal consistency due to Mahajan, Alvisi & Dahlin: in addition to causality it enforces a real-time condition — causally concurrent writes that do not overlap in real time must be applied in their real-time order. Viotti & Vukolić (ACM Computing Surveys 2016, Eq. 28) express it as RealTimeCausality = Causality ∧ RealTime, so it is strictly stronger than causal consistency. It is incomparable to causal+: real-time causality does not imply strong convergence, and causal+ does not imply the real-time ordering (V-V §3.5, correcting Lloyd et al.'s original classification).
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 source-level memory model of CompCertTSO, a Coq-verified compiler from a concurrent C-like language (a threaded extension of CompCert's Clight) to x86 assembly. By design it mirrors the x86-TSO model at the language level, exposing per-thread FIFO store buffers, loads, stores, compare-and-swap, and memory barriers with TSO behaviour; a single TSO abstract machine is shared across all of the compiler's intermediate languages. The store→load relaxation is thus exactly that of TSO/x86-TSO, making it a verified-compiler vehicle for the same model rather than a behaviourally distinct one.
A hardware/software co-designed extension of the DeNovo coherence protocol that adds efficient support for disciplined non-determinism — lock-based synchronization — on top of DeNovo's deterministic core. It combines distributed queue-based locks with access signatures to keep the protocol free of transient coherence states, invalidation traffic, directories, and false sharing, while still guaranteeing sequential consistency for data-race-free programs. It is reported to match or improve on a MESI baseline in performance and energy for non-deterministic (lock-based) workloads.
Basic eventual consistency for replicated data stores, defined axiomatically over abstract executions with visibility and arbitration relations (in analogy to weak shared-memory models) by two axioms: EVENTUAL guarantees an update cannot stay invisible to infinitely many operations on the same object, so if updates stop replicas converge to the same state; THINAIR forbids out-of-thin-air values. Causal (and further sequential/linearizable) consistency are obtained by adding successively stronger ordering axioms (POCV/POCA, then COCV/COCA) on top of it, so eventual consistency is strictly weaker than causal consistency. First given a formal definition in MSR-TR-2013-39 (2013).
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.
Per-object (per-key) causal consistency: causal consistency restricted to a per-object happens-before order hbo = ((so ∩ ob) ∪ vis)+, as described by Burckhardt, Gotsman, Yang & Zawirski (POPL 2014) and Viotti & Vukolić (ACM Computing Surveys 2016, §3.9). In Burckhardt's framework it is eventual consistency (EVENTUAL+THINAIR) plus the per-object ordering axioms POCV/POCA, whereas (cross-object) causal consistency additionally imposes the stronger COCV/COCA. Hence it sits strictly between eventual consistency (weaker) and causal consistency (stronger).
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.
An extension of the DeNovo coherence protocol that lifts DeNovo's restriction to structured synchronization and supports arbitrary synchronization — including non-blocking algorithms — without writer-initiated invalidations. It relies on reader-initiated self-invalidation combined with synchronization read registration and hardware backoff, and adopts the standard data-race-free memory model of C++/Java, which defines sequentially consistent semantics for data-race-free programs; sequential consistency is used as the correctness criterion for synchronization accesses. It thereby guarantees sequential consistency for data-race-free programs while broadening the synchronization constructs DeNovo can support.
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 C/C++ memory model as of C++17. It narrows release sequences relative to C++11/14: a release sequence is continued only by read-modify-writes, no longer by later relaxed stores of the same thread, so a pattern that synchronised under C++11/14 stops synchronising. It keeps the (broken) C++11 seq_cst and leaves the thin-air problem unresolved. Behaviourally it is therefore strictly weaker than C11/C++11 — it admits a non-synchronising outcome C++11 forbids while forbidding nothing C++11 allows. Mechanised by the cpp17.cat model (vendored from gonzalobg/cpp_memory_model; herd7-checked). Its relationship to C++20 turns on where exactly the release-sequence change landed in the standard — the cpp_memory_model models attribute the narrowing to C++17 while WG21 P0982 is a C++20 paper — so no direct C++17↔C++20 edge is drawn; see the C11↔C++17 litmus README.
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.
The ARMv8 instance of the unified declarative transactional framework of Dongol, Jagadeesan & Riely (POPL 2018), which adds transactions to a relaxed-memory architecture parametric in the base model (the paper instantiates it at SC, TSO, ARMv8 and PPC/POWER). It treats relaxed memory as a restricted distributed system with no global real-time clock and uses observation-based 'observable serializability' rather than strict serializability, admitting flexible STM-style abort. A genuine sibling to the Chong-Sorensen-Wickerson TM cluster with a distinct construction and authorship. The added transactional axioms only constrain transactional events, so on programs with no transactions this instance coincides with ARMv8 by construction.
An axiomatic extension of the ARMv8 memory model with (unofficial) transactional-memory rules based on a proposal considered within ARM Research: strong isolation, implicit transaction fences, transaction ordering, and RMW cancellation. ARM hardware did not support TM, so the model could not be tested directly, but the generated test suites revealed a TxnOrder violation in an RTL prototype. The paper's headline result is that combining any reasonable TM extension with the recommended ARMv8 spinlock makes lock elision UNSOUND (Example 1.1): a critical region can begin executing after the lock is observed free but before it is taken. No behavioural-equivalence edge to ARMv8 is asserted; the fix proposed is to append a DMB to the lock() implementation, after which lock elision becomes sound.
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.
An axiomatic formalisation of the C++ transactional-memory technical specification (relaxed and atomic transactions) layered on the repaired C11/C++ memory model of Lahav et al. (RC11), chosen because it supports correct compilation to Power. The extension makes two amendments to the base model: the definition of a data race is unchanged, and conflicting transactions synchronise via a transaction order folded into happens-before. On programs without transactions the model coincides with its RC11 base. The authors prove atomic transactions are strongly isolated, that race-free programs with no non-SC atomics and no relaxed transactions enjoy 'transactional SC', and (up to a bound) that C++ transactions compile soundly to x86, Power, and ARMv8. Handling of programmer-invoked abort() is left to future work.
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.
An execution criterion that forbids out-of-thin-air (OOTA) results by preserving a syntactic notion of dependency, requiring the union of (syntactic) dependency and reads-from to be acyclic. A strictly weaker guarantee than load-store ordering, targeted at Java-like languages in which every memory access can contribute to OOTA. Implemented in the LLVM compiler; the authors measure a 3.1% average (17.6% worst-case) overhead on SPEC CPU2006 for a prototype dependency-preserving compiler.
An execution criterion that forbids out-of-thin-air (OOTA) results by preserving load→store ordering, requiring the union of sequence-before and reads-from to be acyclic. Targeted at C/C++-like memory models in which racing operations are explicitly labelled atomic, so it constrains only relaxed atomics; the authors implement it in the LLVM AArch64 backend and report no average overhead (6.3% worst case) on concurrent data-structure benchmarks. A strictly stronger guarantee than the paper's dependency-preserving criterion.
The PPC (POWER) instance of the unified declarative transactional framework of Dongol, Jagadeesan & Riely (POPL 2018), which adds transactions to a relaxed-memory architecture parametric in the base model (the paper instantiates it at SC, TSO, ARMv8 and PPC/POWER). It treats relaxed memory as a restricted distributed system with no global real-time clock and uses observation-based 'observable serializability' rather than strict serializability, admitting flexible STM-style abort. A genuine sibling to the Chong-Sorensen-Wickerson TM cluster with a distinct construction and authorship. The added transactional axioms only constrain transactional events, so on programs with no transactions this instance coincides with POWER by construction.
An axiomatic extension of the IBM POWER memory model with rules for its hardware transactional memory. Successful transactions create cumulative memory barriers at their boundaries, contain an integrated barrier ordering observed writes before transactional writes, and appear atomic to other threads (strong isolation). The additions only constrain transactional events, so on programs without transactions the model coincides with POWER. Validated by synthesising forbidden litmus tests run 10M times each on an 80-core POWER8 machine, none of which were observed. The work also flagged an ambiguity in the Power TM specification and showed that coalescing transactions is unsound in Power.
A standard database / distributed transactional consistency model, given a declarative (acyclicity-axiom) semantics by Raad, Lahav & Vafeiadis together with a simple lock-based reference implementation built on top of the release-acquire (RA) fragment of the C/C++11 memory model and proved sound and complete against the declarative specification — the first treatment of PSI as an STM model over a weak-memory programming language. PSI weakens serializability, letting conflicting transactions without a write-write conflict commit in parallel; it permits the write-skew anomaly and the long-fork anomaly (the latter forbidden under Snapshot Isolation). The authors also give Robust PSI (RPSI), extending PSI to mixed transactional/non-transactional code with its own sound-and-complete RA implementation.
Persistent-memory model layering buffered epoch persistency on top of the TSO / x86-TSO consistency model. It adds an orthogonal persist-order axiom (what survives a crash on non-volatile memory) rather than reordering reads/writes: the crash-free behaviour coincides with TSO, while persistency governs the order in which store-buffered writes reach NVM. Given both operationally and declaratively.
The SC instance of the unified declarative transactional framework of Dongol, Jagadeesan & Riely (POPL 2018), which adds transactions to a relaxed-memory architecture parametric in the base model (the paper instantiates it at SC, TSO, ARMv8 and PPC/POWER). Following Alglave et al.'s vocabulary it treats relaxed memory as a restricted distributed system with no global real-time clock, and replaces strict serializability with an observation-based 'observable serializability' criterion (a committed-transaction order need only respect the observable coherence and causal orders), admitting flexible STM-style abort. A genuine sibling to the Chong-Sorensen-Wickerson TM cluster with a distinct construction and authorship. The added transactional axioms only constrain transactional events, so on programs with no transactions this instance coincides with SC by construction.
A flexible coherence interface for heterogeneous CPU/GPU systems in the DeNovo lineage that lets devices with diverse coherence properties and memory demands interoperate efficiently by directly translating between request types rather than forcing a single protocol on every device. It assumes a sequential-consistency-for-data-race-free (SC-for-DRF) consistency model, so on the race-free fragment it admits exactly the SC behaviours; the choice of coherence request type affects only performance, never the consistency guarantee. It is reported to reduce execution time by 16% on average (max 29%) and network traffic by 27% (max 58%) versus a hierarchical baseline.
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.
The TSO instance of the unified declarative transactional framework of Dongol, Jagadeesan & Riely (POPL 2018), which adds transactions to a relaxed-memory architecture parametric in the base model (the paper instantiates it at SC, TSO, ARMv8 and PPC/POWER). It treats relaxed memory as a restricted distributed system with no global real-time clock and uses observation-based 'observable serializability' rather than strict serializability, admitting flexible STM-style abort. A genuine sibling to the Chong-Sorensen-Wickerson TM cluster with a distinct construction and authorship. The added transactional axioms only constrain transactional events, so on programs with no transactions this instance coincides with (x86-)TSO by construction.
An axiomatic (herd7-style) extension of the x86-TSO memory model with rules for hardware transactional memory (Intel TSX). Transactions are treated as atomic units bounded by implicit fences (a committed transaction has LOCK-prefix ordering semantics) with strong isolation. The additions only constrain transactional events, so on programs without transactions the model coincides with x86-TSO. Validated by synthesising 'minimally forbidden' litmus tests that were run on four Intel TSX implementations (Haswell, Broadwell, Skylake, Kabylake) and never observed.
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.
First formalisation of the persistency semantics of the ARMv8 architecture, layering a persist-order axiom (what survives a crash on non-volatile memory) on top of the ARMv8 consistency model. The persist dimension is orthogonal to ARMv8's read/write reordering; the crash-free behaviour coincides with ARMv8.
A transactional persistency model giving the first formalisation of transactional semantics in the non-volatile-memory setting: it extends serialisability with an orthogonal persist-order axiom over durable transactions. Proven to compile correctly to PARMv8.
A timestamp-based operational concurrency model for the ARMv8 and RISC-V instruction sets. It computes allowed behaviours incrementally from thread-local conditions, executing instructions in program order (bar early writes) without branch speculation, giving a substantially simpler operational presentation than prior ARM/RISC-V operational models. It reworks the timestamp/promise approach of the C/C++ Promising Semantics with a new uniform treatment of dependencies, but targets ISAs rather than C/C++, so it is a distinct model. Proven equivalent in Coq (for finite executions) to the axiomatic ARMv8 and RVWMO models.
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.
The snapshot-isolation transactional consistency model — the default in many databases — given simplified, timestamp-free semantics by Raad, Lahav & Vafeiadis as two lock-based multiple-readers-single-writer (MRSW) reference implementations (one eager/prescient, one lazy) built over the release-acquire (RA) fragment of C/C++11 and proved sound and complete against the declarative (acyclicity-axiom) SI specification. SI permits only the write-skew anomaly and otherwise coincides with serializability; it is strictly stronger than Parallel Snapshot Isolation, forbidding the long-fork anomaly PSI allows. The paper also introduces Robust SI (RSI) for mixed transactional/non-transactional code, again with sound-and-complete RA implementations.
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 first formal relaxed-memory model for WebAssembly's shared-memory threads and atomics, and the basis of the model later folded into the Wasm specification. Built on the C/C++11 axiomatic model of Batty et al., it exposes only two access modes — unordered (unord) non-atomics and sequentially-consistent (seqcst) atomics — and, unlike C/C++11, carefully avoids undefined behaviour, giving racy accesses defined but weak (thin-air-permitting) semantics. It is deliberately not sequentially consistent (the authors argue no SC semantics can be given to memory growth) but is proven to guarantee Sequential Consistency for Data-Race-Free programs (SC-DRF), the same guarantee class as C11; the paper also shows the contemporary JavaScript model's SC-DRF claim was false and proposes two conditions, since adopted by TC39, that align JavaScript's SharedArrayBuffer semantics with Wasm's.
A rigorous concurrency model for the 'system semantics' of instruction fetch and instruction/data-cache maintenance in Armv8-A, capturing self-modifying code, program loading, dynamic linking and JIT patterns (Sec. 4-5). It extends the base Armv8-A user-mode concurrency (Flat) model with instruction-fetch events, a fetched-from (fetch-read) relation, and instruction-cache (IC) and data-cache (DC) maintenance events, showing that instruction fetches are more relaxed than data accesses and that even coherence for the fetched stream is not guaranteed without explicit IC/DC/ISB synchronisation. Given in both an operational (extending Flat) and a functionally-equivalent axiomatic style. On programs that perform no instruction fetch or cache maintenance it coincides with the base Armv8-A user-mode model (validated identical over the 8950-test Flat regression suite, Sec. 6); outside that fragment it admits additional executions arising from stale instruction caches.
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.
First formalisation of the persistency semantics of the Intel-x86 architecture, layering a persist-order axiom (what survives a crash on non-volatile memory) on top of the x86 (x86-TSO) consistency model. Given both operationally and declaratively, with the two shown equivalent. The persist dimension is orthogonal to x86's store-load reordering; the crash-free behaviour coincides with x86-TSO.
A denotational relaxed-memory model for a Java-like language that combines pomsets (Gischer 1988) with preconditions (Hoare-style logical formulae labelling events) to calculate semantic dependencies. It bans out-of-thin-air reads while supporting temporal-safety reasoning, all expected sequential compiler optimizations (including common subexpression elimination, unlike C11 relaxed atomics), and the sc-drf criterion. The model realizes multi-copy atomicity and compiles to x64 and Arm8 without extra fences on relaxed accesses, but is deliberately not implementable on non-MCA processors such as POWER and Armv7. It is the base model that Pomsets with Predicate Transformers / 'The Leaky Semicolon' (Jeffrey et al. 2022) extends to give a direct, compositional account of sequential composition; that later work's PwT-mca1 imposes the same reads-from-implies-order requirement (m7c) as PwP and is thus close to it, while its PwT-mca2 drops m7c and is a strictly weaker model new to the 2022 paper.
Cho et al.'s declarative Armv8 persistency model, which simplifies and fixes documented flaws in Raad et al.'s PARMv8. Formally, they prove (Thm 6.1) that PArmv8axiom is equivalent to SPArmv8, a strengthening of PARMv8, and (Thm 6.2) that it is equivalent to the operational PArmv8view. This axiomatic model has been reviewed by Arm engineers; the crash-free behaviour coincides with Armv8.
Cho et al.'s declarative Intel-x86 persistency model, which simplifies and fixes documented flaws in Raad et al.'s Px86. Formally, they prove (Thm 4.3) that Px86axiom is equivalent to SPx86, a strengthening of Px86 that executes clflush synchronously, and (Thm 5.3) that it is equivalent to the operational Px86view. The crash-free behaviour coincides with x86-TSO.
A simpler and stronger sequentially-consistent persistency model introduced alongside PTSOsyn: it layers an epoch-persistency dimension over SC rather than TSO, so the crash-free behaviour coincides with sequential consistency. Khyzha & Lahav develop a sound mapping from PSC down to x86 and establish a data-race-freedom guarantee giving programmers a safe programming discipline for persistent memory.
An operational x86-TSO persistency model with synchronous explicit persist operations and per-cache-line persistence buffers, developed as a developer-friendly reformulation of Raad et al.'s Px86, whose persists are asynchronous. Khyzha & Lahav prove PTSOsyn equivalent, in terms of reachable states, to Px86, so its crash-free consistency coincides with x86-TSO while persistency is governed by synchronous per-line persists that are closer to programmers' intuition.
The first operational persistency model for Armv8, part of Cho et al.'s view-based revamp of hardware persistency. It extends the Armv8view consistency model with persistency views over the store/persist history in the same uniform operational style as Px86view, differing in the ordering imposed by flushes and the absence of a strong-flush primitive. Proven equivalent (mechanised in Coq) to the axiomatic PArmv8axiom; the crash-free behaviour coincides with Armv8.
The first operational, view-based persistency model for Intel-x86, part of Cho et al.'s revamp of hardware persistency. Each thread tracks views over the store/persist history in a uniform operational style, extending the x86view consistency model with persistency. Proven equivalent (mechanised in Coq) to the axiomatic Px86axiom, and thereby to Raad et al.'s Px86 modulo the flaws Cho et al. repair. The crash-free behaviour coincides with x86-TSO.
A Herd-style axiomatic concurrency model extending the base Armv8-A user model with virtual-memory and address-translation events (T translation-reads, TLBI, TE, ERET, MSR, DSB) and new relations (trf, tfr, iio, tob, obtlbi, ctxob, wco), in Strong and Weak variants, with soundness/metatheory proofs. For programs with stable, injectively-mapped address spaces it collapses exactly to the base Armv8-A user-mode concurrency model (Sec. 6); outside that fragment it admits additional executions arising from translation-table manipulation and TLB maintenance.
Extends the Px86 (Px86sim) persistency model of Raad et al. to cover the full range of Intel-x86 memory types (uncacheable, write-combined, write-through, write-back) and non-temporal stores (MOVNT), together with their subtle interactions, validated by extensive testing on real Intel-x86 hardware. PEx86 is a conservative extension of Px86sim: for programs restricted to regular stores on write-back memory it coincides with Px86, differing only in a minor divergence over flush/flushopt ordering that PEx86 drops to follow the updated Intel manual. Given both operationally and declaratively.
A compositional, denotational relaxed-memory model based on pomsets with predicate transformers (PwT), extending Pomsets with Preconditions (Jagadeesan, Jeffrey & Riely, POPL 2020) with families of predicate transformers so that the denotation of a sequential composition S1;S2 is computed directly from those of S1 and S2. It bans out-of-thin-air behaviour (verified in Coq) while permitting common compiler and hardware reorderings, and defines two instances: PwT-C11 (inherits RC11's top-level axioms; lowers to any C11-supported architecture) and PwT-mca (fully compositional, with optimal lowering to multi-copy-atomic architectures such as Arm8). Despite the overlapping author set, this is the pomsets/preconditions lineage rather than the Well-Justified Event Structures (Jeffrey & Riely 2016) event-structures line; the paper states no formal ordering to WJES.
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.
RC11 updated to account for the C++17 release-sequence definition: like RC11 (repaired seq_cst, no out-of-thin-air via acyclic(po|rf)), but a release sequence is continued only by read-modify-writes, not by later same-thread relaxed stores. It is therefore strictly weaker than RC11 (it admits a non-synchronising outcome RC11 forbids) and strictly stronger than C++17 (it keeps the no-thin-air axiom C++17 lacks). Mechanised by the rc17.cat model (vendored from gonzalobg/cpp_memory_model; herd7-checked).
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.
The memory model of NVIDIA's Tile IR, a tile-based virtual ISA introduced with CUDA 13.1 (2026) as a lower-level compilation target for tile programs (e.g. the experimental Triton-to-Tile-IR backend). This axiomatic, scoped model defines coherence order, happens-before, program order, 'morally strong' accesses, reads-from and token-based dependency ordering, with scopes tile_block/device/sys; global memory accesses are unordered by default. NVIDIA's documentation states the axioms and relations are intended to be a strict weakening of the PTX model. Vendor documentation only — no peer-reviewed formalisation or proof.