Relaxed Memory Model Zoo

Help & guide
← Back to the map
Work in progress

This site is under active development. The set of models, the ordering edges between them, the litmus tests, and the per-model property data are incomplete and may change. Treat every classification as provisional and verify it against the cited papers before relying on it.

The zoo is an interactive map of hardware and programming-language memory models, ordered by the inclusion of their allowed execution behaviours — inspired by the Complexity Zoo. This page explains how to read the map and use its controls.

Overview

Each box on the map is a memory model — a definition of which outcomes a concurrent program may produce. Models are arranged vertically by strength: a model higher up allows fewer behaviours (it is stronger, easier to reason about), while a model lower down allows more behaviours (it is weaker, but admits more hardware/compiler optimisations). Arrows between boxes record how two models relate.

Click any box to open its details in the right-hand panel. Use the filters in the top-right to narrow the map to a kind of model, a programming language, or a set of formal properties.

Reading the map

The vertical axis is strength. The strongest model — Sequential Consistency (SC) — sits at the top; the weakest baseline — per-location Coherence — sits at the bottom. Faint horizontal bands label the tiers, from Strongest (SC) down to Baseline coherence.

The horizontal position within a tier carries no meaning of its own; nodes are only arranged left-to-right to minimise the number of crossing edges.

The core reading rule for an arrow A → B is: B allows strictly more behaviours than A (B is the weaker model). Other arrow styles encode other relationships — see Relations below.

Node types & colours

A box's colour indicates what kind of model it is:

A small sub-label under the abbreviation shows a representative architecture or language for the model where one applies.

Relations between models

Edges are typed and colour-coded; the same legend appears in the sidebar on the map. For an edge drawn from A to B:

Strictly weaker — A → B
B allows strictly more behaviours than A; every behaviour of B is also a behaviour of A, but not vice versa.
Equivalent — A ⋯ B
A and B allow the same set of behaviours (they may differ only in formulation, mechanism, or — as noted on the edge — some orthogonal detail).
Compiles correctly to — A → B
Programs written under A can be compiled to B while preserving their semantics (a soundness-of-compilation relation, not a strength relation).
Incomparable — A ⋯ B
Neither model's behaviours contain the other's; each allows something the other forbids.

Hover or open a model to read the exact justification for each of its edges in the detail panel. Some edges carry one or more litmus tests that witness the relation.

Edge provenance — how strong is the evidence?

Every edge records the source of its evidence, because not all relations are equally certain. The detail panel shows a badge on each relation, and the map draws the two kinds of edge differently. This matters most for strictly-weaker edges:

Strictly weaker — literature (bold)
The containment is established (or claimed) in the primary literature, or holds by construction — for example because B is A with one relaxation added, or because a paper proves B's behaviours are a subset of A's. Strong evidence.
Strictly weaker — argued (thin, dashed)
A genuine strict order, but argued rather than mechanised. A single litmus test (allowed by B, forbidden by A) shows only that A is not stronger-or-equal to B; on its own it could not rule out incomparability. So these edges are never left at a one-sided test: the containment is established by an explicit model-level argument (for example the cross-ISA monotonicity argument that PSO ⊆ POWER), corroborated by the litmus sweep. The direction is not in doubt — the lighter arrow marks that the containment is argued and corroborated rather than proved by a cited theorem or holding by construction. (There are 7 such edges today, among them PSO→POWER, TSO→ARMv8, TSO→RVWMO.)

For incomparable edges there are two modes too:

Incomparable — litmus both ways
A concrete separating litmus test exists in each direction — the incomparability is directly witnessed.
Incomparable — literature
The incomparability is asserted in the literature (or rests on a reasoning-guarantee, transformation, or feature difference) rather than on a runnable program in each direction.

A third provenance, deduced, marks relations obtained by deduction over the rest of the graph (transitivity, or transport across an equivalence) rather than by a direct witness. A fourth, memalloy, marks edges whose verdict comes from a mechanical model comparison with the memalloy tool — it generates the distinguishing execution, or finds none up to an event bound (bounded-exhaustive); these are the scoped-GPU edges. Equivalent and compilation edges are otherwise literature-backed.

