Mutexes and deadlock

Each card is a thread with its steps; the highlighted step runs next. Click a card to run that thread's next step, as if the scheduler picked it. A thread waiting for a lock someone else holds is blocked and cannot be clicked. The wait-for graph on the right updates after every step.

• With Opposite order, click T1 once and T2 once: each holds one lock and wants the other's. Or press Shortest way to deadlock.
• Switch to Same order and try to reach a deadlock: the exploration panel confirms there is no state where it happens.
• Open Dining philosophers: of billions of possible schedules, only a few hundred deadlock, yet a scheduler picking threads at random deadlocks in 15.8% of runs.

The exploration is a small model checker: it visits every state reachable by any choice of thread at every step. Its schedule counts match a brute-force walk over every interleaving, and every deadlock it finds has a cycle in the wait-for graph.

A deadlock is a state in which a group of threads, processes or transactions are each waiting for something that another member of the group holds, so none of them can ever proceed. The classic case is two threads and two mutexes: thread 1 holds lock A and waits for B, thread 2 holds B and waits for A.

Unlike most bugs, a deadlock does not corrupt anything; the program simply stops making progress, usually without an error message. It depends on timing, so it can pass every test and appear only under load.

Coffman, Elphick and Shoshani's 1971 survey "System Deadlocks" gave the conditions that must all hold for a deadlock:

1. Mutual exclusion: a resource can be held by only one thread at a time.
2. Hold and wait: a thread holds resources while waiting for more.
3. No preemption: a resource cannot be taken from its holder; only the holder releases it.
4. Circular wait: there is a cycle of threads, each waiting for a resource held by the next.

Every prevention technique breaks one of them. Mutexes exist to provide mutual exclusion, so in practice the target is usually circular wait or hold and wait.

A deadlock needs the threads to interleave in a particular way. The model checker counts the possibilities for each program on this page:

• Lock ordering. Give every lock a rank and always acquire in increasing rank. No cycle can form, which removes circular wait. The fixed dining philosophers do exactly this: the last philosopher takes the higher-numbered fork first. For locks that have no natural order, such as two bank accounts, order them by an ID or address.
• Trylock and back off. Take the first lock, try the second, and if it is busy release the first and start again. This breaks hold and wait, but two threads can keep colliding and retrying in step, a livelock; adding a random delay before retrying makes that unlikely.
• Take everything at once, or use one coarser lock, at the cost of less concurrency.
• Timeouts on lock acquisition turn a hang into an error the program can handle.
• Avoidance: Dijkstra's banker's algorithm grants a request only if the system stays in a state where every thread can still finish. It needs to know maximum demands in advance, so it is rare outside textbooks.

Systems that cannot rule deadlocks out detect them instead. Database engines build a wait-for graph among transactions and abort one transaction in any cycle; PostgreSQL runs the check once a transaction has waited longer than deadlock_timeout, one second by default. The Linux kernel's lockdep validator records the order in which every class of lock is ever taken and reports a possible deadlock the first time it sees two orders that could form a cycle, even if the deadlock did not happen on that run. The Go runtime aborts with "all goroutines are asleep - deadlock!" when no goroutine can run.

Edsger Dijkstra studied deadlock (he called it "deadly embrace") in the 1960s while designing the THE multiprogramming system, devised the banker's algorithm, and set the dining philosophers problem as an exercise. His 1971 paper "Hierarchical ordering of sequential processes" presents it: one semaphore per fork "contains the danger of the deadly embrace", and his fix lets a philosopher start eating only when neither neighbour is eating. Breaking the cycle by ordering resources was proposed by J. W. Havender at IBM in 1968. Coffman, Elphick and Shoshani's survey of the same year named the four necessary conditions.