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 — litmus only (thin, dashed)

Weaker evidence, and a genuine caveat. A single litmus test whose outcome is allowed by B and forbidden by A shows that A is not stronger-or-equal to B — but on its own it does not establish the converse (that every B behaviour is an A behaviour). Such an edge may actually be incomparable: we may simply not have found a separating litmus test the other way. Read these arrows as "weaker as far as we can tell", not as proven.

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. Equivalent and compilation edges are all literature-backed.

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;
• 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. There are three independent filters and they combine: a model is shown only if it passes the category filter and the language filter and the property filter. 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.

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

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.

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.

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 puts its id in the URL (e.g. #RC11); copy or share that URL to link straight to a model. The copy-link button in the detail panel does this for you.

Data & sources

The classification draws on the survey by Moiseenko, Podkopaev & Koznov — A Survey of Programming Language Memory Models — and on the primary paper for each model, cited with a DOI or link in that model's detail panel. 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