Ten chapters in, you are hopefully convinced that consistency models and coherence protocols are complex and subtle. This final chapter is about taming that subtlety rigorously: how to formally specify consistency models and coherence protocols (this section), how to explore the behaviors a specification allows (§11.2), and how to validate that implementations actually obey their specifications (§11.3).
A specification is the contract between a system’s user and its implementer: it answers what are the allowed behaviors? — leaving how they are enforced to the implementation. A system meets its environment through actions: input actions (user → system), internal actions (invisible inside), and output actions (system → user). Only input and output actions are visible, so a sequence of them is a behavior — and the observable actions observable actions The input/output actions at a system's interface (internal actions are invisible); their sequences define the system's behavior. Consistency model: loads/stores + values returned. Coherence protocol: read/write-request and read/write-return — a write's completion instant is observable for coherence but not for consistency. defined in Chapter 11 — open in glossary are where all specification begins. Two classes of properties constrain behaviors: safety safety The 'nothing bad ever happens' half of correctness — coherence's SWMR and data-value invariants. Trivially satisfiable by doing nothing; must be paired with liveness. defined in Chapter 9 — open in glossary (“bad things don’t happen” — which sequences are legal; concurrency means there are usually many) and liveness liveness The 'something good eventually happens' half of correctness: freedom from deadlock, livelock, and starvation. defined in Chapter 9 — open in glossary (“good things eventually happen” — a system that accepts one input and halts is safe and useless).
Consistency model: what’s observable
The contract is software ↔ hardware. Inputs: loads and stores (with core ID, address, store value). Outputs: the values loads return. Nothing else — in particular, when an operation completes is not observable.
Coherence protocol: what’s observable
The protocol’s user is the pipeline (§2.3’s interface). Inputs: read-request, write-request. Outputs: read-return (a value), write-return (an ack) — the pipeline must know when a write completes, so a write’s completion instant IS observable here.
That last asymmetry — write completion observable for coherence, invisible for consistency — will decide exactly which correctness condition specifies each, in a few paragraphs. There are two major specification styles: operational (describe an abstract reference implementation) and axiomatic (describe behaviors with mathematical axioms).
11.1.1 Operational specification
An operational specification 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 is a reference implementation, usually a state machine: whatever behaviors it can exhibit are, by definition, the legal ones. Internal state and internal actions do the constraining (that’s safety); liveness rides along as separate temporal-logic axioms (“state changes must eventually happen”).
An operational consistency spec typically has two components mirroring real hardware — a pipeline part and a memory system part, the latter presenting exactly the coherence interface above. Here are two operational specs of SC with identical in-order pipelines but different memory systems — a contrast that will formally separate §2.3’s two coherence classes.
Spec1: in-order pipeline + atomic memory
- Fetch: a core is picked non-deterministically; it fetches its next instruction into a local queue.
- Issue: a core is picked; a memory instruction issues a read-request or write-request and the pipeline blocks.
- Atomic memory: a read-request reads memory and responds with the value; a write-request writes memory and responds with an ack.
- Return: the pipeline unblocks on the response.
This is §3.6’s switch, formalized. Non-determinism at steps 1–2 generates all the legal interleavings.
Spec2: in-order pipeline + buffered memory buffered memory (sc spec2) Atomic memory front-ended by one global FIFO store queue; writes ack on enqueue and late-ack on drain; a load waits for its core's latest write to be late-acked. Still yields SC — an operational specification of consistency-directed coherence. defined in Chapter 11 — open in glossary
- Issue′: a store issues a write-request and blocks; a load first waits for the core’s latest write to be late-acked, then issues a read-request and blocks.
- Buffered memory: one global FIFO store queue fronts memory. A write-request is enqueued (with address, value, core ID) and acked immediately; when it drains to memory, a late-ack goes to the issuing core. Reads read memory directly.
Still SC! The single FIFO queue drains stores without violating any core’s program order — and the load rule keeps a core from racing past its own queued store.
In the message-passing program (Table 11.1 — our old friend: S1: St data=NEW; S2: St flag=SET vs a spin on flag then L2: Ld r2=data),
both specs can exhibit «S1, S2, L1:r1=SET, L2:r2=NEW» — and neither
can exhibit the SC-violating «…, L1:r1=SET, L2:r2=0».
Same SC, different coherence: linearizability
As consistency specs, Spec1 and Spec2 are equivalent. As coherence specs, they differ observably. Spec1’s atomic memory performs writes synchronously — a consistency-agnostic consistency-agnostic coherence Coherence in which a write returns only after being made visible to all cores; presents the illusion of an atomic memory, independent of the consistency model. defined in Chapter 2 — open in glossary protocol. Spec2’s buffered memory performs them asynchronously — a consistency-directed consistency-directed coherence Coherence in which writes propagate asynchronously but the order writes become visible must obey the consistency model; the newer GPU-era category. defined in Chapter 2 — open in glossary protocol (Afek et al.’s lazy caching is a more aggressive spec in the same family). One four-event trace tells them apart:
Four observable actions; the internal story is unknown.
1 / 6The trace on trial (Table 11.2)
Core C1: write-request(X,1) at t0, write-return at t1. Core C2: read-request(X) at t2, read-return → 0 at t3. The write RETURNED before the read was even issued — and yet the read saw the old value. Is this behavior legal? Depends on whom you ask.
Refining specs into implementations. The operational style’s great convenience: implementations are just refinements. Add per-core caches and coherence controllers to Spec1 — read/write-requests now check the local cache, misses send GetS/GetM to a directory — and you have a detailed protocol. Read that sentence again with ch. 6–9 in mind: the book’s protocol tables are operational models, refinements of Step 3. Pipelines refine the same way (more stages, more internal actions). Tool support: state-machine languages like Murphi and TLA+ express these models directly — every protocol table in this site could be typed into either almost mechanically.
11.1.2 Axiomatic specification
An axiomatic specification 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 constrains behaviors with mathematics instead of machinery. You have been reading axiomatic specs since chapter 3 — the formalism of §3.5, §4.3, and §5.2 is exactly this method:
- Observable actions: loads, stores, values returned.
- Relations: program order program order The per-core total order (<p) of a core's memory operations as specified by its program. defined in Chapter 3 — open in glossary (per-core total order) and the global memory order memory order The total order (<m) on all cores' memory operations that an execution appears to perform. defined in Chapter 3 — open in glossary (total order over all cores’ operations).
- Safety axioms (for SC): the preserved program order preserved program order (ppo) axiom The global memory order respects each core's program order — SC's first safety axiom, shrunk by relaxed models. defined in Chapter 11 — open in glossary axiom — memory order respects each core’s program order; 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 — a load returns the most recent same-address store in memory order; and the atomicity axiom — an RMW read-modify-write (rmw) An atomic instruction (e.g., test-and-set, fetch-and-increment, compare-and-swap) whose load and store appear consecutively in memory order. defined in Chapter 3 — open in glossary ’s load and store sit consecutively in memory order.
- A liveness axiom: no operation is preceded by infinitely many others — every operation eventually performs.
A behavior is legal iff some global memory order satisfying all the axioms exists. Coherence gets the same treatment: take the four request/return actions, add two internal actions — read-perform and write-perform, the instants a request takes effect — define memory order over the perform events, keep SC’s three safety axioms, and add a fourth: each perform sits between its request and its return. That fourth axiom is precisely the real-time rule, so the result is per-location linearizability — the axiomatic spec of consistency-agnostic coherence. (Consistency-directed protocols are specified like the consistency models they enforce.)
Specifying implementations axiomatically
Axioms can also model hardware faithfully rather than specify
correctness — the goal shifts from “what is legal” to “what does this
pipeline actually do.” Following Lustig et al.’s PipeCheck, each
load or store expands into per-stage sub-actions — a five-stage
pipeline gives loads fetch, decode, execute, memory, writeback and
stores those five plus exits-store-buffer, memory-write — and
pipeline ordering axioms pipeline ordering axioms Microarchitectural happens-before axioms over per-stage sub-actions (fetch, decode, …, exits-store-buffer, memory-write) that faithfully model a pipeline (PipeCheck). An acyclic set of required edges = permitted behavior; a cycle = forbidden.
defined in Chapter 11 — open in glossary
state which orderings the machine preserves, as microarchitectural
happens-before (µhb):
- fetch honors program order: i1 →po i2 ⇒ i1.fetch → i2.fetch;
- decode/execute/memory/writeback each preserve the previous stage’s order;
- the store buffer is FIFO: writeback order ⇒ exits-store-buffer order;
- writes are ordered: exits-store-buffer order ⇒ memory-write order;
- and a µhb load value axiom: a load’s memory stage reads the latest memory-write before it.
Note the altitude change: ppo specifies correctness; pipeline ordering axioms describe an implementation — whether the implementation’s axioms uphold the model’s ppo is exactly the validation question of §11.3. The analysis style, though, is one you can run by hand — witness a forbidden outcome by trying to order the sub-actions, and watch it die by cycle:
Each arrow: “must happen before.”
1 / 6The question (Table 11.3)
C1: S1: St data=NEW; S2: St flag=SET. C2: L1: Ld r1=flag; L2: Ld r2=data. Suppose L1 reads SET. Can L2 still read the old 0? Method: model each instruction as pipeline SUB-ACTIONS (fetch, decode, execute, memory, writeback — stores add exits-store-buffer and memory-write), then try to build a global order of sub-actions satisfying the pipeline ordering axioms. If the required orderings form a cycle, no such execution exists.
Manerkar et al.’s CCICheck extends the same µhb machinery across the pipeline–coherence boundary — it is the tool that formalized (and fixed) §9.3’s Peekaboo problem. Tool support for the axiomatic style: Alloy, the Cat language of the herd tool, and the Check suite’s µspec DSL for pipelines and protocols.
Check yourself: specifying consistency and coherence
1.What is observable for a coherence protocol but NOT for a consistency model?
2.In SC Spec2 (buffered memory), why must a load wait until the issuing core's latest write has been late-acked?
3.The trace «write-request(X,1), write-return, read-request(X) by another core, read-return(X,0)» is…
4.Why can consistency-agnostic coherence be enforced per memory location (e.g., by distributed directories), while SC cannot be decomposed that way?
5.In the axiomatic pipeline model, what does a CYCLE among required µhb edges (as in Table 11.3's message-passing test) establish?