A review board asks the fabric team: "How do you know it cannot deadlock?" The answer "we ran 10,000 random tests and none hung" is evidence, not an argument: the next traffic pattern may be the one that fills a cycle. The board wants a reason that holds for every possible traffic pattern. That reason has a standard structure.
How do you show, for all traffic, that a system cannot deadlock?
The obvious evidence is testing: lots of random traffic, long runs, stress patterns. Tests find deadlocks; they cannot show there are none, because deadlocks need specific coincidences of traffic that random tests may never produce (lesson 9.6 had one that survived months). What can cover all traffic is an argument about structure: if no cycle of waits can exist, no traffic can create one.
Build the resource dependency graph. Nodes: every buffer, virtual channel, queue, tracker and credit pool. Edges: "a message holding X may wait for Y", from routing (next hop), from message dependencies (a request waits for a response's resources), and from each block's internal waits.
Show the graph is acyclic. Usually by construction: a numbering of resources such that every edge goes from a lower to a higher number (XY routing's dimension order, a dateline's VC 0 → VC 1, message classes ordered request → response).
State the assumptions, and check each one. The consumption assumption (endpoints always accept responses, lesson 9.5); every block obeys the channel dependency rules (lesson 9.3); no resource is shared between classes anywhere.
Cover the edges you cannot remove with a liveness argument. Retry paths need a progress guarantee (protocol credits, lesson 9.7); arbiters need fairness bounds (lesson 8.3).
Tool | Can show | Cannot show |
|---|---|---|
Random and stress simulation | Deadlocks that the tested traffic triggers; performance under load | That none exist for untested traffic |
Protocol checkers (assertions) | That each block obeys its dependency rules in every simulated cycle | System-level cycles between compliant blocks |
Formal property checking | Absence of a deadlock state in a bounded or abstracted model; rule compliance for all inputs of one block | Full SoC-scale proofs directly: state spaces are too large, so models are abstracted and the abstraction must be justified |
The structural argument above | No cycle can exist for any traffic, given the assumptions | Anything about blocks that violate the assumptions |
The strongest position combines them: the structural argument for the fabric, formal or assertion checks that every block meets the assumptions the argument relies on, and stress simulation to catch where the model of the design and the design itself disagree.
A fabric (illustrative) had a sound proof covering routing and message classes, and still deadlocked in silicon. A bridge added late in the project had one shared internal FIFO for requests and responses, a resource the proof's graph never included because the bridge was treated as a wire. The lesson: every block that buffers anything is a node in the graph, and adding a block means re-checking the argument.
Deadlocks need specific coincidences of traffic; simulation shows only that the tested patterns did not deadlock, not that no pattern can.
If every wait goes from a lower number to a higher one, a cycle would need some wait to go downwards, which none does, so no cycle can exist.
Prove deadlock freedom structurally: a complete resource dependency graph shown to be acyclic.
State and check the assumptions: endpoints consume responses, blocks obey dependency rules, classes never share resources.
Add liveness arguments for retries and arbiters; use simulation and formal checks as support, and re-check when blocks change.