Here is the whole experiment:

initially: x = 0, y = 0

Thread 0          Thread 1
x = 1             y = 1
r0 = y            r1 = x

Ask for the ending that feels most illegal:

r0 = 0 and r1 = 0

Both threads wrote first. Both threads read second. And yet each read missed the other thread’s write.

If your mental model is “there is one real order in which memory operations happen,” this outcome is impossible. But that mental model has a name: sequential consistency. Lamport defined it as the condition that a concurrent execution looks like some single interleaving of all processors’ operations, while preserving each processor’s program order.1 It is beautiful. It is also a contract, not a law of physics.

The small program above is the store-buffering litmus test. It is useful because nothing about it is ornate. There is no lock, queue, compiler trick, or data structure. It is just the question: when a core has performed a store, who has seen it?

The Forbidden Interleaving

Under sequential consistency, each thread has two ordered events:

T0: store x=1 before load y
T1: store y=1 before load x

For r0 to be zero, the load of y must happen before Thread 1’s store to y. For r1 to be zero, the load of x must happen before Thread 0’s store to x.

Put those together:

T0 store x=1
  < T0 load y
  < T1 store y=1
  < T1 load x
  < T0 store x=1

The order loops back into itself. A single global timeline cannot contain that cycle. So sequential consistency forbids the 00 ending.

This is the first lesson: a memory model is not merely about whether values are atomic. It is about which explanations are allowed.

The Store Is Still in the Hallway

A store buffer gives the 00 ending an explanation.

The core can retire its store into a private buffer and continue. Later, that buffer drains to shared memory. A later load from the same core may be allowed to read shared memory before another core’s buffered store has drained. The core did not travel backward in time. It simply did not make the write globally visible before the load.

One witness looks like this:

T0 buffers x=1
T0 reads y -> 0
T1 buffers y=1
T1 reads x -> 0
T0 drains x=1
T1 drains y=1

This style of operational story is close to the approachable presentation of x86-TSO: each processor has a FIFO store buffer, loads consult their own buffer for the same address and otherwise read shared memory, and fences or locked operations can force stronger ordering.2 It is still a model. Real machines and languages have more detail. But as a first lens, it is the right kind of wrong.

Adve and Gharachorloo’s memory-consistency tutorial is useful because it keeps the central tension visible: programmers want simple reasoning rules, while implementations want caches, write buffers, speculation, and reordering freedom that preserve single-thread behavior but can surface in concurrent code.3

A Litmus Lab

The lab exhaustively enumerates the tiny program and then runs a random operational scheduler. The random frequency is not a CPU probability; it is a way to make the witness appear and disappear as stores drain earlier or later.

Try these three modes:

  • Sequential consistency: 00 is crossed out because no interleaving preserves both threads’ program order and produces it.
  • TSO store buffer: 00 is allowed. Both writes can sit in private store buffers while both loads read old shared values.
  • TSO with fences: a fence between each store and load makes the core wait for its own store buffer to drain before reading.

Default audited facts:

  • sequential consistency has 6 exact interleavings and 0 both-zero paths;
  • the store-buffer model has 80 exact transition paths and 18 both-zero paths;
  • adding fences removes both-zero again;
  • the default random TSO scheduler sees both-zero about 31.8% of the time.

    The audit checks that SC forbids both-zero, TSO permits it, fenced TSO forbids it, exact outcome counts are finite, and the default simulation reaches a both-zero witness.

    The Language Has Its Own Contract

    There are two layers that are easy to mix together.

    At the hardware layer, a model such as x86-TSO describes which machine-code executions are allowed. At the language layer, C++ atomics describe which source-level executions are allowed and what compilers may transform. Boehm and Adve’s C++ memory-model paper is explicit about the bargain: ordinary data races do not get a friendly semantics, while race-free programs are meant to recover sequentially consistent reasoning for the high-level subset.4

    So the litmus test should not be written with plain racing C++ variables and then interpreted as a portable program. Use atomics if you want a language-level experiment. With relaxed atomics, C++ guarantees atomicity for each object but does not make the operations synchronization operations.5 With memory_order_seq_cst, the language adds a single total order over the sequentially consistent atomic operations, which rules out this particular both-zero result.

    The trap is thinking that “atomic” means “everyone saw it in the same story.” Atomicity is not enough. You also need an ordering relation strong enough for the invariant you are trying to prove.

    What the Test Teaches

    The store-buffering litmus test is small enough to fit in a margin, but it contains the hard part of concurrent programming:

    • Local program order is not automatically global visibility.
    • A write can be complete for the writing core before it is visible to another core.
    • A fence is not ceremonial. It changes the set of legal explanations.
    • Testing by repetition is evidence about one environment, not a proof of a memory model.
    • Tools such as herd7 exist because tiny litmus tests are already too subtle to reason about by vibe.6

    The deepest mistake is to imagine memory order as a timestamp attached to each operation. The useful picture is relational. Which operations must be before which other operations? Which reads are allowed to see which writes? Which cycles are forbidden?

    The write happened.

    The question is where.

    1. Leslie Lamport, “How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs”, IEEE Transactions on Computers, 1979. ↩

    2. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen, “x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors”, Communications of the ACM, 2010. ↩

    3. Sarita V. Adve and Kourosh Gharachorloo, “Shared Memory Consistency Models: A Tutorial”, IEEE Computer, 1996. ↩

    4. Hans-J. Boehm and Sarita V. Adve, “Foundations of the C++ Concurrency Memory Model”, PLDI, 2008. ↩

    5. “std::memory_order”, cppreference.com. ↩

    6. Jade Alglave and Luc Maranget, “Simulating memory models with herd7”, herdtools documentation. ↩