Litmus Tests and How Allowed Outcomes Are Decided

A memory model is a specification of which behaviours a program may exhibit. Specifications of this kind are hard to read in prose and hard to test by running code, because the interesting behaviours appear only under specific interleavings on specific hardware, and a test that fails once in a million runs tells you little. Litmus tests are the instrument that makes the question tractable. They are small programs with a fixed number of threads, a fixed set of shared locations, and a small set of observable final states, and they are used both to characterise hardware and to define what a model permits.

The technique is old and the tooling is not. The reason it works is that the state space of a litmus test is small enough to enumerate exhaustively, so the answer is a proof over all executions rather than a sample.

The shape of a litmus test

Every litmus test has the same four parts: initial values for the shared locations, one program per thread, a set of registers to record what each thread observed, and a predicate over the final state. The predicate names the outcome being asked about. A test is usually named for the pattern it encodes, and the names are conventional enough to be worth knowing:

Name	Pattern	Question it asks
SB	store buffering	can both threads’ loads miss?
MP	message passing	can a reader see the flag but not the data?
LB	load buffering	can two loads each read the other’s later store?
IRIW	independent reads of independent writes	can two readers disagree on the order of two stores?
WRC	write-read coherence	can a third thread miss a write another thread already saw?

The store buffering test is the one from Store Buffers and the Total Store Order That Replaces Sequential Consistency: each thread stores to its own variable and loads the other’s, and the question is whether both loads can return zero. The message passing test is the publication pattern without any ordering: thread 1 stores data then a flag, thread 2 reads the flag then the data, and the question is whether thread 2 can see the flag set and still read stale data. Load buffering reverses the roles: each thread loads a variable and then stores to the other, and the question is whether each load can read the value the other thread stores afterwards. The answer separates models that preserve load-store order from models that do not.

Each test is written in a notation that names the operations explicitly, so that the ordering constraints the model imposes can be checked against the program rather than inferred from source. A message passing test looks like this:

MP
{ x=0; y=0; }
P0          | P1
MOV [x],$1  | MOV EAX,[y]
MOV [y],$1  | MOV EBX,[x]
exists (P1:EAX=1 /\ P1:EBX=0)

The exists clause is the outcome under test. Running the test means asking whether any execution of the program produces a final state satisfying that clause. On x86-TSO, the answer for MP is no: the store to x precedes the store to y in program order, stores drain in order, and the reader’s load of y precedes its load of x, so a reader that sees y set must see x set. On Arm, where store-store order is not preserved, the answer is yes.

Enumerating executions rather than sampling

The tool that made litmus testing practical is a model checker that takes the test and a description of the memory model and enumerates all executions permitted by the model. Each execution is a set of choices: for each load, which store it reads from; for each pair of operations, whether they are ordered. The model constrains the choices, and the checker reports which final states are reachable.

The number of candidate executions grows quickly with the number of threads and accesses, but litmus tests are deliberately tiny, so the enumeration finishes. For a test with two threads and two accesses each, the interesting cases number in the dozens. For four threads with two accesses each, the count is larger but still tractable. This is why the tests are kept small: the tractability is the point, not an aesthetic preference.

Two families of model description are in use. Operational models describe the hardware as a machine with buffers, queues, and caches, and generate executions by simulating it. Axiomatic models describe the model as a set of relations over the events in an execution, and generate executions by choosing relations consistent with the axioms. The two can be proved equivalent for specific models, and the equivalence proofs are themselves part of the literature. The axiomatic form is what most current specifications use, because it is easier to state precisely and easier to check against a candidate execution.

An axiomatic model is a conjunction of constraints, typically of this shape: an execution is allowed if there is a relation hb (happens-before) built from program order plus synchronisation, and every location’s reads and writes are consistent with coherence, and certain relations are acyclic. The acyclicity requirement is what forbids the outcome: if the candidate execution requires a cycle in the union of relations, no consistent ordering exists, and the execution is rejected. The message passing outcome on x86-TSO is rejected because it yields a cycle: program order puts the store to x before the store to y and the reader’s load of y before its load of x, the load of y reads the store to y, and the load of x reads the initial value, which places it before the store to x in coherence order. Following those edges returns to the start, so no consistent ordering exists.

Never observed, forbidden, and the gap between them

The most important distinction in this area is between what a test never produces on hardware and what a model forbids. They are not the same, and the gap has caused real arguments.

A model is a specification, and hardware is an implementation of it. An implementation may be stronger than the model it claims to implement, meaning it never produces some outcome the model allows. A test that never produces an outcome on a particular chip is evidence about that chip, not about the model. Conversely, a model may allow an outcome that no current implementation produces, because allowing it costs nothing in implementation terms and forbidding it would constrain future designs unnecessarily.

The practical consequence is that “it works on my machine” is not a correctness argument for synchronisation code, and neither is “it fails on my machine” a proof of a specification violation. The question is always which model the code targets. A test outcome is meaningful only relative to a stated model.

A second distinction is between an outcome being forbidden and being unlikely. Store buffering outcomes on x86 are allowed by the model and do occur; a program that assumes otherwise is wrong regardless of how often it passes. Message passing violations on x86 are forbidden by the model and should not occur; observing one on a conforming processor would indicate a hardware bug or a misidentified model. The two cases call for different responses, and telling them apart requires knowing which model applies.

Building tests that discriminate

A litmus test is only useful if different models give different answers. A test that every model forbids teaches nothing, and a test that every model allows teaches nothing either. The craft is in choosing a pattern whose outcome separates the models under consideration.

The standard progression is by strength. Sequential consistency forbids every relaxed outcome. x86-TSO allows store buffering but forbids load buffering, message passing, and IRIW: it relaxes only store-load order, so the load-load and load-store orderings that load buffering needs are preserved. Arm and PowerPC allow store buffering, load buffering, and message passing, and their treatment of IRIW depends on whether the model is multi-copy atomic. Each step down in strength is characterised by a test that the stronger model forbids and the weaker one allows, and the sequence of tests is the model’s fingerprint.

This is why the tests accumulate in the literature rather than being replaced. Each one marks a specific relaxation, and a model is defined by which of them it permits. A new architecture is characterised by running the existing suite against it, and a new model is validated by checking that its answers to the suite match the intended behaviour.

The tests also serve as regression checks for compilers. A compiler that is allowed to reorder non-atomic accesses can turn a program that is correct under a model into one that is not, and the transformation is visible as a litmus test outcome that changes. The interaction between compiler permissions and hardware permissions is Compiler Reordering and the Contract It Must Not Break.

Where the method stops being conclusive

Litmus testing has three known limits, and each one is a place where the method’s answer is narrower than it appears.

Scale. The enumeration is exhaustive only for small tests. A test with six threads and four accesses each has a state space that is no longer tractable, and the interesting behaviours of real programs typically require more threads than the tests have. The method characterises the model, not the program.

Timing. Litmus tests model ordering, not duration. An execution that is allowed by the model may be unreachable in practice because the window in which it could occur is a few cycles wide, and an outcome that requires an implausible interleaving may be formally allowed while being effectively unobservable. The model is still correct to allow it, since the specification is about possibility.

Coverage of features. A test covers the operations it names. Features that interact with ordering in ways the test does not exercise, such as unaligned accesses, memory-mapped device regions, or operations that cross page boundaries, need their own tests. A model validated on aligned word accesses says nothing about a 16-byte access split across two cache lines, and the atomicity question there is separate from the ordering question.

The method’s value is that it converts a vague question about hardware behaviour into a finite enumeration with a definite answer. That is enough to characterise models, to validate implementations, and to settle arguments that would otherwise be conducted with anecdotes.