A rule that says nothing bad happens and a rule that says something good happens need different evidence, different engines, and different counterexamples. Confusing them produces the two classic false claims: calling a bounded pass a liveness proof, and calling an unconstrained starvation trace a design bug. This topic draws the line, then works the three rules that live on it: bounded response, fairness, and the weak-strong distinction.
Lesson | After it you can... |
|---|---|
Classify any rule as safety or liveness and name the shape of its counterexample. | |
Say what weak and strong mean on infinite traces and on finite prefixes, and separate both from vacuity. | |
Write a grant-within-N rule with a justified N, and show that too small and too large both mislead. | |
Constrain the environment to be fair without constraining the design, and spot a fairness that hides starvation. |
Suggested order: top to bottom. Classification first, because every later lesson names which side its rule is on; then weak and strong, which refines the liveness side; then bounded response, the runnable substitute the open flow supports; then fairness, which is what makes liveness proofs honest. The engine view of liveness continues in the proof-engines section.