Litmus Tests and Store Buffering

A litmus test is a program so small that its entire state space can be enumerated, paired with a question about which of its outcomes are permitted by a given memory model. The programs are usually a handful of instructions on two threads, and the answers distinguish models that are otherwise indistinguishable from their prose descriptions. Store buffering is the smallest test that separates x86’s total store order from sequential consistency, and it is the reason a sequentially consistent store on x86 costs more than a plain move.

The shape of a litmus test

The convention is a set of threads, each executing a short sequence, with the observed final values of a few registers listed as the outcome. Store buffering uses two locations, x and y, both starting at zero, and two threads:

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

The question is whether the outcome r0 == 0 && r1 == 0 is allowed. Each thread writes one location and then reads the other. If the writes are ordered before the reads, then at least one read must see the other thread’s write, and the outcome is impossible. If a thread’s write can be delayed while its read proceeds, both reads can see the initial zero.

Under sequential consistency, r0 == 0 && r1 == 0 is forbidden. The model requires a single total order over all operations consistent with program order, and in every such order one of the two reads comes after the other thread’s write.

On x86 under total store order, the outcome is permitted. Each core has a store buffer, and a store retires into that buffer rather than into the coherent cache immediately. A load that follows a store to a different address does not wait for the store to drain; it reads from the cache and can miss the other core’s write, which is still in that core’s store buffer. The two cores can therefore each hold their own write in flight while reading the other’s location and seeing zero.

The test is not a theoretical curiosity. It runs on real hardware, and on x86 the outcome occurs readily when both threads execute on different physical cores. Its frequency depends on timing, but the model permits it, so a program that requires the outcome to be impossible must add ordering rather than rely on the timing being unfavourable.

What the store buffer actually does

A store buffer is a small queue between the core and its L1 cache. Stores enter it in program order and drain to the cache in program order, which is why x86 preserves store-to-store ordering. The buffer exists so that a store does not stall the pipeline waiting for cache ownership: the core records the store and continues, and the coherence transaction happens in the background.

The load path bypasses the buffer for a different address, which is the source of the reordering. A load to y does not need to wait for the store to x to drain, because the two addresses are unrelated. It reads the cache, misses if the other core owns the line, obtains a shared copy, and returns the value that is there. Meanwhile the store to x may still be queued.

There is one exception, and it is the reason the buffer is not simply a source of chaos. A load to an address that has a pending store in the buffer must see that store’s value, a property called store-to-load forwarding. Without it, a single thread would appear to violate its own program order, which no model permits.

The buffer is also why a fence is expensive. To guarantee that a store has drained, the core must either wait for the buffer to empty, which stalls the pipeline for the duration of a coherence transaction, or use a mechanism that serialises the store queue. On x86 a sequentially consistent store is implemented as a locked operation or an mfence, both of which impose that serialisation on the whole core rather than on one address.

Making the outcome impossible

A program that needs the outcome forbidden has to prevent the load from being satisfied before the store drains. There are three ways, and they differ in what they constrain.

A full fence between the store and the load orders every prior memory operation against every following one. On x86 that is mfence, or a locked instruction that has the same effect. The fence does not flush the store buffer; it waits for it to drain, which is the distinction between a fence and a flush that matters for cost: the fence’s latency is the latency of the slowest pending store.

An exchange instead of a store achieves the same thing, because a locked exchange is serialising by definition. This is the classic trick for a sequentially consistent store on x86: xchg with an immediate, which is implicitly locked and therefore ordered against everything.

A release store followed by an acquire load does not suffice. The release orders prior operations before the store, and the acquire orders following operations after the load, but neither orders the store against the load in the same thread. That is the asymmetry set out in Acquire and Release: What Each Ordering Forbids, and store buffering is the test that exposes it. A thread that stores with release and then loads with acquire is still permitted to see the other thread’s initial value, on x86 and on any other model that allows store-load reordering.

The other classic tests

Store buffering is one of a small family, and each isolates a different reordering.

Load buffering swaps the operations: each thread reads the location the other writes, then writes the location the other reads. The outcome r0 == 1 && r1 == 1 is forbidden under sequential consistency and permitted under almost every real model, including x86, because loads can be issued before earlier loads to different addresses complete.

Message passing is the producer/consumer test: one thread writes data and then a flag, the other reads the flag and then the data. The forbidden outcome is a reader seeing the flag set and stale data. x86 forbids it because stores are ordered with stores, so the flag cannot become visible before the data. Arm and POWER permit it, which is why release and acquire are needed there and are free on x86.

The load-buffering and message-passing pair show why the four reorderings are treated separately. Load-to-load and store-to-store are preserved on x86; load-to-store is preserved; store-to-load is not. On Arm all four are permitted by default, and each needs an explicit ordering. A model that is described as “strong” may preserve three of the four and permit the fourth, which is exactly x86’s position.

Reading a litmus result correctly

The outcome of a litmus test is a statement about the model, not about a particular execution. That the forbidden outcome never appears in a run on one machine does not mean it is impossible; it means the run did not hit the window. The models are defined over sets of allowed executions, and a single observed allowed execution refutes a claim that the outcome is impossible, while any number of non-observations proves nothing.

This asymmetry is why tool support matters. Model checkers enumerate the executions permitted by a formalised model and report which outcomes are reachable, and they are the standard way to check that an algorithm’s ordering is sufficient. The formal models are also where the differences between the C/C++ model and the hardware models show up, and where the C/C++ model’s own difficulties became visible: the original 2011 formulation permitted outcomes that no hardware produces, a defect addressed by later revisions and by the repair work that followed.

The practical use is narrower than the formal study. A programmer writing a lock-free structure needs to know which of the four reorderings the target permits and which orderings forbid them, and the litmus tests are the compact statement of that knowledge. Store buffering answers the store-to-load question. Message passing answers the store-to-store question. The rest follow from the same table, and the happens-before machinery that turns an observed ordering into a visibility guarantee is set out in Atomicity and Ordering Are Separate Guarantees.

Why this matters beyond the test

The reason to care about store buffering is that it defines the cost model of every flag-based publication. A release store is cheap on x86 because store-to-store ordering is free; a sequentially consistent store is expensive because store-to-load ordering is not, and the only way to get it is to drain the buffer. On Arm the accounting is different: the acquire and release forms are single instructions with modest cost, and sequential consistency requires additional barriers in positions where the pair alone does not produce a single total order.

The consequence for design is that ordering should be requested at the point where it is needed, not at the point where it is easiest to write. A flag published with release and consumed with acquire is correct for any publication of data behind a flag, costs nothing extra on x86, and costs one instruction each on Arm. A flag published with sequential consistency is correct too, costs a serialisation on every architecture, and is the right choice only when the algorithm reasons about a total order across several locations rather than about visibility of one. The litmus tests are what make that distinction checkable rather than a matter of taste.