A Contract says more than a Verdict

Rust’s memory model, litmus tests, and concurrency tools — towards code patterns correct by design

This post follows on from The Relaxed Memory Model Zoo, where I introduced the Relaxed Memory Model Zoo (the Zoo), a map of 101 published memory models ordered by the behaviours they admit, and litmus tests to support the judgements. I ran the litmus tests from the Zoo’s corpus through Rust the common concurrency tools Miri and loom. The search yielded a gap between the tooling and the “memory model” as documented. This may be fine today, as neither the compiler frontend as implemented today nor common target architectures will produce the bug, but any layer of the stack exhausting its liberties will make the gap bite.

Rust was designed as a memory-safe language, one that admits neither uninitialised reads nor use-after-free. Every allocation has one owner. A reference cannot outlive the value it borrows, and the compiler, in particular the borrow checker, rejects any program where it might. Two threads can share mutable memory only through types that implement the Send and Sync traits, which rules out data races at compile time too. For safe Rust this holds without exception. The borrow checker guarantees that a program with no unsafe code anywhere does not free memory that is still in use.

In unsafe Rust the picture is different: inside an unsafe block a program may dereference a raw pointer, call a function the compiler cannot check (Box::from_raw, which takes ownership back from a raw pointer, is one), or declare by hand that a type is safe to send between threads. The borrow checker no longer asserts memory safety there, giving the responsibility to the programmer. Unsafe code is a pillar of the Rust language. Vec, Arc, Mutex and the channels in std are all built on unsafe code that their safe interfaces hide. Safe Rust is safe only if every unsafe block underneath it keeps its promise.

Lock-free code relies heavily on unsafe Rust for a structural reason. A lock-free queue or stack lets one thread read a node while another unlinks it, with no lock to wait on and no reference count on every access. When the node may be freed depends on an atomic protocol at run time: a flag, an epoch, a hazard pointer. The borrow checker decides lifetimes at compile time, so it cannot express this. The node is held through a raw pointer (AtomicPtr<T>, *mut T), and freeing it is unsafe. Crates such as crossbeam-epoch and the hazard-pointer libraries exist to package the unsafe step behind a minimal controlled surface within the protocol. Arc contains one too.

At that point the safety argument has moved out of the type system and into the memory model. The free is sound only if the protocol’s atomics order it after every use of the node, and whether they do, depends on the memory orderings the programmer chose. The compiler accepts the program either way. Whether it should have is a question for the memory model, and for the tools Rust developers use to check unsafe code against it. (Why safe Rust cannot even state the racy programs that litmus tests usually start from is the subject of a section near the end.)

This matters more now than it did a few years ago. More and more code, concurrent code included, is written by AI agents, and an agent works towards whatever check it is given. A change that keeps every test green is, to an agent, a correct change, and as this post shows, a memory-ordering bug can keep every test green. When code arrives faster than anyone can review its memory orderings, a green run can no longer stand in for that review. What can stand in is an explicit contract the code is checked against, and patterns that are correct against it by design. That is what this post is after.

The Rust “memory model”

Rust’s memory model for atomics is borrowed from: core::sync::atomic follows the C++20 memory model, which Mara Bos’s Rust Atomics and Locks ^[1] explains for Rust programmers. This is the contract I hold code to in this blog post. This statement, however, is not a specification: it says nothing about the C++ model’s known defects, and Rust ships no Rust.cat for herd7, so its tools have nothing to check code against. ORC11, from the RustBelt line of work, is the nearest formal Rust model, built to prove unsafe libraries such as Arc sound; it is an idealised research model, and not what rustc promises.

There are two more contracts underneath. rustc hands atomics to LLVM, whose monotonic is C++’s Relaxed, and LLVM hands them to the hardware, whose specification allows it to reorder instructions. Each layer may do anything the layer above allows, so a program is only as safe as the weakest contract in the chain.

Here is flag-guarded reclamation cut down to two threads, with a use-after-free in it. Like every code block in this post it is a sketch, one column per thread; runnable versions are in the code samples.

1
2
3
4
5
6
7

// x, y: AtomicUsize::new(0);  p: *mut Payload, currently live
// T0                                   // T1
let r0 = x.load(Relaxed);               let r1 = y.load(Relaxed);
y.store(1, Relaxed);                    x.store(1, Relaxed);
if r0 == 1 {                            if r1 == 1 {
    unsafe { drop(Box::from_raw(p)) }       let _v = unsafe { (*p).field };
}                                       }

