11.2Exploring the Behavior of Memory Consistency Models

Consistency models define shared-memory behavior — so programmers and middleware writers (compiler authors, kernel developers) must be able to tell which behaviors a model permits and which it forbids. Vendors, however, traditionally specify their models in prose, which has a track record of ambiguity (a famous Linux kernel mailing-list thread spent weeks arguing about a spin-unlock optimization the manual couldn’t settle). A formal specification is unambiguous — and, better still, it makes exploration automatic.

11.2.1 Litmus tests

A memory model barely matters to a high-level programmer whose synchronization comes from libraries. It matters enormously to low-level programmers: the compiler writer implementing language-level synchronization, the kernel developer, the author of a lock-free data structure. For them, litmus tests litmus test A small multithreaded program abstracting a synchronization idiom; the outcomes a memory model allows on it characterize the model (Dekker, message passing, the same-address “coherence” test). defined in Chapter 11 — open in glossary — small multithreaded programs abstracting a synchronization situation — are the lingua franca: the outcomes a model allows on a litmus test tell the low-level programmer exactly what their hand-crafted synchronization can rely on, and whether a particular FENCE is needed. Processor vendors use the same tests in their manuals to explain their models.

You have been reading litmus tests since chapter 3: Table 3.3 is Dekker’s litmus test (it abstracts the mutual-exclusion handshake of Dekker’s algorithm), and Table 3.1 is the message-passing test. One more classic completes the set — the “coherence” litmus test (book Table 11.4): one core stores x = NEW while another loads x twice. May the first load see NEW and the second see the old 0?

Enumerate under SC, then under XC: the outcome (NEW, 0) never appears. A later same-address load reading an older value than an earlier load would violate the data-value invariant — it is exactly the per-location SC per-location sc Every memory location individually sequentially consistent. Too weak to fully specify either coherence class, but a standard safety check — weak memory models' “coherence axiom.” defined in Chapter 11 — open in glossary “coherence axiom” that even the weakest commercial models mandate (XC’s same-address Load→Load rule is this test’s guardian).

11.2.2 Exploration

Given a formal memory model and a litmus test, tools can compute every behavior the model allows on that test. The recipe is blunt-force and beautiful: exhaustively enumerate the test’s possible schedules; for each candidate execution, either check the mathematical axioms ( axiomatic axiomatic specification Specifying a system as mathematical axioms over observable actions and relations (program order, global memory order) — the formalism used for SC/TSO/XC in chapters 3–5, given its name. defined in Chapter 11 — open in glossary models) or run the reference state machine ( operational operational specification Specifying a system as an abstract reference implementation (typically a state machine) whose exhibited behaviors define the legal ones; safety from internal state, liveness via temporal-logic side conditions. Chapter 3's switch and chapters 6–9's protocol tables are operational models. defined in Chapter 11 — open in glossary models) and record the values the loads return.

Test generation matters as much as exploration: tests can be written by hand for any interesting corner, generated randomly (the TSOtool/McVersi lineage, §11.3.2), or derived systematically by shape (diy) or from the model itself (litmustestgen). One caveat keeps everyone honest: a litmus suite conveys intuition but normally cannot be a complete specification — behaviors the tests don’t cover stay unspecified. MemSynth closes that loop by synthesizing the full model that the tests imply.