The Relaxed Memory Model Zoo

In a weak memory setting, memory accesses can become observably out of order: another thread can see them take effect in an order contradicting the order the program is written in. On machines that are not multi-copy atomic, it goes further still: two observer threads can disagree with each other about the order of the same two writes.

Reordering is the common case but not the only one. Eliminating a redundant access, forwarding a value into a register, and — at the pathological end — producing a value with no origin at all belong to the same family: things an implementation may do to your program that its text does not obviously permit. The example below shows how gcc 15.2 -O2 on x86-64 eliminates the first of two ordinary stores to the same variable:

1
2

x = 1;
x = 2;

1

movl    $2, x(%rip)

Which modifications an implementation may make is neither arbitrary nor a matter of cleverness — it is written down, in a memory consistency model.

A memory consistency model is the contract that binds a program to its execution. Adve and Gharachorloo call it “an interface between the programmer and the system”, one that needs a specification at every level of that interface — machine code as much as high-level language ^[3]. The contract reading is Adve and Hill’s: they re-define weak ordering as “a contract between software and hardware”, in which software agrees to formally specified constraints and hardware agrees to appear sequentially consistent to at least the software that obeys them ^[4].

The contract is between three parties: it tells the programmer what they may assume about what other threads can observe, the compiler which transformations are sound with respect to the desired target, and the hardware which reorderings and buffering it may perform.

Each party’s freedom is another’s obligation, which is why most of the Zoo’s property columns describe transformations — whether a reordering, an elimination or a value-forwarding step is sound under the model. A compiler writer reads such a column as the optimisations they may apply, a hardware architect as the reorderings the machine may perform, and a programmer as a guarantee they no longer have. The rest state guarantees outright: coherence, external data-race freedom, absence of undefined behaviour, multi-copy atomicity.

A model fixes the class of behaviours a program may be observed to have, not the behaviour it has. Almost every interesting concurrent program has many permitted outcomes, and the model draws the boundary of that set. This is why the natural ordering on models is set inclusion over behaviours, and why the unit of evidence is a single outcome that falls inside one boundary and outside another.

The contract is drawn at more than one boundary. A hardware model is the contract between an ISA and its microarchitecture; a language model is the contract between a language and its whole implementation — compiler, runtime and hardware together. These are different models, not two statements of one: RC11 says nothing about ARMv8’s store buffers, and ARMv8 says nothing about what a C++ compiler may do to a non-atomic access. What a running program actually gets is the composition of the two, and they compose only when someone proves the compiler’s mapping from one to the other sound. That proof is a relation between models rather than a part of either — which is why it appears in the Zoo as its own edge type: 25 compilation edges, and why, for instance, RC11 reaches hardware through IMM ^[5] rather than directly.

Not every node on the map is a contract someone signed. SC is a reference point nobody implements; causal consistency and the session guarantees come from distributed storage; snapshot isolation and its persistent variants come from databases. They earn their place by the same test the contracts do: each fixes a set of allowed behaviours precisely enough to be compared by inclusion, and the models that are contracts are positioned against them. That is the criterion for what belongs in the Zoo — anything whose allowed behaviours can be stated sharply enough to be ordered, with a published source to attribute it to.

Follow one program through all three. On the left, three statements with ordinary (non-atomic) accesses, in the order you wrote them. On the right, what actually gets executed — real gcc 15.2 -O2 output for x86-64, with directives and address setup elided:

1
2
3

x = 1;
int a = x;
y = a;

1
2

movl    $1, x(%rip)
movl    $1, y(%rip)

The load is gone. The compiler forwarded the stored value into the third statement, so the store to y no longer takes its value from x at all, and the dependency that ran load → store in your source no longer exists in the object code. Clang 20 does the same thing on AArch64: both str instructions take their value from the same register, and nothing separates them.

That transformation is the compiler exercising its half of the contract, and the language model is what says it may. Notably, it is also free not to: make those same accesses relaxed atomics and neither GCC 15 nor clang 20 forwards, even though C11 permits it. Implementations are frequently stricter than the contract requires — which is why a model’s guarantees, not any compiler’s behaviour, are what you have to reason against.

Now the third signatory. After forwarding, the object code is two independent stores, and whether another core can observe y == 1 while x is still 0 is no longer the compiler’s business — it is the hardware model’s. On x86-TSO it cannot: stores are not reordered with stores, so the order you wrote survives by accident. On ARMv8 or POWER, where store→store is relaxed, the second store may become visible first, and getting your order back costs an explicit barrier.

That single question — may store→store be reordered — is one of the 28 property columns (reorder_ss), and the reason TSO, PSO and ARMv8 are three different nodes on the map rather than one. What another thread finally observes is the composition of two permissions granted by two different documents: one the compiler took under the language model, one the CPU took under its own. Neither document alone predicts it.

