A proof report says a liveness rule passed a bounded run, and the team signs off. The report means no finite prefix of that length broke the rule, which for a liveness rule means almost nothing: only an infinite trace can refute it, and a bounded run never sees one. This lesson's one job is the classification that stops that sign-off: which rules a bounded run can refute, and what refutes the rest.
Safety says nothing bad happens within any finite prefix: overflow, two grants, a corrupted word. A finite trace that exhibits the bad thing refutes it, which is why a bounded run, exhibiting finite traces, can refute safety and why every safety counterexample in this course is a finite path. Liveness says something good happens on every infinite trace: every request granted, no starvation. No finite prefix refutes it, because any prefix could extend with the good thing; only a lasso, a prefix plus a loop that repeats for ever without the good thing, refutes it.
A bounded response, grant within N cycles, is safety wearing a number: exceeding the bound is a finite bad prefix of length N plus 1. That single move, adding the bound, is what makes response rules provable in a flow with no liveness engine, and the next lessons price it exactly.
Rule | Safety or liveness | What refutes it |
|---|---|---|
FIFO never overflows | Safety | The finite push sequence that fills it plus one. |
Grant is one-hot | Safety | One cycle with two grant bits. |
Every request is eventually granted | Liveness | Only a lasso where the loop never grants it. |
Every request granted within 6 cycles | Safety | A finite wait of 7 cycles. |
No deadlock, defined as: no reachable state in which no step is enabled | Safety | The finite prefix that reaches such a state (the bad thing is a state predicate). |
Mutual exclusion | Safety | One cycle with both sides inside. |
Fair service, served again and again | Liveness | Only a lasso where the loop skips it. |
Responses leave in request order | Safety | The finite pair that swaps. |
Credits are conserved | Safety | The finite point where the count disagrees. |
Reset releases the block: it starts eventually | Liveness as written; safety once bounded (starts within N cycles) | Unbounded: only a lasso that never starts. Bounded: a finite wait of N plus 1 cycles. |
Two rows need care. A deadlock check is safety only because it is defined as reaching a state: the checker looks for a configuration in which no step is enabled. The informal idea, activity that never completes (a livelock) or one requester skipped while others are served (starvation), is not a state predicate and needs a lasso, so it sits on the liveness side. The three words are separated precisely in the applications section. The reset row shows the general move: any liveness rule with a stated deadline is safety, and the deadline has to come from the specification.
Every property comment says which side it is on: within N cycles for safety, eventually for liveness, with no mixing of the words.
Every liveness claim names its engine or its bound: a bare eventually with a bounded proof behind it is a review failure.
Deadlock, livelock and starvation are three different words: no progress possible, activity without completion, and one requester skipped while others are served.
Classify before proving: ask what the shortest refuting trace looks like. If you can draw it as a finite path, the rule is safety and a bounded run can refute it. If refuting it needs the trace to loop for ever, it is liveness and a bounded pass is inconclusive by construction. When a rule you believed was liveness turns out windowed, say so in its comment and move it to the safety column.
Refuting safety needs only a finite bad prefix, which fits inside the bound. Refuting liveness needs an infinite trace with no good event, and every bounded trace is finite, so the good event might always arrive one cycle later.