Open LB+UAF in the MoRDor playground

The bug needs a reordering which the contract, the C++20 memory model, allows. Each relaxed store goes to a different location from the load before it and does not depend on it, so a compiler, or a CPU, may move the store above the load (fig1). The result is still a correct compilation of the same program.

After the move, an ordinary interleaving reaches the use-after-free: both stores run, both loads read 1, one thread frees p and the other reads through it (fig2).

I ran both versions on a 13th generation Intel i7 and on an AWS Graviton3. The litmus harness witnessed (r0=1, r1=1) in the reordered program 200 times in 30 million runs on x86 and 7 times in 30 million on Graviton3, where the CPU’s own store buffering narrows the window. The program as written never produced it on either CPU. Under AddressSanitizer on x86, the reordered program reports a heap use-after-free immediately.

Also Miri sees the bug in the reordered source matching the execution. Over 8,192 runs of each version (64 runs under each of 128 seeds), 4 seeds hit undefined behaviour in the reordered program and none in the original (fig3). Miri interprets the source, not the compiled binary, so a move the compiler or CPU may make reaches Miri only if someone writes it into the source, as I did by hand. No developer can do that as a practice: it would mean writing out every reordering the contract allows and running each variant through CI.

Every layer allows the move, but none does yet

So who would make the move? Looking at each layer (tbl1):

On Arm, rustc 1.99 emits a plain ldr then a plain str, in source order and with no barrier: the compiler keeps the order but leaves the CPU free to reorder, and the Graviton3 CPU simply does not.

This matters to anyone shipping lock-free code, because a no in the last column may be true in current platforms, but not a promise about the future. Nothing in LLVM’s contract stops a future release from making the move, nothing in Arm’s stops a future core, and a port to RISC-V lands on a model that allows load buffering too. Then the program above frees memory under a reader without a line of it changing, after years of passing tests.

On the program as written, the tools agree with practice: loom passes, Miri runs clean on every seed, and neither CPU ever misbehaved. About today’s binaries that is the right answer. It is not an answer about the contract, and a green run reads as though it were both.

The fix is one word per access. Load the flags with Acquire and store them with Release, and (1, 1) is forbidden at every layer: by C++20, by LLVM, and by the Arm mapping, which then emits ldar and stlr. The code is then correct by design, against the contract, rather than by observation, against today’s binary. Getting there means knowing which moves the contract allows before something in the chain makes them, and I think that is the most useful thing a catalogue of memory models can give a working language like Rust

Litmus tests make the contract checkable

The Relaxed Memory Model Zoo orders published memory models by the behaviours they allow, and every edge in it is supported by a set of litmus tests: small programs whose outcome one model permits and the other forbids. Ported to Rust atomics, each test has two uses: 1) Checked against Rust’s specification, which tells us whether Rust allows the outcome. 2) Run under a tool, it shows whether the tool detects the outcome. In the following we look at the second use: the tests where a tool’s answer differs from the specification’s. The same tests are a regression suite for the chain: run against a new LLVM release or on a new core, they show which allowed moves it has started to make. Models are the contracts; litmus tests hold each layer to them.

Below we look at three concrete cases of such litmus tests twice: first to see how each is evaluated under the available tools, and second how each can lead to more robust code patterns.

1. Exhibit 1 Load buffering, the shape above: allowed by the model, but not produced in Rust nor in the concurrency tools today;
2. Exhibit 2 Relaxed message passing, a payload behind a flag: allowed by the model, and produced today on Arm;
3. Exhibit 3 IRIW with SC fences: forbidden by the model, but produced anyway by one of the concurrency tools, which reported undefined behaviour that could not happen.

Where execution and concurrency tools disagree

Running the compiled binary, in CI or a stress harness, shows what actually happens; loom is a testing framework, and Miri is an interpreter making one execution of the Rust Abstract Machine at a time. herd7 and MoRDor run nothing: they evaluate the specification, and are the reference for what the model allows. Most misreadings come from treating these as interchangeable.

Running the binary in CI covers only what it ran on

A CI run executes the binary a limited number of times, built by only a handful of compiler versions, on the few CPUs the pipeline has. An outcome it shows is real, but limited to the environment available to the CI pipeline. An outcome it never shows means “not here, not yet”.

loom proves nothing outside its own model

