6.2 Dining Philosophers Problem

6.2 Dining Philosophers Problem

The Dining Philosophers problem (Dijkstra, 1968a) is a classic concurrent-programming problem in which the deadlock is not quite so apparent as in the previous examples. We develop both the model and Java implementation. The problem is stated as follows: five philosophers share a circular table (as depicted in Figure 6.5) at which they have allotted seats. Each philosopher spends his life alternately thinking and eating. In the center of the table is a large plate of tangled spaghetti. A philosopher needs two forks to eat a helping of spaghetti. Unfortunately, as philosophy is not as well paid as computing, the philosophers can only afford five forks. One fork is placed between each pair of philosophers and they agree that each will only use the forks to his immediate right and left.

Figure 6.5: The Dining Philosophers table.

The resources in this system are the forks shared between the philosophers. We model a fork in the same way that we modeled the scanner and printer resources in the previous section:

 FORK = (get -> put -> FORK).

To use a fork, a philosopher must first pick up (get) that fork and when finished with the fork, the philosopher puts it down (put). Each philosopher is modeled by the process:

 PHIL = (sitdown->right.get->left.get           ->eat->left.put->right.put           ->arise->PHIL).

In other words, when a philosopher becomes hungry, he (or she) sits down at the table, picks up the fork to his right, if it is free, and then picks up the fork to his left, if it is free. The philosopher can then eat. When finished eating, the philosopher releases the forks and leaves the table. The Dining Philosophers system can now be described by the composition of five fork processes and five philosopher processes as depicted in Figure 6.6.

Figure 6.6: Dining Philosophers composite model.

The diagram of Figure 6.6 can be expressed concisely as the composite process:

 ||DINERS(N=5)=    forall [i:0..N-1]    (phil[i]:PHIL    || {phil[i].left,phil[((i-1)+N)%N].right}::FORK).

The expression ((i-1)+N)%N is subtraction modulo N so that, for example, a fork is shared between phil[0] and phil[4]. Analysis of this system reveals the following deadlock:

 Trace to DEADLOCK:      phil.0.sitdown      phil.0.right.get      phil.1.sitdown      phil.1.right.get      phil.2.sitdown      phil.2.right.get      phil.3.sitdown      phil.3.right.get      phil.4.sitdown      phil.4.right.get

This is the situation where all the philosophers become hungry at the same time, sit down at the table and then each philosopher picks up the fork to his (or her) right. The system can make no further progress since each philosopher is waiting for a fork held by his neighbor. In other words, a wait-for cycle exists, as described in the introduction.

6.2.1 Dining Philosophers Implementation

It is generally not a good idea to implement an erroneous model. However, in this section, our objective is to show that, while deadlock can be detected easily in a model, it is not so apparent in the running program which corresponds to that model. In translating the Dining Philosophers model into an implementation, we must consider which processes in the model will be represented by passive objects (monitors) and which by active objects (threads), as outlined in the previous chapter. The decision is reasonably obvious; forks are the passive entities and philosophers are the active entities in this system.

The relationships between the various classes involved in the Dining Philosophers program is shown in the class diagram of Figure 6.7.

Figure 6.7: Dining Philosophers class diagram.

The display is implemented by the PhilCanvas class. The interface offered by this class is given in Program 6.1.

Program 6.1: Outline of PhilCanvas class.

 class PhilCanvas extends Canvas {   // set state of philosopher id to display state s,   // method blocks calling thread if display is frozen   synchronized void setPhil(int id,int s)         throws java.lang.InterruptedException{}   // "freeze" display   synchronized void freeze(){}   // "un-freeze" display   synchronized void thaw() {}   // set state of fork id to taken   synchronized void setFork(int id, boolean taken){} }

The Java implementation of the Fork monitor is listed in Program 6.2. The boolean variable, taken, encodes the state of the fork. When the fork is on the table, taken is false. When the fork has been picked up by a philosopher, taken is true.

Program 6.2: Fork monitor.

 class Fork {   private boolean taken=false;   private PhilCanvas display;   private int identity;   Fork(PhilCanvas disp, int id)     { display = disp; identity = id;}   synchronized void put() {     taken=false;     display.setFork(identity,taken);     notify();   }   synchronized void get()      throws java.lang.InterruptedException {     while (taken) wait();     taken=true;     display.setFork(identity,taken);   } }

The code for the Philosopher thread is listed in Program 6.3. It follows directly from the model. The detail of the philosopher sitting down and leaving the table has been omitted; philosophers think while sitting at the table.

Program 6.3: Philosopher thread class.

 class Philosopher extends Thread {   private int identity;   private PhilCanvas view;   private Diners controller;   private Fork left;   private Fork right;   Philosopher(Diners ctr,int id,Fork l,Fork r){     controller = ctr; view = ctr.display;     identity = id; left = l; right = r;   }   public void run() {     try {       while (true) {         // thinking         view.setPhil(identity,view.THINKING);         sleep(controller.sleepTime());         // hungry         view.setPhil(identity,view.HUNGRY);         right.get();         // gotright fork         view.setPhil(identity,view.GOTRIGHT);         sleep(500);         left.get();         // eating         view.setPhil(identity,view.EATING);         sleep(controller.eatTime());         right.put();         left.put();       }     } catch (java.lang.InterruptedException e){}   } }

The time that a philosopher spends thinking and eating is controlled by the slider in the applet display (Figure 6.8).

Figure 6.8: Dining Philosophers applet – executing.

The code to create the Philosopher threads and Fork monitors is:

 for (int i =0; i<N; ++i)   fork[i] = new Fork(display,i); for (int i =0; i<N; ++i){   phil[i] =     new Philosopher(this,i,fork[(i-1+N)%N],fork[i]);   phil[i].start(); }

Figure 6.8 depicts the Dining Philosophers applet running. The applet may run for a long time before deadlock occurs. To ensure deadlock occurs eventually, the slider control may be moved to the left. This reduces the time philosophers spend thinking and eating and this “speedup” increases the probability of deadlock occurring. Figure 6.9 depicts the applet when deadlock occurs. It is clear that each philosopher is holding on to the fork on his right.

Figure 6.9: Dining Philosophers applet – deadlocked.

6.2.2 Deadlock-Free Philosophers

There are many different solutions to the Dining Philosophers problem. Some of these are referenced in Notes and Further Reading at the end of this chapter. All of the solutions involve denying one of the four necessary and sufficient conditions for deadlock identified at the beginning of the chapter. The solution we outline here depends on ensuring that a wait-for cycle cannot exist. To do this, we introduce some asymmetry into the definition of a philosopher. Up to now, each philosopher has had an identical definition. We make odd-numbered philosophers get the right fork first and even-numbered philosophers get the left fork first. The revised model is listed below:

 FORK = (get -> put -> FORK). PHIL(I=0)     = (when (I%2==0) sitdown          ->left.get->right.get          ->eat->left.put->right.put->arise->PHIL       |when (I%2==1) sitdown          ->right.get->left.get          ->eat->left.put->right.put->arise->PHIL       ). ||DINERS(N=5)=    forall [i:0..N-1]    (phil[i]:PHIL(i)    || {phil[i].left,phil[((i-1)+N)%N].right}::FORK).

This specification for the Dining Philosophers is deadlock-free since it is no longer possible for the wait-for cycle to exist, in which each philosopher holds the right fork. The reader should verify using LTSA that the above model is in fact deadlock-free. The same change can of course be made to the Java implementation and the result is a deadlock-free program.