11.3Validating Implementations

Consistency enforcement spans the pipeline, the caches, and the memory system — and all of them must cooperate to deliver the promised model. Validating that they do is the endgame of the whole book. Exhaustive validation of a full modern multiprocessor is out of reach, so a gamut of techniques exists, from formal verification down to plain testing. This section is the whistle-stop tour.

11.3.1 Formal methods

A formal model of the implementation is validated against a specification. Since each side can be 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 or 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 , the techniques sort into a matrix:

Operational implementation vs axiomatic spec. The classic manual proof shows the implementation satisfies each axiom: Meixner & Sorin proved that a pipeline presenting loads/stores in program order, on top of a protocol maintaining SWMR swmr invariant Single-writer–multiple-reader: for any memory location at any moment, either one core may write (and read) it, or some number of cores may only read it. defined in Chapter 2 — open in glossary and the data-value invariant data-value invariant The value of a memory location at the start of an epoch equals its value at the end of its last read-write epoch. defined in Chapter 2 — open in glossary , enforces SC (§3.11’s result, now in its proper home). A powerful proof template (Plakal et al.) borrows Lamport’s clocks from distributed systems: assign hypothetical timestamps to actions (a store’s fetch; the GetM it causes gets a later one), derive a global order of all memory operations, then check every load against the load value axiom load value axiom A load returns the value of the most recent same-address store before it in global memory order. defined in Chapter 11 — open in glossary . Model checking model checking Exhaustive exploration of a state machine's state space against invariants such as SWMR: explicit-state (Murphi), symbolic, or bounded; parameterization generalizes exhaustive small-system results to arbitrary cores and addresses. defined in Chapter 11 — open in glossary automates the spirit: express the protocol — the book’s tables translate almost mechanically — in a tool like Murphi, state invariants like SWMR, and let the checker explore the entire state space, returning either “holds” or a concrete counterexample trace. The catch is state-space explosion: explicit-state checking only handles toy configurations (2–3 cores, addresses, values). Countermeasures: symbolic model checking (manipulate sets of states), bounded model checking (counterexamples up to a length limit, surrendering exhaustiveness), and — for a complete proof — exhaustively checking a small system, then parameterization to arbitrary cores and addresses.

Operational implementation vs operational spec. Two state machines, Q (implementation) and S (spec), same observable actions: show every behavior of Q is a behavior of S. The stylized technique is refinement refinement (simulation) Proving implementation Q's behaviors are contained in specification S's via an abstraction function F from Q-states to S-states that preserves initial states and observable transitions. Making F work surfaces the protocol's invariants (e.g., SWMR). defined in Chapter 11 — open in glossary — reason about pairs of states instead of sequences, via an abstraction function. Watch it run on a familiar protocol, and watch the proof obligation surface an invariant you know well:

The Kami framework carries out exactly this style of proof mechanically, showing that a processor plus coherent memory system satisfies SC. A lighter-weight alternative runs Q and S side by side in a model checker on the same inputs, checking they emit the same outputs (Banks et al. validated a lazy coherence protocol against its weak model this way). It is sound — “equivalent” verdicts are true — but non-determinism makes it incomplete: identical behavior under different schedules can look like a mismatch.

Axiomatic implementation vs axiomatic spec. For µhb pipeline models (§11.1.2), the Check family (PipeCheck, COATCheck for the hardware-OS interface, CCICheck for the coherence–consistency interface) reuses §11.2’s trick: exhaustively enumerate the implementation’s behaviors on a litmus test and compare against the spec’s behaviors. More behavior than the spec allows = a bug; less = the implementation is conservative. Repeat across the suite. The residual gap — exhaustive only per test — is closed by PipeProof: an induction-style proof over a symbolic program abstraction covering programs of any length, all addresses, all values.

11.3.2 Testing

Formal verification is not a panacea, for three reasons: it scales poorly (model checkers drown; the techniques that don’t aren’t automatic), formal models can be mis-specified, and even accurate models can be incomplete — silicon contains things the model never mentioned. So the final implementation must also be tested, two ways.