Nothing moves, something moves but never finishes, or everything moves except one victim. These are three different failures with different proofs, and confusing them wastes weeks: a deadlock needs a cycle in the wait-for graph, livelock needs activity without completion, starvation needs one requester denied while others are served. This topic defines all three once, proves bounded grants on the round-robin arbiter, finds a wait cycle in a two-stage handshake chain structurally before proving progress temporally, and writes down exactly what fairness was assumed.
Lesson | After it you can... |
|---|---|
Define the three precisely and argue circular wait on a graph. | |
Prove one-hot, no-phantom and bounded-wait grants for four requesters. | |
Find a wait cycle structurally and prove bounded progress. | |
State, bound, document and check the fairness a progress proof rests on. |
Suggested order: top to bottom. Definitions first, because every later lesson uses them; the arbiter proof, which is the worked starvation case; the chain lesson, which adds the structural step; fairness last, because it tells you what the first three assumed. The safety-versus-liveness background and the liveness-engine view sit in their own lessons.
Deadlock until shown otherwise: no progress is possible anywhere. Livelock would show activity, starvation would show other requesters being served. Confirm on the wait-for graph, then read the temporal trace.