Concurrency: State Models and Java Programs - page 43

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.

Notes and Further Reading

The Dining Philosophers problem has been widely used to compare both process synchronization primitives and strategies for dealing with deadlock. The problem was introduced by Dijkstra (1968a) in a paper which shows how to use semaphores to solve a variety of synchronization problems. We have used asymmetry to avoid deadlock. A second way to avoid deadlock is to allow at most four philosophers to sit down together at the table. Another approach is to ensure that the act of picking up both forks is atomic. Chandy and Misra (1984) proposed a fully distributed solution which passes tokens between philosophers. All of these approaches to the Dining Philosophers problem are deterministic: each process takes a predetermined set of actions. Lehman and Rabin (1981) showed that any deterministic solution has to be asymmetric or use an outside agent (such as the butler in exercise 6.2). They also presented a probabilistic solution to the problem which is perfectly symmetric. Philosophers toss a coin to determine the order of picking up forks and defer to a neighbor if it has used the fork less recently.

Exercises

6.1 The figure below depicts a maze. Write a description of the maze in FSP which, using deadlock analysis, finds the shortest path out of the maze starting at any square.
( Hint : At each numbered square in the maze, a directional action can be used to indicate an allowed path to another square.)
6.2 One solution to the Dining Philosophers problem permits only four philosophers to sit down at the table at the same time. Specify a BUTLER process which, when composed with the model of section 6.2, permits a maximum of four philosophers to engage in the sitdown action before an arise action occurs. Show that this system is deadlock-free.

6.3 Using the Java timed wait primitive:


public final

void wait(long timeout)

throws

InterruptedException

modify the Fork monitor such that after a wait of 1 second, the call to get times out and returns the result false. The Philosopher should release the other fork, if it holds it, and try again. Observe the behavior of the resulting system.
6.4 It is possible for the following system to deadlock. Explain how this deadlock occurs and relate it to one of the four necessary and sufficient conditions for deadlock to occur.
```
Alice = (call.bob -> wait.chris -> Alice). Bob = (call.chris -> wait.alice -> Bob). Chris = (call.alice -> wait.bob -> Chris). S = (Alice  Bob  Chris) /{call/wait}.
```

The following model attempts to fix the problem by allowing Alice, Bob and Chris to time out from a call attempt. Is a deadlock still possible? If so, describe how the deadlock can occur and give an execution trace leading to the deadlock.

Alice = (call.bob -> wait.chris -> Alice  timeout.alice -> wait.chris ->Alice). Bob = (call.chris -> wait.alice -> Bob  timeout.bob -> wait.alice ->Bob). Chris = (call.alice -> wait.bob -> Chris  timeout.chris -> wait.bob ->Chris). S = (Alice  Bob  Chris) /{call/wait}.