1.4Specifying and Validating Memory Consistency Models and Cache Coherence

Managing the complexity

Everything previewed so far — consistency models memory consistency model The precise, architecturally visible definition of shared-memory correctness in terms of loads and stores; usually admits multiple correct executions. defined in Chapter 1 — open in glossary with their many legal executions, coherence protocols coherence protocol The set of rules implemented by a system's distributed actors (cache and memory controllers) that prevents access to stale data. defined in Chapter 1 — open in glossary with their swarms of transient states — is complex and subtle. That complexity must be managed, for two audiences at once:

• Programmers need multicores to be programmable: it must be possible to determine, clearly and exhaustively (ideally with tool support), which behaviors the memory model permits and which it forbids.
• Implementors need designs to be validatable: without a precise reference for what the hardware is supposed to do, there is no way to check that it does it.

Both needs point to the same requirement: consistency models must be specified formally. An informal English paragraph cannot be fed to a tool, and cannot settle an argument about a corner-case interleaving.

What Chapter 11 will cover

The final chapter of the book addresses this requirement in two movements:

1. Specification. Two complementary methods for specifying systems, each applied to both consistency models and coherence protocols:
   • operational specifications — describe an abstract machine whose step-by-step execution defines the legal behaviors;
   • axiomatic specifications — give mathematical constraints (orders and axioms) that any legal execution must satisfy.
2. Validation. Techniques for checking implementations — processor pipelines as well as coherence protocol implementations — against their specification, spanning formal methods (machine-checked proof, model checking) and informal testing.

The programmability half of this promise also explains a choice this book already made: the definition of a memory model in §1.1 — “what values dynamic loads may return” — is already phrased so it can be made mathematically precise, which is exactly what the formalism of chapters 3–5 will do.