The word doing the work in weak memory model is a comparison to sequential consistency ^[6], in which every execution is some interleaving of the threads’ program orders. SC is the model nearly everyone reasons with informally, and nearly nobody implements: store buffers, caches, speculation and ordinary compiler optimisations all violate it. Every model below SC in the map keeps part of that intuition and gives up the rest. What separates them is where they draw the line — which guarantees a programmer loses so that a store buffer, a cache or an optimisation can be kept.

Language models mostly recover the intuition conditionally rather than abandoning it: if your program is data-race-free, you are promised sequential consistency. What happens when it is not race-free is where the contracts genuinely diverge — undefined behaviour in C++ ^[7][8], a bounded safety guarantee in Java ^[9], races bounded in space and time in OCaml ^[10]. Two of the property columns, no_ub and edrf, track exactly this split.

For some of the mainstream language models, this contract is known to be defective. The C11/C++20 axioms fail to forbid out-of-thin-air values that no compiler and no CPU actually produce. A substantial share of the models in the Zoo exist to close that gap, and the disagreements between them are still live — the subject of its own section below. The map is, in that sense, a picture of a contract still under negotiation — not a settled taxonomy.

Wherever a model draws its line, a litmus test pins down one point on it: a small program with an outcome reachable only if a specific relaxation is allowed.

A litmus test is a tiny concurrent program — usually two to four threads, a handful of accesses — together with an initial state and a question about the final state. It is not a test in the software-engineering sense. It asks whether a particular outcome is permitted, and the answer is a property of the model, not of any one run.

Here is the one the SC → TSO edge rests on, exactly as it sits in the repository:

1
2
3
4
5
6
7

X86 SB
"Store buffering: store->load reordering. Forbidden under SC, allowed under TSO."
{ x=0; y=0; }
 P0          | P1          ;
 MOV [x],$1  | MOV [y],$1  ;
 MOV EAX,[y] | MOV EAX,[x] ;
exists (0:EAX=0 /\ 1:EAX=0)

Four parts: the architecture and a name; the initial state (x and y both zero); two threads, each storing to one location and then loading the other; and the condition — the outcome we are asking about. Here it asks whether both threads can read 0.

For both loads to return 0, each thread’s load must effectively happen before the other thread’s store — which requires the store to be delayed past the load. That is store→load reordering, and whether it is allowed is precisely what separates sequential consistency from TSO. Run the same file through herd7 ^[1] under the two models:

1
2
3
4
5

$ herd7 -model sc.cat     SB.litmus
Observation SB Never 0 3

$ herd7 -model x86tso.cat SB.litmus
Observation SB Sometimes 1 3

Never 0 3 means the tool enumerated three candidate executions and none satisfied the condition — the outcome is forbidden. Sometimes 1 3 means one of three did — it is allowed. A store buffer, which lets a store sit in a per-core queue while later loads proceed, is exactly the implementation that makes the second verdict true.

The same discipline extends past herd7 where it has to: the Java and OCaml edges run under a JDK and an OCaml runtime, the thin-air edges run under MoRDor ^[11]. A follow-up post will show how the same tests locate a real language implementation in the lattice, using Rust as the example and running under loom, Miri and real silicon.

One test, run under two models, yields two verdicts — and that pair is the witness for a relation in the graph.

In the Zoo, that separation is witnessed by a test shipped with the dataset wherever one exists. Take the store→store question the compiler example ended on, as the Zoo’s TSO → PSO edge states it, in the message-passing shape:

1
2
3
4
5
6
7
8
9

AArch64 MP
"Message passing with two plain stores. Store->store reordering."
{ 0:X1=x; 0:X3=y; 1:X1=y; 1:X3=x; }
 P0           | P1           ;
 MOV W0,#1    | LDR W0,[X1]  ;
 STR W0,[X1]  | LDR W2,[X3]  ;
 MOV W2,#1    |              ;
 STR W2,[X3]  |              ;
exists (1:X0=1 /\ 1:X2=0)

P0 writes the data x and then the flag y; P1 reads the flag and then the data. The condition asks whether P1 can see the flag set (1:X0=1) while still reading the data as stale (1:X2=0) — the message arriving before its contents. Run the same file under both models:

1
2
3
4
5

$ herd7 -model abstract-tso.cat MP.litmus
Observation MP Never 0 3

$ herd7 -model abstract-pso.cat MP.litmus
Observation MP Sometimes 1 3

Forbidden under TSO, allowed under PSO. Without such a program the claim would be an assertion about two papers rather than a fact about two models.

A model that does not constrain reordering tightly enough admits behaviours no implementation ever produces. The sharpest case is a value appearing that nothing in the program ever wrote. Batty et al.’s formalisation of C++11 ^[8] exposed it in the mainstream language models: the standard’s prohibition on out-of-thin-air reads was informal prose that resisted formalisation, so the model as written does not actually forbid such executions — a gap they later set out in full ^[14]. RC11 and the models after it exist to close it.

