CSCI P545 Computer Science Department Indiana University Thu Feb 7 17:00:44 EST 2008 © [SDJ]

The Dining Philosophers Problem

The Dining Philosophers problems is a classic synchronization problem (E. W. Dijkstra. Co-operating Sequential Processes. In F. Genuys (ed.) Programming Languages, Academic Press, London, 1965) introducing semaphores as a conceptual synchronization mechanism. The problem is discussed in just about every operating systems textbook.

Dining Philosophers. There is a dining room containing a circular table with five chairs. At each chair is a plate, and between each plate is a single fork (originally a chopstick). In the middle of the table is a bowl of spaghetti. Near the room are five philosophers who spend most of their time thinking, but who occasionally get hungry and need to eat so they can think some more. In order to eat, a philosopher must sit at the table, pick up the two forks to the left and right of the plate, then serve and eat the spaghetti on the plate.

Thus, each philosopher is represented by the following pseudocode:

        process P[i]
          while true do
            { THINK;
              PICKUP(FORK[i], FORK[i+1 mod 5]);
              EAT;
              PUTDOWN(FORK[i], FORK[i+1 mod 5])
             }

A philosopher may THINK indefinately. Every philosopher who EATs will eventually finish. Philosophers may PICKUP and PUTDOWN their forks in either order, or nondeterministically, but these are atomic actions, and, of course, two philosophers cannot use a single FORK at the same time.

The problem is to design a protocol to satisfy the liveness condition: any philosopher who tries to EAT, eventually does.

Discussion. Of course, the best thing is to go off and try to solve this problem on your own by exploring various protocols philosophers might use to acquire forks. You are likely to quickly encounter the same deadlock and livelock scenarios we saw in the mutual exclusion problem, but you will quickly see in this case that mutual exclusion is too primitive a synchronization mechanism for solving this problem.

In his textbook Modern Operating Systems (Prentice-Hall, 1992) Tannenbaum gives the pseudo-code for a solution to the dining philosophers problem that is shown below. Similar solutions are found in most operating systems textbooks. All of them are renditions of the original treatment by Dijkstra, which motivated the semaphore mechanism he was introducing in his original article. A \emph{semaphore} is an integer or boolean value, S, with two associated atomic operations:

DOWN(S) wait until S > 0, then decrement S;
UP(S) increment S

In time-sharing systems, "waiting" is implemented by the operating system, which may put processes on a wait-list for later execution. In hardware, "waiting" may be accomplished by busy-waiting or by some form of explicit signaling, such as token passing.

Tannenbaum's Solution. This solution uses only boolean semaphors. There is one global semaphore to provide mutual exclusion for exectution of critical protocols. There is one semaphore for each fork. In addition, a local two-phase prioritization scheme is used, under which philosophers defer to their neighbors who have declared themselves "hungry." All arithmetic is modulo 5.

system DINING_PHILOSOPHERS

VAR
me:    semaphore, initially 1;                    /* for mutual exclusion */
s[5]:  semaphore s[5], initially 0;               /* for synchronization */
pflag[5]: {THINK, HUNGRY, EAT}, initially THINK;  /* philosopher flag */

As before, each philosopher is an endless cycle of thinking and eating.

procedure philosopher(i)
  {
    while TRUE do
     {
       THINKING;
       take_forks(i);
       EATING;
       drop_forks(i);
     }
  }

The take_forks procedure involves checking the status of neighboring philosophers and then declaring one's own intention to eat. This is a two-phase protocol; first declaring the status HUNGRY, then going on to EAT.

procedure take_forks(i)
  {
    DOWN(me);               /* critical section */
    pflag[i] := HUNGRY;
    test[i];
    UP(me);                 /* end critical section */
    DOWN(s[i])              /* Eat if enabled */
   }

void test(i)            /* Let phil[i] eat, if waiting */
  {
    if ( pflag[i] == HUNGRY
      && pflag[i-1] != EAT
      && pflag[i+1] != EAT)
       then
        {
          pflag[i] := EAT;
          UP(s[i])
         }
    }

Once a philosopher finishes eating, all that remains is to relinquish the resources---its two forks---and thereby release waiting neighbors.

void drop_forks(int i)
  {
    DOWN(me);                /* critical section */
    test(i-1);               /* Let phil. on left eat if possible */
    test(i+1);               /* Let phil. on rght eat if possible */
    UP(me);                  /* up critical section */
   }

The protocol is fairly elaborate, and Tannenbaum's presentation is made more subtle by its coding style.

A Simpler Solution. Other authors, including Dijkstra, have posed simpler solutions to the dining philosopher problem than that proposed by Tannenbaum (depending on one's notion of "simplicity," of course). One such solution is to restrict the number of philosophers allowed access to the table. If there are N forks but only N-1 philosophers allowed to compete for them, at least one will succeed, even if they follow a rigid sequential protocol to acquire their forks.

This solution is implemented with an integer semaphore, initialized to N-1. Both this and Tannenbaum's solutions avoid deadlock a situation in which all of the philosophers have grabbed one fork and are deterministically waiting for the other, so that there is no hope of recovery. However, they may still permit starvation, a scenario in which at least one hungry philosopher never gets to eat.

Starvation occurs when the asynchronous semantics may allow an individual to eat repeatedly, thus keeping another from getting a fork. The starving philosopher runs, perhaps, but doesn't make progress. The observation of this fact leads to some further refinement of what fairness means. Under some notions of fairness the solutions given above can be said to be correct.