A store-buffer memory-model interpreter

You cannot test a memory-ordering bug. So build the memory model instead, and drive it with an explicit schedule.

pub fn interpret(program: Vec<Instr>, schedule: Vec<usize>) -> Vec<i64>

This is the testable companion to the orderings article. A real reordering is invisible on x86 and non-deterministic on ARM — but a simulator of the store-buffer model, stepped by a schedule you supply, is completely deterministic, and getting it right requires understanding the semantics rather than reciting them.

The machine

Two threads (0 and 1), two shared variables (0 and 1), two registers per thread. Everything starts at 0.

Each thread has a store buffer: a FIFO queue of writes it has issued but which are not yet visible to the other thread. This one structure explains almost every surprising outcome real hardware produces.

Keep this enum exactly as given — the grader constructs values of it:

#[derive(Clone, Copy)]
pub enum Instr {
    Store { thread: usize, var: usize, value: i64, seq_cst: bool },
    Load  { thread: usize, var: usize, reg: usize, seq_cst: bool },
    Flush { thread: usize },
}

The rules, precisely

Store, relaxed (seq_cst: false) — push (var, value) onto the back of this thread’s buffer. Memory is untouched. The other thread cannot see it.

Store, seq_cst — drain this thread’s whole buffer into memory in FIFO order first, then write value to memory directly.

Load, relaxed — if this thread’s own buffer has pending writes to var, read the most recent one; otherwise read memory. This is store-to-load forwarding: a thread always sees its own writes in order, even the ones nobody else can see yet.

Load, seq_cst — drain this thread’s buffer into memory first, then read memory.

Flush — pop one entry from the front of this thread’s buffer into memory. No-op if the buffer is empty. This is the schedulable stand-in for the hardware draining a store buffer whenever it feels like it.

Execution

program is a flat list; the instructions belonging to one thread execute in the order they appear. schedule[k] names a thread: step k executes that thread’s next unexecuted instruction, or does nothing if it has none left. Instructions never reached by the schedule simply do not run.

When the schedule ends, drain thread 0’s buffer, then thread 1’s.

Return six values:

[ t0.r0, t0.r1, t1.r0, t1.r1, mem[0], mem[1] ]

The litmus test this exists for

Store buffering, the classic:

T0: store x = 1 ; load y -> r0
T1: store y = 1 ; load x -> r0

Schedule [0, 0, 1, 1] — each thread runs both of its instructions in order, T0 fully before T1. Nothing is reordered within a thread.

With relaxed stores, both loads read 0. Both threads stored 1 to their own variable, and neither sees the other’s, because both writes are still sitting in store buffers.

That outcome is impossible under sequential consistency. There is no interleaving of the four operations in which both loads read 0: whichever store happened first must be visible to the later load. And yet it is exactly what an x86 processor does, every day, because x86’s store buffer is real. The most famous “impossible” result in concurrency, produced by two queues.

With seq_cst stores, the same program and the same schedule give r0 = 0, r1 = 1. T0’s store lands in memory immediately, so T1’s load sees it. Same instructions, same interleaving, different answer — and that difference is precisely what an Ordering argument buys.

Why the starter fails

It is a sequentially consistent interpreter: every store hits memory the moment it executes, and seq_cst changes nothing because everything already behaves that way. It is a perfectly good model of a machine that does not exist. It cannot produce (0, 0) on the store-buffering test, and it is therefore useless for predicting what your real program will do.

What this is, and what it is not

Real hardware and the real C++20/Rust model are far richer than this: load buffering, speculative execution, cache-coherence protocols, dependency ordering, and a formal semantics stated over partial orders rather than buffers. loom, the crate that does this properly, explores all legal interleavings rather than one you supplied, which is what makes it a testing tool rather than a teaching one.

What the store-buffer model does capture is the single most common source of real-world surprise, and the reason Release/Acquire exist at all. If you can predict this machine’s output, you can read a lock-free algorithm and say something true about it.