A coherence protocol can look right in every trace drawn so far and still be wrong in an interleaving nobody drew. This part turns the course's invariants into checks: a reference model and a value checker that judge every load, formal properties for SWMR and the data-value invariant on small models, and a coverage plan built from the protocol table and its races. The Python models here run in the course checks, and each protocol model is shown catching a deliberately injected bug.
Lesson | After it you can... |
|---|---|
Explain why a checker must judge every load's value. | |
Run a small protocol model with a golden value checker. | |
Show that the checker catches each injected bug. | |
Place monitors and checkers in a real testbench. | |
Write SWMR and the data-value invariant as properties. | |
Separate safety from liveness and state the fairness needed. | |
Spot over-constraint and vacuous passes. | |
Model-check a tiny protocol and read a counterexample. | |
Derive a coverage model from the protocol table. | |
Cover the races that random traffic rarely hits. | |
Choose knobs that make races happen. | |
Assemble sign-off evidence and review a waiver. |
General verification method (scoreboards, coverage, formal) is taught in the First Principles of Verification Strategy course; this part applies it to coherence and links there instead of repeating it.
That the checker actually judges values (not only states), that the races in the protocol table were exercised (race and cross coverage), that assertions were not vacuous, and that SWMR holds on a small model by proof. A large passing number alone shows only that the traffic it generated did not expose a bug.