Deadlock 2026-10-14
A group of participants cannot proceed because each waits for a resource whose release depends on another participant in the group. Consider two initially free mutex objects A and B. T1 acquires A then tries B; T2 acquires B then tries A. If each obtains its first mutex, both wait permanently for the other, with release reachable only after the second acquisition. Each mutex still enforces mutual exclusion.[ref]
Common Concurrency Problems. pp. 5–7, figures 32.6–32.7: opposing acquisition orders and circular wait
Reachable states for opposite mutex acquisition orders and for one shared lock ordering
. Details. Each software thread performs four indivisible operations: acquire its first mutex, acquire its second, release the second, release the first. An unavailable acquisition blocks; neither participant releases early. A state records each participant's completed-operation count and both owners. Exhaustive exploration finds 19 reachable states with opposite orders, including exactly one nonterminal state with no enabled operation: both counts are , T1 owns A, and T2 owns B. Giving both participants the order A then B leaves 16 reachable states and no such blocked state. Unshown grid positions are unreachable. These are tiny sequential consistency models, without timeouts, cancellation, recursive acquisition or other resources.
