Relaxed Memory Model Zoo

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:

• CPU model — a hardware architecture (e.g. x86-TSO, ARMv8, POWER, RISC-V).
• Language model — a programming-language memory model (e.g. C/C++11, Java, OCaml).
• Formal / both — a theoretical model, or one spanning both hardware and language.
• GPU / scoped model — a scoped-synchronisation model for GPUs and heterogeneous compute (e.g. PTX, Vulkan, HRF).

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 6 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.

A fifth, kater, is the strongest of the mechanical ones and the narrowest. The kater tool decides whether one model is weaker than another by reducing the question to language inclusion between regular languages, so — unlike a search up to some event bound — a passing check is a proof that holds for executions of every size. What it proves is the containment half only. A strictly-weaker edge needs both halves, so these edges still carry the separating litmus test that makes the containment strict: kater says every behaviour of A is a behaviour of B, the litmus test says B has one A does not. Their arrows are drawn exactly like literature-backed ones — the claim on the map is the same claim, only differently established — and the badge in the detail panel is what tells them apart. (There are 6 such edges today; the queries that prove them live in the dataset repository under litmus/kater/ and re-run in its CI.)

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, kater, a JVM run (jcstress), OCaml, or mordor/SMRD — at least on the decisive side. (44 of 160 edges, 6 of them via memalloy and 6 via kater.)

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. (95 edges.)

by construction