A loom test wraps the code in loom::model. Built with --cfg loom, the target crate uses loom’s replacements for std::sync, and loom runs the test again and again under its own scheduler. Each run is an interleaving: the threads’ operations taken one at a time, each thread in program order. loom does not reorder a thread’s operations. Its one concession to weak memory is that every atomic keeps a history of its stores, and a load may read an older store from that history instead of the latest one. That covers store buffering and relaxed message passing, where a load sees a stale value. It cannot cover load buffering, where a load reads a store that, in the interleaving, has not happened yet.

loom explores these interleavings and store choices systematically, pruning equivalent ones, and a failing test hands back a replayable schedule. But it runs neither your binary nor std::sync::atomic, and a passing test is weaker than it looks.

If loom is in your CI chain, a green run does not mean every concurrent execution was tested. It does not test:

• load buffering: a relaxed load reading a value another thread stores after its own load in program order. loom’s own load_buffering test ships #[ignore]d, and exhibit 1 shows what that hides;
• SeqCst accesses as SeqCst: they are modelled as AcqRel, so a failure loom reports there may be one Rust forbids;
• code that bypasses loom’s types: std atomics or locks reached directly run outside the model;
• schedules past the preemption bound, when LOOM_MAX_PREEMPTIONS is set.

Inside its model — acquire/release synchronisation, every interleaving up to the bound — loom is exhaustive, and code that never depends on load buffering stays inside it.

Miri stays inside the model without covering it

Miri interprets Rust’s intermediate representation, executing the Abstract Machine step by step and stopping at the first undefined behaviour. It runs real std::sync::atomic. Where the Abstract Machine is nondeterministic, started with seeds — which thread runs next, which store a relaxed load reads — Miri does not explore the choices; it makes one at random. So the question is which executions it can make.

For sequential semantics (provenance, alignment, initialisation, validity) Miri is as close as Rust has to an executable reference. For weak memory it promises much less. Its emulation follows Lidbury and Donaldson’s race detector for C++11 ^[2]: a scheduler with random preemption, and for each atomic its last 128 stores for a relaxed load to read back into. Every weak behaviour Miri produces is meant to be allowed; it does not try to produce all of them, and with no load→store speculation, load buffering is out of reach. Its source states the guarantee against C++11 and warns that it “may generate behaviours C++20 disallows”, because the design predates the SC repair; exhibit 3 is where that showed. For the tests here, an outcome Miri produces is a witness; one it never produces, across any number of seeds, is evidence, not proof. Unlike loom it runs SeqCst as SeqCst. Alongside sit a happens-before race detector and an aliasing checker, both below.

herd7 reads the contract and runs nothing

herd7 takes a litmus test and a cat model ^[3], enumerates the candidate executions, and reports which the axioms permit. Its answer is about the specification, not your compiler or CPU, which is why it settles load buffering and the RC11-versus-C11 split. Its Never is decisive, but only for the cat file it is given, and it ties every read to an actual store, so it cannot construct a thin-air execution: on thin air, herd7 is stricter than the specification it models.

MoRDor, the sMRD reference implementation, answers the same kind of question without cat files. Its models, C++20 and RC11 among them, are built in and named in each test’s assertion, and it derives the candidate executions from sMRD’s event structures, so its C11 and C++20 models do admit thin-air executions.

So there are two references, herd7 for what the model permits and running the binary for what one machine did, with two approximations between them: loom, narrower than Rust and systematic inside it, and Miri, inside the model by sampling. The most interesting facts below lie in the gap between an approximation and its reference.

The exhibits against the instruments

We look at three exhibits which put the contract, real executions and the tools in tension. Each shows a gap:

• In exhibit 1 the contract allows an outcome no compiler or CPU produces yet. The tools agree with today’s binaries; the risk is an upgrade or a port.
• In exhibit 2 the contract allows an outcome Arm produces today and x86 never does. Code tested on an x86 laptop and in CI can fail in production on Graviton, and Miri catches it only by chance.
• In exhibit 3 the contract forbids an outcome a tool produced anyway: a false alarm, not a missed bug.

Exhibit 1: load buffering, allowed but not happening yet

A developer wants confidence in a relaxed fast path and writes a loom test — rightly, since exhaustive search is what they want. The shape is load buffering:

1
2
3
4
5

// T0                              // T1
let r0 = x.load(Relaxed);          let r1 = y.load(Relaxed);
y.store(1, Relaxed);               x.store(1, Relaxed);