Edge evidence — was it run, or cited?

Provenance records an edge's source; a second, orthogonal badge records its evidence — how far it is actually verified — because carrying a litmus test is not the same as having run it. Each relation in the detail panel shows this as a second chip:

machine-run
A checker actually produced the distinguishing verdict — herd7, memalloy, a JVM run (jcstress), OCaml, or mordor/SMRD — at least on the decisive side. (40 of 145 edges, 4 of them via memalloy.)
cited
The verdict is taken from the primary literature — a stated theorem, the defining paper's own example, or a model no checker can build (thin-air outcomes, the classical Steinke–Nutt lattice, compilation-soundness results) — not executed here. (86 edges.)
by construction
Holds by definition: one model is an operational reformulation of the other. (19 of the 35 equivalent edges.)
deduced
Obtained purely by deduction over other edges (transitivity / equivalence transport). No drawn edge is merely deduced — deduction only fills the order's closure.

Model details

Clicking a box opens its detail panel, which contains:

Filtering

The controls in the top-right narrow which models are shown. The filters are independent and combine: a model is shown only if it passes every active one — the category, language, formalism, property, and publication-year filters — as well as any text in the search box. If a filter hides a model you have deep-linked to, the category filter is reset so the model remains visible.

Category filter — All / CPU / GPU

These three buttons are mutually exclusive. All shows every model; CPU restricts to hardware (non-GPU) models; GPU restricts to GPU / scoped models.

Language filter

The Language dropdown filters by the programming language a model targets. It is a multi-select: tick one or more languages and the map shows every model that targets any of them (an OR over your selection). A badge on the button shows how many languages are selected, and Reset clears them.

The many specific dialect names in the data (for example C++11, C++20, C11-variant, CUDA C++, Linux kernel C) are grouped into canonical languages — such as C / C++, Java, CUDA — each shown with a count of how many models target it. The original dialect strings are still listed verbatim on each model's detail panel.

Models that do not name a concrete language (most hardware models and several purely theoretical ones) are simply absent from the language facet and drop out when any language is selected.

Formalism filter

The Formalism dropdown filters by the representational style in which a model is specified, following the survey taxonomy of Su & Colvin, Weak Memory Model Formalisms: Introduction and Survey (Concurrency Comput. Pract. Exper. 38(2), 2026), §6. Like the language facet it is a multi-select with OR semantics, a count badge, and a Reset.

A model may carry more than one style when the literature formalises it both ways (x86-TSO, for instance, has both a mechanistic write-buffer form and an axiomatic one). Representation-agnostic or contested models — the abstract SC/TSO/PSO/RMO baselines, bare Coherence, the official Java Memory Model — are deliberately left unassigned and drop out when any formalism is selected, just like an unknown property cell.

Property filter

The Properties dropdown filters by the formal properties of a model, organised exactly as in Table 1/2 of Moiseenko, Podkopaev & Koznov's survey of programming-language memory models. Each field is ternary:

The fields are grouped as:

Multiple property selections all apply together (AND). A model is kept only if its value for every selected property is known and matches; models with a grey (unknown) value for a selected property are dropped, as are models not yet characterised at all.

Where the values come from. 29 of the 101 models take their property vector directly from the survey's Tables 1–2 (survey-sourced); the other 72 — raw hardware, the GPU/scoped family, C++17/20, RC17, IMM, and the classical Steinke–Nutt lattice — are author-extrapolated from established semantics, with only the cells their definition pins down set and the rest left grey. Which is which is recorded per model (modelPropertyProvenance) and flagged in each model's detail panel under Property data as survey-sourced or author-extrapolated, so you can tell a grounded value from a derived one. Each model's own page (/models/<id>/) additionally lists its full known property vector under Properties, grouped as in the filter.