Holds by definition: one model is an operational reformulation of the other. (21 of the 38 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:

• the model's name, abbreviation, year, and authors;
• tags describing its character (e.g. formal, operational, standard, scoped);
• a prose description;
• the hardware architectures and/or programming languages it covers;
• Cat model — whether the model is, could be, or cannot be specified in herd7's cat language, with the note and citation the verdict rests on;
• Relations — every edge to or from the model, each with a one-line justification and, where available, a litmus-test link;
• References — the papers and specifications the entry is based on, with DOI/links.

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, cat, 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.

• Axiomatic — declarative constraints on candidate execution graphs, e.g. the Cat language (§6.3). Used for x86-TSO, Arm, RISC-V, C/C++, IMM, the Linux kernel model, and most GPU models.
• Mechanistic — hardware-like abstract machines built from write/read buffers (§6.1), e.g. x86-TSO and the buffered/operational-approach models.
• Operational — step-based abstract machines using timestamped messages, promises, or views (§6.2), e.g. the Promising semantics and the operational reformulations of RC11/the JMM.
• Event structures — event structures and pomsets that encode several executions at once (§6.4), e.g. Weakestmo, MRD, and well-justified event structures.
• Reordering — program transformations / instruction reordering over a sequentially consistent baseline (§6.5).

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.

Cat filter — is the model written in cat, could it be, or can it not be?

The Cat dropdown filters by whether a model is expressible in cat, the domain-specific language of the herd7 simulator introduced by Alglave, Maranget & Tautschnig (Herding Cats, TOPLAS 2014). A cat model fixes a candidate execution — events with program order po, reads-from rf and coherence co — and accepts or rejects it with acyclicity, irreflexivity and emptiness axioms over relations built from those. cat is the de-facto lingua franca for machine-readable memory models, so “does this model have a cat model?” is a practical question: it decides whether you can run a litmus test against it. Every model in the zoo carries exactly one of three statuses, so the facet partitions the dataset:

• Specified in cat (25 models) — a cat model exists and is named in the note: herd7's own catalogue (aarch64.cat, ppc.cat, riscv.cat, rc11.cat, …), the zoo's litmus/models/ tree, the kernel tree's linux-kernel.cat, or the model's defining artefact. Also counted here is a model proved to allow exactly the behaviours of an existing cat model — Promising-ARM, for instance, is operational but Coq-proved equal to aarch64.cat and riscv.cat.
• Expressible in cat (67 models) — no cat model is published, but the model's allowed behaviours are a predicate on a single candidate execution, so one could be written. This covers the declarative models given as Coq axioms or inference rules (IMM, the DJR transactional instances, snapshot isolation), the operational models with a proved declarative counterpart (ORC11, the view-based persistency models), the prose-specified GPU models, and the classical Steinke–Nutt lattice. Where the gap is herd7's event vocabulary rather than cat's expressiveness — persistency models need crash and persist events — the note says so.
• Not expressible in cat (14 models) — the verdict is not a per-execution predicate at all. The Java Memory Model validates an execution against a sequence of committing executions; the Promising semantics certifies a promise with a future thread-local execution; the event-structure and pomset models (Weakestmo, MRD, sMRD, CSRA, WJES, PwP, the Leaky Semicolon) justify behaviour across conflicting executions or compute it denotationally over program syntax; RAO and the speculation calculi define behaviour by rewriting derivations. Two more fall outside for a different reason: real-time causal consistency appeals to wall-clock intervals, and eventual consistency to a liveness property over infinite executions — neither is in cat's vocabulary.

This axis is about the specification language, not model strength: a “not expressible” verdict is a statement about cat, and is usually the point of the model in question — the thin-air-free models are hard to state in cat precisely because per-execution axioms cannot see the dependency structure they rely on.

Where the verdicts come from. Each model's detail pane (and its own page) shows the status, a one-line justification, the citation it rests on, and a second chip recording how the cell was decided: cat file identified (19) — a concrete cat model was located and named; cited (25) — the primary literature states the claim, whether an equivalence theorem, the authors' own cat mechanisation, or the obstacle that rules cat out; or author-extrapolated (62) — a judgement from the model's definitional style, where no source addresses the cat question directly. The data lives in catSupport in models.json.

Provenance filter — which relations are proved, run, or cited?

The Provenance dropdown is the one filter here that selects relations rather than models: every node stays on the map, and only the edges known the selected way are drawn. Use it to see the shape of the evidence — which parts of the order are decided by a tool, which are witnessed by a program that was actually run, and which rest on a citation. The five values are the provenances above, and its counts are over edges:

• literature — established or claimed in the primary literature, or holding by construction. The bulk of the graph.
• litmus · herd7 (6 of them strictly-weaker) — carried by litmus tests that herd7 actually runs in the dataset repository: a separating program in each direction for an incomparable edge, or a one-sided witness plus a model-level containment argument for a strictly-weaker one.
• memalloy (6 edges) — a mechanical model comparison that generated the distinguishing execution, or found none up to an event bound. Mechanical, but bounded.
• kater · proved (6 edges) — decided by language inclusion, with no bound at all, so the containment holds for executions of every size. For a strictly-weaker edge that is half the claim: the strictness still comes from the litmus witness, which is why these edges carry both.
• deduced — obtained from the rest of the graph by transitivity or by transport across an equivalence, rather than from a source of its own.

Selecting several shows their union. The filter combines with the model filters and with the edge-type legend, so kater plus the strictly-weaker arrow isolates exactly the containments that are proved. The data lives in each edge's provenance field in models.json; the queries and witnesses behind the mechanical ones live in the dataset repository under litmus/.

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:

• any — do not filter on this property (the default);
• yes — keep only models that satisfy it;
• no — keep only models that do not satisfy it.

The fields are grouped as:

• Compilation — whether the model has an optimal compilation mapping to x86, POWER, Armv7, Armv8.
• Reordering — whether each of the four store/load reorderings (Store→Load, Store→Store, Load→Load, Load→Store) is a sound transformation.
• Elimination — whether each of the four access-elimination transformations is sound.
• Other local — irrelevant-load elimination, speculative-load introduction, roach-motel reordering, inverse (reversed) roach-motel reordering, strengthening, trace-preserving transformations, common-subexpression elimination.
• Global — register promotion, thread inlining, value-range transformations.
• Reasoning — external DRF, coherence, no undefined behaviour, in-order execution, no out-of-thin-air.
• Atomicity — multicopy atomicity: every thread observes each variable's writes in one consistent order. Power and NVIDIA PTX are the canonical models that lack it. (Source: Su & Colvin, Weak Memory Model Formalisms: Introduction and Survey, 2026, §2.4.)

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 106 models take their property vector directly from the survey's Tables 1–2 (survey-sourced); the other 77 — 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.

Search

The Search box filters the map by free text, matched against each model's name, abbreviation, and description, and against its references — title, authors, venue, and year. Only models that match are shown, and the search combines with the filters above (a model must match the search and pass every active filter). Clear the box to drop the constraint.

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.

Reading a kater query

Relations with a kater provenance carry a second kind of source in the same viewer, chosen from the Source dropdown: not a witness but a proof obligation, in the input language of kater. A query is short — it includes the two models and states one inclusion:

include "../../kat/sc.kat"
include "../../kat/tso.kat"

assert tso::tso <= sc::sc+

Read the assert as every step TSO constrains is a path SC constrains — so TSO's axiom follows from SC's, every SC-consistent execution is TSO-consistent, and TSO is the weaker model. kater decides that by turning both sides into automata and testing language inclusion, which is why the answer needs no bound on execution size. A compilation query has the same shape with the mapping's premises added as assume lines.

To run one: docker pull genmc/kater, then make kater in the dataset repository, which re-decides every query in litmus/kater/queries/ against the pinned image. litmus/kater/README.md is the runbook, and litmus/kater/open/ holds the queries that do not pass, with the obstacle each one hits.

A query proves containment and nothing else. A strictly-weaker relation also needs a behaviour the weaker model allows and the stronger forbids — so these edges carry a litmus witness too, and the viewer lists both.

Navigation & links

• Pan by dragging the graph; zoom with the + / − buttons or the scroll wheel, and reset the view with ⌂.
• Theme — toggle light/dark with the button in the header; the choice is remembered.
• Deep links — selecting a model or an edge puts a target in the URL: a model's id for a box (e.g. #RC11), or #from-to for an edge (e.g. #TSO-ARMv8, in the direction the relation is stored). Copy or share that URL to link straight to the model or relation; the copy-link button in the detail panel does it for you. Loading such a URL, and the browser's back/forward buttons, restore the selection.
• Linking to several things at once — separate targets with commas to highlight a group: #SC,C11,RC11 lights those models and every relation between them, #SC-C11,MRD-C11 lights just those two relations, and the two kinds can be mixed. A list is taken literally — unlike a single model, which also brings in its neighbours. Build one by ⇧- or ⌘/Ctrl-clicking boxes and edges to add or remove them; a plain click still selects one thing.
• Sharing — the Share menu in the footer posts the page to LinkedIn, Mastodon, X, Bluesky, Hacker News, Reddit or email, or copies its link. On the map it shares whatever is currently selected, so a link to #SC,C11,RC11 travels with it. Mastodon has no single share address — it depends on your home instance — so that entry asks for yours the first time and remembers it.

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. The cat-specifiability column is assembled here rather than taken from a survey: each cell either names a concrete cat model, cites the paper that settles it, or is flagged as author-extrapolated. 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.

Citing the zoo

Cite the dataset rather than this page: it is the versioned artifact, and the map is one rendering of it. Ready-made citation metadata is published in Citation File Format alongside the data it describes, at /data/CITATION.cff. Most reference managers import it directly, and GitHub reads the same format.

The file is stamped with the version and release date of the dataset published with it — the same pair shown in the footer of this page — so a citation taken from it names exactly the snapshot you were reading. Cite that version; the data behind the map changes as models and relations are added or corrected. The dataset is released under the 3-clause BSD licence.

Individual claims are a separate matter: a model, an ordering edge or a property cell carries its own reference in the detail panel, and reusing one means citing that primary source too.

Something wrong or missing?

A misplaced model, an edge that should not be there, a missing model, a property cell that contradicts the paper it cites — please report it. The data lives on GitHub in christiankissig/rmm-zoo-dataset; open an issue there, or send a pull request. Corrections are as welcome as additions, and a correction that comes with its source is the most useful thing you can send.

Read the contributing guide first: it explains how the dataset is structured, what evidence a new model, edge or property value needs, and the invariants the consistency gate enforces. There are pull-request templates for each kind of change — adding a model, correcting a relation, adding litmus tests — that walk you through what to supply.

To follow the project, watch or star the dataset repository; the site that renders it is at christiankissig/rmm-zoo.kissig.org.