Summary

In this chapter, we have seen that deadlock is a system state in which all of the processes in a system are blocked and the system can consequently make no further progress. Deadlock is modeled by a state with no outgoing transitions. Deadlock analysis of a model involves performing an exhaustive search of the labeled transition system for such states. If none are found, the model is shown to be deadlock-free.

We identified four necessary and sufficient conditions for deadlock. Strategies for dealing with deadlock involve ensuring that at least one of these conditions does not hold. The conditions are:

• Serially reusable resources: the processes involved share resources which they use under mutual exclusion.

• Incremental acquisition: processes hold on to resources already allocated to them while waiting to acquire additional resources.

• No preemption: once acquired by a process, resources cannot be preempted (forcibly withdrawn) but are only released voluntarily.

• Wait-for cycle: a circular chain (or cycle) of processes exists such that each process holds a resource which its successor in the cycle is waiting to acquire.

The Dining Philosophers problem was used to illustrate the point that while deadlocks are easily found in models, they are not so readily apparent in programs. Indeed, the reason for modeling is to remove problems such as deadlock during design.