Column and cell provenance. Provenance is layered, finest wins. A few columns are drawn from outside the Moiseenko et al. survey and are recorded in propertyProvenance, marked in the filter with a dagger (†) whose tooltip gives the source: the Atomicity / multicopy-atomic column comes from Su & Colvin §2.4, and the Inverse roach motel column — moving a shared access out of a critical section — is not in the survey at all but from Poetzl & Kroening, Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models (2015), §4, which proves it sound for the SC-for-DRF execution model. Finer still, an individual cell — one (model, property) pair — may cite the specific paper that establishes that value for that model, recorded in modelPropertyCitations and shown inline on the model's page next to the value (e.g. every SC-preserving / SC-for-DRF model's Inverse roach motel cell cites Poetzl & Kroening 2015). This lets one property be sourced from different literature for different models.

Year filter

The Published control is a two-handle slider over the range of publication years in the data. Drag the lower and upper handles (or focus one and use the arrow keys) to keep only models published within that window; the label above the track shows the current range, and Reset restores the full span. Like the other filters it combines with them, so you can, for example, narrow to language models from the last decade that satisfy a chosen property.

Models with no recorded year fall outside any restricted window and drop out once the range is narrowed from its full extent.

Litmus tests

Some relations are backed by litmus tests — small concurrent programs whose allowed/forbidden outcomes witness the difference (or coincidence) between two models. When an edge has tests, its entry in the detail panel shows a litmus test(s) link; clicking it opens a viewer with the full test source.

For a strictly-weaker edge A → B, the test's distinguishing outcome is forbidden by the stronger model A and allowed by the weaker model B. For an incomparable edge, the test separates the two models in at least one direction. The viewer's header notes which relation the test witnesses.

Running a litmus test

The viewer shows each test's complete source, so you can reproduce it yourself. Most tests run in herd7, the memory-model simulator from the herdtools7 suite.

  1. Install herd7 (one-time), most easily via OCaml's package manager: opam install herdtools7, then eval $(opam env).
  2. Copy the source from the test viewer and save it to a file, e.g. test.litmus.
  3. Run it. Tests whose first line names a real architecture — X86, AArch64, ARM, PPC, RISCV — use herd7's built-in model for that architecture:
    herd7 test.litmus.
    Tests written in C (first line C …) use herd7's C11 model:
    herd7 -c11 test.litmus.

herd7 reports each named outcome on an Observation line:

Observation <name> Never 0 N
The outcome is forbidden — 0 of the N candidate executions match it. This is the verdict you expect from the stronger model.
Observation <name> Sometimes k N
The outcome is allowed — k of N executions match it. This is the verdict you expect from the weaker model.

A few tests can't be run in stock herd7 and are cited rather than executed live: the classical abstract models (SC, TSO, PSO, RMO, bare Coherence) need small custom cat models because herd7 ships only the named-hardware ones; thin-air (out-of-thin-air) behaviour can't be exhibited by herd7's execution model at all; and the GPU/scoped models, IMM, and Promising have no herd7 model and rely on their own verification artifacts. In those cases the viewer records the expected verdict and the source it is cited from.

Data & sources

The classification draws on two surveys and on the primary paper for each model, cited with a DOI or link in that model's detail panel. The property vectors and the strength ordering follow Moiseenko, Podkopaev & Koznov — A Survey of Programming Language Memory Models. The formalism taxonomy (§6) and the multicopy-atomicity / Atomicity column (§2.4) follow Su & Colvin — Weak Memory Model Formalisms: Introduction and Survey. Because the field is large and still evolving — and because this site is a work in progress — the ordering and property data are best regarded as a starting point for reading the literature, not an authority.

E. Moiseenko, A. Podkopaev, and D. Koznov. “A Survey of Programming Language Memory Models.” Programming and Computer Software 47(6), 439–456, 2021. doi:10.1134/S0361768821060050

Su and Colvin. “Weak Memory Model Formalisms: Introduction and Survey.” Concurrency and Computation: Practice and Experience 38(2), 2026.

← Back to the map