Safety says a bad permission or value state is never reached. Liveness says useful completion eventually occurs. A valid liveness argument must account for the environment and finite resources, not merely repeat the safety invariant. The other Part 5 lessons cite these assumptions as A1-A6.
Assumption | What it supplies | What it does not supply |
|---|---|---|
A1. Eventual reliable delivery of accepted messages | A message the network has accepted is not lost or delayed forever. | Correct response matching or fair controller service. |
A2. Weakly fair service of enabled required work | Weak fairness: an action that stays enabled is eventually taken. (Strong fairness: an action enabled infinitely often is eventually taken.) | A fixed cycle bound, or service of work whose eligibility keeps flickering. |
A3. Finite, correctly counted buffers with the required reservations | Accepted work has a protected place and capacity is not invented. | Freedom from cycles among those resources. |
A4. Eventual downstream acceptance | A kept grant or response can leave its source. | Permission to overwrite it before acceptance. |
A5. A complete enough dependency graph | The analysed wait edges cover the claimed subsystem. | Coverage of unmodelled power, error or external-agent states. |
A6. H learns grant delivery | H can release a pending entry, by the course-model assumption or a completion message. | Delivery itself, which is A1 and A4. |
Take the corrected P/Q example: X's response has a reserved Qresp slot (A3) and updates the existing P_X. By A1 and A2, H accepts the protected Data(1). By A4 and A2, H delivers the M grant to C1. By A6, H learns the delivery, releases P_X and admits queued Y. The newest value stays at T0, in H's buffer or at C1 throughout.
This argument is invalid if Qresp itself waits for a new free P, if the output consumer can stay stopped forever, or if a credit can be lost. It also says nothing about a numerical deadline unless the assumptions include bounds for each stage. Weak fairness justifies eventual service of work that stays enabled; work whose eligibility flickers needs strong fairness or a reservation.
For verification, record which assumptions are asserted about the environment and which are proved about the design. An assumption that the request always completes would make a liveness proof circular. A fairness assumption that excludes the real starvation workload can hide the bug you wanted to find.
No. Eventual service is not a numerical bound. A bounded guarantee needs explicit arbitration, arrival and downstream-service bounds that support the calculation.