Everyone is waiting for someone else, and the graph shows the cycle. Draw an edge Ti → Tj whenever Ti waits for a resource Tj holds; the whole system is stuck if and only if that wait-for graph contains a cycle. Down the center, data flows: a hold/wait state goes in, the engine builds the graph and hunts the cycle, the verdict comes out — proven against ground truth over 4096 states. The blue team builds and defends it; the red team tries to break it.
source E. G. Coffman, M. J. Elphick, A. Shoshani, System Deadlocks, ACM Computing Surveys 3(2):67–78 (1971), DOI 10.1145/356586.356588 (paywalled — canonical id cited, AMBER). Rendered, not quoted.
Single-instance resources. Each thread holds a set of locks and is blocked on at most one it requests. Build the wait-for graph: an edge Ti → Tj exactly when Ti waits for a lock Tj currently holds.
The theorem (Coffman 1971): a deadlock exists iff the graph has a cycle. Ground truth is not the cycle — it is graph reduction: repeatedly finish any thread whose request is free or held by an already-finished thread, releasing its locks. Whoever can never finish is deadlocked. For the current scenario:
| thread | waits for | reduction |
|---|
Coffman 1971 named the wait-for cycle and the four conditions. Detection asks "is the system already stuck?" — it lets a cycle form, then finds it.
Avoidance refuses to enter the states where a cycle could form at all: the diagnosis here is exactly what the-banker deadlock-avoidance is built to prevent. Each sphere is the next one's premise — the cycle you can detect is the cycle the banker declines to risk.
The blue team's live check: re-verify cycle ↔ deadlock over all 4096 states, and confirm the shipped detector matches ground truth on a scenario battery. If red swaps the cycle test for a timeout, the battery disagrees and this badge turns red.
Three threads T0 T1 T2, three single-instance locks R0 R1 R2. A state is: which lock each thread holds, and which lock each thread is waiting to acquire. That is all the detector needs.
A thread is blocked only if the lock it wants is held by another thread. Feed a state into the engine below — the wait-for edges are read straight off it.
| Coffman condition | status |
|---|
The verdict is reduction ground truth, and it equals cycle-detection — computed on the spot from the state, never looked up.
What the machine proves, exactly: over all 4096 single-instance states of 3 threads / 3 locks, a deadlock exists ⟺ the wait-for graph has a cycle — both directions. Every thread on a cycle is in the deadlocked set; the bipartite resource-allocation graph reduces to the wait-for graph; and imposing a lock ordering (killing circular wait) makes every state acyclic and deadlock-free.
The blue team's witness (left) confirms these facts live; the red team (right) swaps in a timeout and gets caught.
And detection alone does nothing to recover: you still must kill a thread or preempt a lock, both of which lose work. That is why avoidance (the banker) and prevention (ordering) exist upstream.
"A cycle might just be a slow thread." Cut. In a single-instance system a wait-for cycle is exactly deadlock — proven both directions over all 4096 states in the engine.
"Breaking one Coffman condition might help." Cut. All four are necessary together; break any one and deadlock is impossible. The engine verifies it for circular-wait, mutual-exclusion, and hold-and-wait exhaustively.
"Deadlock = the whole system froze." Kept, corrected. Only threads whose wait-chain reaches a cycle are stuck; the rest run on. Reduction reports the exact stuck set.
The red team's move: detect deadlock by a timeout — declare deadlock whenever a thread has waited longer than T — instead of finding a cycle. A thread merely blocked on a busy-but-progressing lock gets falsely flagged.
Swap to the timeout rule and a non-cyclic wait becomes a false positive — the witness (window 7) reruns the scenario battery, disagrees with ground truth, and turns red. Nothing is faked; the attack is real and it is caught.