assert!(!(r0 == 1 && r1 == 1));    // "both can't read 1 — nothing wrote yet"

Open LB in the MoRDor playground

loom finds nothing and goes green on every CI run. Yet (1, 1) is allowed, because C++20 permits load→store reordering of relaxed accesses. loom does not explore load buffering, as its documentation says; Miri does not emulate the speculation, so it cannot produce it from this source; and neither CPU produced it. Only herd7, consulting the model, answers. The mistake is not using loom but reading the loom test passed as cannot happen.

The opening program is this shape with consequences: LB+UAF, flag-guarded reclamation. The stores stay unconditional, so it is plain load buffering, not a thin-air cycle; the guards sit on the effects. As the opening showed, the use-after-free does not happen in any binary I tested, Miri reports it once the source is rearranged (fig3), and more seeds do not help, since -Zmiri-many-seeds samples interleavings of the same source, not other arrangements of it. MoRDor, asked about the model, produces it at once: under C++20, two of the seven executions it enumerates carry the use-after-free, both with (1, 1); under RC11, none do. Acquire loads alone are not enough under C++20, since a relaxed store read by an Acquire load creates no synchronisation, and the use-after-free remains (playground). Release stores with Acquire loads leave one execution, with no undefined behaviour (playground).

Miri’s README recommends loom where atomics get complicated, and loom’s documentation says it skips load buffering. Follow both and you miss exhibit 1, where the two blind spots coincide.

Exhibit 2: relaxed message passing, which Arm does today

A developer publishes a payload behind a flag and wonders whether Release/Acquire is needed:

1
2
3
4

// T0                              // T1
data.store(42, Relaxed);           let f = flag.load(Relaxed);
flag.store(1, Relaxed);            let d = data.load(Relaxed);
// (f, d) == (1, 0): the flag is seen, the payload is stale

Open MP+rlx in the MoRDor playground

So the developer weakens the memory order to Relaxed, and tests it on x86 and under cargo miri test in CI, never see the stale read, and ships it to Graviton. On x86 it cannot happen: the hardware keeps stores in order and loads in order ^[1], and the harness never saw it in 10 million runs. Arm does not, and on Graviton3 the same harness saw (1, 0) 4,761,020 and 1,954,952 times in two runs of 100 million. No amount of x86 testing could have shown it. The standard library shipped this shape in Arc::get_mut (again below).

Miri could have caught it: its model allows the stale read and can produce it. But it samples, and this outcome is rare enough to need many iterations or -Zmiri-many-seeds. Hence the asymmetry worth internalising: an outcome Miri shows you once is a witness that the model allows it; an outcome Miri never shows you is not proof of anything. With a non-atomic payload the race detector decides instead, on every run (see below).

Exhibit 3: IRIW with SC fences, forbidden by the model, but allowed by one of the tools

Two writers (T0 and T1), and two readers (T2 and T3) that load both locations in opposite orders with an SC fence between:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

// x, y: AtomicUsize::new(0)
// T0                              // T1
x.store(1, Relaxed);               y.store(1, Relaxed);

// T2                              // T3
let r1 = x.load(Relaxed);          let r3 = y.load(Relaxed);
fence(SeqCst);                     fence(SeqCst);
let r2 = y.load(Relaxed);          let r4 = x.load(Relaxed);

// (r1, r2, r3, r4) == (1, 0, 1, 0): T2 saw x written first, T3 saw y first

Open IRIW+Fsc+Fsc in the MoRDor playground

