Simulation shows that the traces you happened to run were correct. A formal property states what must hold on every trace, and a model checker or formal tool searches all of them within a model. This topic turns the two coherence invariants from Part 2 into properties, separates properties that a finite trace can refute from those that need an infinite one, shows how assumptions can make a proof meaningless, and ends with an explicit-state model checker that finds a seeded bug in a few milliseconds.
Lesson | After it you can... |
|---|---|
Write SWMR, the MOESI dirty rule and the data-value invariant as SVA and as a Python invariant with a ghost variable. | |
Classify a property, write it with assert property, s_eventually or a bounded window, and name the fairness it needs. | |
Write legal environment assumptions, spot an over-constraint and prove a pass is not vacuous with covers. | |
Size a protocol model, explain why small configurations find most bugs, and read a counterexample trace. |
Suggested order: the four lessons in sequence. They assume the SWMR and data-value invariants and the transient states of Parts 2 and 4, and the progress assumptions A1 to A6 of Stating Progress Assumptions. General formal method (what a proof is, bounded proofs, induction) lives in the First Principles of Verification Strategy course's Formal and Simulation part; this topic applies it to coherence.
The environment assumptions may exclude the traces that reach the bug (over-constraint), so the proof is about a smaller system than the real one. Or the property may be weaker than SWMR: for example it only counts M states and forgets that SM^D still serves loads, or it checks permissions but not values. Covers that reach the interesting scenarios, and a seeded bug the property must catch, address both.