Start from the compiler example above. The compiler kept 1 in a register and reused it, deleting the load — and with it, the dependency that ran from the load to the store. That is an ordinary, desirable optimisation. It is also the root of the trouble: a syntactic dependency in your source is not a fact about the program’s semantics, and implementations are free to discover that it carries no information and remove it. Register caching and value forwarding are the plain cases; common-subexpression elimination and value-range reasoning do the same thing less visibly.

That freedom has a consequence for the specification. A model cannot simply decree “respect dependencies”, because it cannot say which ones are real without either forbidding those optimisations or reasoning about the semantics of the whole thread. The axiomatic C11/C++20 models therefore validate an execution by a weaker local condition — every read reads from some write — and that condition can be satisfied by a cycle that supports itself:

Both threads read 42, and both write 42 only because they read it. No instruction anywhere stores 42 unconditionally — the constant does not occur in the program except as the thing being tested for. Yet nothing in the C11 axioms rules the execution out. The value is invented out of thin air, and the literature’s name for the phenomenon is exactly that ^[15].

No compiler and no processor actually does this, so the specification is strictly weaker than every implementation of it. What it costs is formal reasoning: with thin-air values permitted, you cannot prove that a value your program never wrote cannot appear — fatal for security arguments and for compositional verification, and forbidding it turns out to cost real performance ^[16].

The models that close the gap are among the most interesting recent ones, and they disagree about how: the acyclic(po ∪ rf) axiom in RC11 ^[17], promised writes that a thread later certifies in Promising ^[18], alternative executions tracked to tell a real dependency from a false one in the event-structure models of Jeffrey and Riely ^[19] and Weakestmo ^[20], and modularly computed dependencies in MRD ^[21]. MRD is the one the Zoo’s thin-air edges are actually checked against, since herd7 cannot construct such an execution at all.

So the most important open question in the field is precisely the one the standard tool cannot exhibit.

I wrote the Zoo to make it possible to search over a space that is otherwise distributed across proceedings. The map filters by the language a model targets, by formalism style, by year, and by the property vectors from Moiseenko, Podkopaev and Koznov’s survey ^[12] — so “which models are thin-air-free, multi-copy-atomic, and support store→load reordering?” becomes a query rather than a literature review.

Cat specifiability matters for anyone mechanising. cat is the domain-specific language in which herd7 models are written ^[1] — a model is a handful of definitions over the standard relations (po, rf, co, fr, dependencies, fences) plus a few acyclicity or irreflexivity axioms over them, and herd7 turns that description directly into an executable checker. It is the closest thing the field has to a common notation. Each model is therefore classified as specified (a real cat model exists — 25 models), expressible (it could be written in cat, but nobody has — 62), or not-expressible (it cannot be stated in cat at all — 14, typically the operational and event-structure models, whose content is a stepwise construction rather than a predicate over a candidate execution). That column is a map of where the tooling stops, which is often exactly what you want to know before starting a mechanisation.

It also answers a question that comes up constantly on the verification side. A whole line of work is deliberately parameterised by the memory model, because that is how it buys generality. Instead of building on one model, these publications state their results for a class of models with assumed properties. The Zoo turns “does this algorithm apply to my model?” into a lookup. If the model is specified, the input the algorithm wants already exists. If it is expressible, the algorithm applies in principle and someone has to write the cat file first. If it is not-expressible, no amount of engineering will make that class of technique fit, and you need a different one. Read that way, the 25 / 62 / 14 split is a statement about the reach of an entire family of verification algorithms: 87 of the 101 models are within it, and 14 are structurally outside.

Everything so far relates published models to published models. One use case turns the dataset the other way round, and points it at a shipped implementation.

The litmus tests are not only evidence for the edges — they are a reusable instrument. Each one is a program whose outcome separates two named models, with the expected verdict on both sides written down. Port that program to a real language and run it, and the verdicts tell you which side of the edge the implementation falls on. The catalogue stops being a map of the literature and becomes a way of locating something real within the literature.

Rust is a good subject, because the question is genuinely open: it ships no Rust.cat, and core::sync::atomic is documented to follow the C/C++ atomic memory model, which is a statement of intent rather than a position in a lattice. In the follow-up post I will write about how I used the Zoo’s language-level tests on Rust atomics and probed the boundaries of loom, Miri, herd7 and real silicon. Spoiler: they did not agree on all behaviours.

The part worth borrowing is not Rust’s position relative to the Zoo but the method. Nothing about the procedure is Rust-specific: a lattice whose edges are defined by runnable tests turns “where does this implementation sit?” from an essay question into a finite, executable checklist, and any language with atomics and a checker to run them under can be located the same way.