May the readers disagree? Original C11 says yes; RC11’s repair ^[4], adopted by C++20, says no, and herd7 confirms that the model Rust documents sides with RC11. None of the CPUs, I ran the litmus tests on, can show the outcome: x86 and ARMv8 are multi-copy-atomic, so the silence is structural. loom runs SeqCst as AcqRel and is not the tool to ask. Miri’s view was wider than the contract: its emulation did not respect C++20’s fix for SC fences, so it could produce the forbidden disagreement and report undefined behaviour in correct code, until fixed in late 2024 (rust-lang/miri#2301). It fails loudly rather than silently, but a tool can be wrong about the contract in either direction.

Where Rust sits in the Relaxed Memory Model Zoo

Reading the position off the map:

1. Strictly weaker than SC. Relaxed SB produces (0, 0) — exhaustively, by witness, and on silicon (6,000 times in 1M runs on x86, 160,000 in 1M on Graviton3).
2. The full C11 acquire/release hierarchy, and multi-copy-atomic. Message passing becomes forbidden with Release/Acquire, and coherence holds for relaxed accesses. Release/acquire also makes causality carry across threads, which the WRC (write-to-read causality) test checks:

   1 2 3 4 5

   // T0 // T1 // T2 x.store(1, Relaxed); let r1 = x.load(Relaxed); let r2 = y.load(Acquire); y.store(1, Release); let r3 = x.load(Relaxed); // (r1, r2, r3) == (1, 1, 0) is forbidden

   T1 sees T0’s write and then raises a flag; if T2 sees the flag, it must also see T0’s write. x86 and ARMv8 give this for free, because a store becomes visible to all other cores at once. POWER and ARMv7 can show a store to some cores before others, so there the guarantee costs a cumulative barrier before the release store (lwsync on POWER, dmb on ARMv7), which the compiler emits for Release.
3. RC11’s SC repair, not original C11’s — exhibit 3.
4. But C++20’s thin-air gap. LB and LB-OOTA are allowed by the letter of the model and forbidden by RC11’s no-thin-air axiom, which C++20 did not adopt. That is the RC11 → C++20 edge.

No real compiler or CPU produces thin-air values; the gap is between Rust’s formal model and its practice. ORC11, from Dang, Jourdan, Kaiser and Dreyer ^[5], the model used to prove Rust libraries sound, sits on the thin-air-free RC11 side of the gap by construction. The four models and the instruments fit on one screen of the map:

So, what does a clean Miri run mean then?

Most developers meet Miri through its aliasing checker: Stacked Borrows ^[6] by default, Tree Borrows ^[7] behind -Zmiri-tree-borrows. cargo miri test is the de facto oracle for undefined behaviour, but Rust has no ratified aliasing model either, and a clean run read as this unsafe code is sound comes apart from real Rust in three ways.

Miri is stricter than the compiler you ship on. A Stacked Borrows error says the program breaks a proposed rule, not that any rustc miscompiles it — worth fixing, but not a bug on today’s toolchain. The two models also disagree: on its authors’ corpus, Tree Borrows rejects 54% fewer test cases than Stacked Borrows, so a verdict can turn on a CI flag.

Miri is also more permissive than the model Rust will end up with. Its README marks both models experimental and expects the eventual model to be stricter than Tree Borrows. A green run describes one proposal at one point in time. The verdict may change, even though the program hasn’t.

And the aliasing checker inherits Miri’s sampling. It inspects only the executions the scheduler produced: a violation on a rare interleaving falls under exhibit 2’s asymmetry, and one needing an execution Miri does not build from the source, as in exhibit 1, is unreachable.

Safe code with no unsafe beneath it gives Miri nothing to find. For unsafe code, run under both aliasing models and read as a statement about today’s proposal, it is the best evidence Rust has today.

Using the Zoo to turn a blind spot into a mechanism

Each exhibit leads, through the corner case it tests, to the model on either of its sides. And, we get a different value in each case.

Exhibit 1 again: load buffering leads us to enumerate, not sample

loom, Miri and the hardware all say nothing about load buffering, and that silence is no evidence the outcome cannot happen. The RC11 → C++20 edge on the map consists of exactly this outcome: LB, allowed by C++20 and forbidden by RC11. The models on the C++20 side of the edge are built to construct such executions. MoRDor is one such implementation and enumerates every execution of the program rather than sampling runs. LB+UAF came from that enumeration. So when the run-based tools share a blind spot, the Zoo points to the model with the outcome they miss.

Exhibit 2 again: relaxed message passing leads to a proof

Relaxed message passing is allowed by every model near Rust, so no edge on the map points at exhibit 2. The Zoo still leads to the right model, through a node instead: among Rust’s neighbours on the map is ORC11, and ORC11 comes with a program logic for unsafe libraries. That is what this exhibit needs, since sampling cannot show a payload is always safe to read, but a proof can. In 2018, Dang, Jourdan and Dreyer used that logic to prove Arc sound ^[5], and the proof found exhibit 2 in the standard library. Their bug report, rust-lang/rust#51780, is the result: Arc::get_mut checked uniqueness with a relaxed read of the strong count that Arc::drop releases, leaving a read of the contents and a write through get_mut unordered. The fix was an Acquire. Proof answers here what silent test cannot: not did it happen? but can it?

Exhibit 3 again: IRIW with SC fences leads to a known bug in the concurrrency tool

The test that showed Rust took RC11’s repair is, almost line for line, the program in Miri’s issue tracker that caught its emulation producing an outcome C++20 forbids (rust-lang/miri#2301). Miri’s emulation descends from C++11 work, on the original side of this edge, so the edge predicted where its guarantee would run out. When a tool descends from a model, the edges between that model and Rust’s mark where to distrust it first.

The route backwards: a model stated up front

Those routes reconstruct a tool’s model from a README, a source header or an issue tracker. A fourth starts where the model is stated. Every Rust atomic reaches the machine through LLVM IR, which Vellvm formalises in Rocq. Its concurrent extension by Chappe, Henrio and Zakowski ^[8], built on choice trees ^[9], names its model outright: the promise-free fragment of Promising semantics ^[10], with non-atomic, acquire/release and SC accesses and, in part, monotonic ones.

The Zoo does the rest before anything runs. Promises are Promising’s only route to load→store reordering, so the fragment sits on the RC11 side of exhibit 1’s edge, and LB+UAF is among the tests that separate it from LLVM IR’s model. The authors say so: an optimisation proved under their semantics carries no guarantee for programs with monotonic accesses. Promises were left out because their thin-air certificates do not fit the choice-tree combinator — the same difficulty that keeps Miri from speculating and loom from exploring LB. The extension’s interpreter will report LB unreachable, as loom does, but here the silence was on the map before the run.

Safe Rust refuses the race before the model sees it

In safe Rust, atomics and locks are the only way to share mutable memory, so the classic litmus tests on non-atomic memory do not even compile:

1
2
3
4
5

let mut data: usize = 0;
let p: *mut usize = &mut data;

// error[E0277]: `*mut usize` cannot be sent between threads safely
let h = thread::spawn(move || unsafe { *p = 1 });

*mut T is not Send, UnsafeCell<T> is not Sync, and the borrow checker will not issue two &mut, so every route stops at sharing the location — one step before the memory model. The escape hatch, a hand-written unsafe impl Send, is what Arc, Mutex and every lock-free structure use: the programmer promises the soundness the compiler would otherwise prove.

Once it compiles, exhibit 2 with a non-atomic payload is decided by Miri’s race detector, not its sampler:

1
2
3
4
5
6
7
8
9

let w = thread::spawn(move || {
    unsafe { *dp.0 = 1 }        // non-atomic payload
    flag.store(1, Relaxed);     // Relaxed: no synchronizes-with edge
});

while flag.load(Relaxed) == 0 { // spin until the flag is observed
    std::hint::spin_loop();
}
let _rd = unsafe { *data };     // RACES with the writer's *dp.0 = 1

On x86 the payload is visible once the flag is, since stores stay in order; on Arm it need not be. Miri reports a data race either way, on every run: a Relaxed pair creates no synchronizes-with edge, so the accesses are unordered whatever the wall clock did. Temporal order is not happens-before, and here a Relaxed flag makes the program undefined behaviour — the mistake Arc::get_mut made. With Release/Acquire it runs clean.

None of this moves Rust in the lattice; it is the Java/OCaml edge of its node, what a language promises for racy programs. C++ says undefined behaviour, Java bounds it, OCaml bounds races in space and time, and Rust mostly refuses to compile them and calls the rest undefined — recorded in the Zoo’s no_ub and edrf columns rather than as an ordering edge.

Code can be written where silence is a verdict

Each blind spot is documented, explained by an edge, and avoidable by construction. Code that never depends on an outcome a tool cannot produce turns that tool’s silence back into a verdict:

1. Pair every flag: Release on the store, Acquire on the load that guards an effect. In exhibit 1 the free and the read then sit on a happens-before cycle, which C++20 forbids outright, so loom’s and Miri’s silence is the right answer.
2. Keep the published payload non-atomic. In exhibit 2 a missing Acquire then becomes a data race Miri reports on every run, not a stale read it finds by luck, and the unsafe impl needed to share the payload marks where to look.
3. Ask the contract about SC fences. For code like exhibit 3, check with herd7 against RC11, with a Miri that has the 2024 fixes as the run-based witness.
4. Use each tool for what it covers. loom for interleavings of acquire/release code; Miri for SeqCst, data races and undefined behaviour; an enumerator — MoRDor, herd7 or GenMC — for load-buffering shapes; and Miri under both aliasing models for unsafe.

None of these is new; release/acquire pairing is the textbook idiom ^[1]. The chart adds the reason each one is needed: a program inside every instrument’s coverage is one where a green run means what it appears to.

Summary

Flag-guarded reclamation with relaxed atomics is ordinary lock-free code, and in the shape of exhibit 1 it carries a use-after-free that no compiler or CPU I tested produces today. loom passes it, Miri runs it clean, and neither x86 nor Graviton3 produced it, in 30 million and 200 million runs. Yet the contract allows it: moved by hand as the contract permits, it shows up on both CPUs and under AddressSanitizer on x86, and Miri reports it once the source matches the execution, which no one can do for every program in CI. Nor is the risk only in the future: relaxed message passing, exhibit 2, never fails on x86 and fails on Graviton3 today, millions of times per 100 million runs.

Rust’s memory model is a chain of contracts — C++20, LLVM’s monotonic, the architecture manual — and a program is only as safe as the weakest of them. No layer makes the move today, but none promises not to: a compiler upgrade, a new Arm core or a RISC-V port can turn code that passed every test for years into one that frees memory under a reader. With Release stores and Acquire loads the same code is correct at every layer, and every silent tool is right to be silent. What separates the two programs is not a better tool but knowing what the contract allows. That distinction matters more as agents write more of the code. An agent can be held to a contract, and to patterns that are correct against it; it cannot be held to a green run, because a green run is the thing it optimises for.

That is what the Zoo is for. Every edge is a litmus test with a known verdict on each side, so running the edges under a tool charts its blind spots as a map rather than as bugs in production; fig5 is one. The chart tells silences apart — by model (loom on load buffering), by chance (Miri on relaxed message passing), by construction (hardware on IRIW with SC fences) — and each has a pattern and an address in the literature: an enumerator, a proof, a known bug, or, where a tool states its model as Vellvm’s extension does, a map drawn before anything runs. Rust’s position falls out along the way: below SC, with the full acquire/release hierarchy, multi-copy-atomic, RC11’s SC repair, and C++20’s thin-air gap, which nothing I tested exercises yet. And nothing in the procedure is Rust-specific: any language with atomics, and any tool that checks them, can be charted the same way.

The map, the edges and the litmus tests are described in The Relaxed Memory Model Zoo.

Two things I would particularly like to hear about. A checker I should have run: GenMC, Dat3M, or a hardware platform other than x86 and Graviton3, any of which could turn one of the silences above into a verdict. And a reference I have missed — work locating Rust, or any other shipped language, against a published model. If you are thinking “he must already know about this”, please send it anyway; that assumption is why most such messages never get written. Write to me at contact [at] kissig [dot] org ; corrections to the underlying dataset go to rmm-zoo-dataset.

References

1. Bos: Rust Atomics and Locks: Low-Level Concurrency in Practice, O’Reilly, 2023 marabos.nl/atomics/
2. Lidbury, Donaldson: Dynamic Race Detection for C++11, POPL 2017 10.1145/3009837.3009857
3. Alglave, Maranget, Tautschnig: Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory, ACM TOPLAS, 2014 10.1145/2627752
4. Lahav, Vafeiadis, Kang, Hur, Dreyer: Repairing Sequential Consistency in C/C++11, PLDI 2017 10.1145/3062341.3062352
5. Dang, Jourdan, Kaiser, Dreyer: RustBelt Meets Relaxed Memory, POPL 2020 10.1145/3371102
6. Jung, Dang, Kang, Dreyer: Stacked Borrows: An Aliasing Model for Rust, POPL 2020 10.1145/3371109
7. Villani, Hostert, Dreyer, Jung: Tree Borrows, PLDI 2025 10.1145/3735592
8. Chappe, Henrio, Zakowski: Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR, CPP 2025 10.1145/3703595.3705890
9. Chappe, He, Henrio, Ioannidis, Zakowski, Zdancewic: Choice Trees: Representing and Reasoning About Nondeterministic, Recursive, and Impure Programs in Rocq, Journal of Functional Programming 35, e21, 2025 10.1017/S0956796825100105
10. Kang, Hur, Lahav, Vafeiadis, Dreyer: A Promising Semantics for Relaxed-Memory Concurrency, POPL 2017 10.1145/3009837.3009850

Subscribe to new posts by RSS