Litmus Tests as Executable Specifications

A memory model that exists only as English prose cannot be tested. The prose can be read two ways, the readings disagree on a program nobody has written yet, and the disagreement surfaces as a bug in a compiler’s fence placement or in a kernel’s barrier macro. Litmus tests exist to make the model falsifiable: a tiny program, a set of observed outcomes, and an annotation saying which outcomes the model forbids.

The technique has a long history in the hardware community and was brought into the tooling era by the herd/herdtools7 suite, which reads litmus files, simulates them against a formal model, and reports whether the annotated outcome is reachable.

Anatomy of a litmus file

A litmus test names the architecture, declares its threads, and ends with an assertion about the final state. The exists clause is the interesting one: it lists an outcome that the test asserts is possible. A model that forbids the outcome makes the test fail, and that failure is a finding.

AArch64 MP
{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X1] ;
 STR W0,[X1] | LDR W2,[X3] ;
 MOV W2,#1   |             ;
 STR W2,[X3] |             ;
exists (1:X0=1 /\ 1:X2=0)

The test is the message-passing pattern: thread 0 writes x, then writes the flag y; thread 1 reads the flag and then reads x. The asserted outcome is that thread 1 saw the flag set but did not see the data. On ARMv8 this outcome is permitted, and the checker reports that it is reachable. Ordering thread 0’s two stores is not enough on its own, because the two stores become visible to thread 1 independently: the flag’s new value can reach thread 1 before the data’s does. This is the reason the kernel inserts smp_wmb between the two stores, and the reason the same test with that barrier added reports the outcome as unreachable.

The same test on x86 reports the outcome as unreachable without any barrier, because a store buffer drains in order and loads are performed in program order, so a reader that sees the later store must also see the earlier one. The difference between the two verdicts is a fact about the models, and a litmus suite that reported the same answer for both architectures would be describing neither of them.

The exists clause names a candidate outcome and asks whether the model permits it; the checker answers Never or Sometimes. The dual clause is forall, which asserts that a condition holds in every permitted execution, and it is the form used when a test is written to assert that something is forbidden. Most suites prefer exists, because the interesting direction is confirming that a model is weak enough to permit the reordering the hardware actually exhibits, and strong enough to forbid the ones it does not.

What the format forces the author to state

A litmus test is an exercise in removing ambiguity. Every location is named; every register is named; the initial memory state is stated; the final condition is a conjunction over registers. There is no room for “the flag is set at some point” or “the read happens after the write” — the test says exactly which registers hold which values at the end.

That explicitness is what makes the tests portable across models. The same file can be run against an axiomatic model, an operational model, and a hardware implementation, and the three answers can be compared. A disagreement between the model and the hardware is either a model bug or a hardware bug, and both are worth knowing about.

The format also encodes the observation model. Values written to memory by a thread appear in registers at the end of that thread’s execution; the test’s final condition reads those registers. This corresponds to a run where each thread executes its instructions and then stops, and the observer reads the final register state. Litmus tests do not, by themselves, test for liveness, fairness, or progress — a thread that never terminates is outside what the final-state assertion can express.

How a model checker searches

An axiomatic checker such as herd works by candidate enumeration. Given the test, it generates the set of possible executions: assignments of reads-from for every read, and a modification order for every location. For each candidate it checks the model’s axioms — does the candidate satisfy coherence, does it satisfy the ordering constraints the architecture imposes, does it contain the annotated final state. A candidate that satisfies everything is a witness, and the test is reported as allowed.

The search space is small for a test with two threads and two locations, and it grows with the number of events. For a test with five events per thread and three locations, the number of candidate executions is manageable; for a real program it is not, which is why litmus tests are five lines rather than five hundred.

A hardware model in the same framework is expressed as a set of relations and constraints over the candidate. The ARMv8 model, for instance, defines orderings such as the barrier-induced order, the dependency-induced order, and the atomicity constraints of exclusive operations, and the checker tests each candidate against all of them. The formal model and the prose specification are then two descriptions of the same predicate, and disagreements between them are the subject of the papers that introduced the models.

Simulation against hardware

A litmus test can also be run on real hardware. The tooling wraps the test’s assembly in a driver that executes it many times with varying interleavings and records the outcomes actually observed. The outcome distribution is not a proof — a rare interleaving may never be sampled — but an outcome that is observed is a proof that the model must permit it.

The asymmetry is the useful part. Simulation can refute a model (by exhibiting an outcome the model forbids) but cannot confirm one. Model checking can confirm that an outcome is reachable in the model but says nothing about whether the hardware ever produces it. The two together bracket the truth: the model is validated when the set of outcomes it permits matches the set the hardware produces, and neither alone establishes that.

A test that the model permits and the hardware never produces is not necessarily a model bug. The model may be conservative — permitting an execution the implementation happens to exclude — and conservative models are the normal case, since the model must cover every implementation of the architecture, including ones with different pipelines.

Why the tests matter beyond hardware

The same technique applies to compiler and language models. A C++ litmus test can ask whether a particular combination of release, acquire, and relaxed operations permits an outcome, and the answer constrains what a compiler is allowed to emit. This is how the more obscure corners of the C++ model were settled: the interaction between fences and relaxed operations, the treatment of read-modify-write chains, and the precise status of memory_order_consume were all argued with litmus tests.

The tests are also the vocabulary in which hardware and compiler people talk to each other. A bug report that says “the compiler reordered my release store past a later relaxed load” is arguable; a bug report that includes a litmus test with an exists clause and a model’s verdict is a specification of the disagreement.

The limits of the approach

Litmus tests are small by construction, and small tests do not compose into large ones. A model that passes every two-thread test in a suite may still permit an outcome that a three-thread program can reach, because the interaction requires a cycle through a third participant. Suites therefore include multi-thread tests, and the search cost grows accordingly.

The tests also assume a fixed observation model and a fixed notion of a final state. Programs whose correctness depends on the order of side effects rather than on final register values — I/O, device access, signal delivery — are outside what the format expresses. And a test asserts reachability, not probability: an outcome that requires an interleaving the hardware reaches once in a billion executions is still permitted by the model and still a real bug if the program depends on its absence.

The happens-before relation is what a language-level litmus test is really probing, and the ARMv8 model’s dependency orderings are the ones whose litmus tests are hardest to get right, because the dependency relation is defined on the syntax of the instruction sequence rather than on its values.