The problem of the dining philosophers

The problem of the dining philosophers is a classical problem in the field of concurrent programming. It offers an entertaining vehicle for comparing various formalisms for writing and proving concurrent programs, because it is sufficiently simple to be tractable yet subtle enough to be challenging.

The problem is set in a secluded community of five philosophers who engage in only two activities—thinking and eating:

Meals are taken communally at a table set with five plates and five forks (Figure 6.3). In the center of the table is a bowl of spaghetti that is endlessly replenished. Unfortunately, the spaghetti is hopelessly tangled and a philosopher needs two forks in order to eat.” Each philosopher may pick up the forks on his left and right, but only one at a time. The problem is to design pre and post protocols to ensure that a philosopher only eats if she has two forks. The solution should also satisfy the correctness properties that we described in the chapter on mutual exclusion.

The correctness properties are:

  • A philosopher eats only if she has two forks.

  • Mutual exclusion: no two philosophers may hold the same fork simultaneously.

  • Freedom from deadlock.

  • Freedom from starvation (pun!).

  • Efficient behavior in the absence of contention.

Here is a first attempt at a solution, where we assume that each philosopher is initialized with its index i, and that addition is implicitly modulo 5.

Each fork is modeled as a semaphore: wait corresponds to taking a fork and signal corresponds to putting down a fork. Clearly, a philosopher holds both forks before eating.

Theorem 6.3 No fork is ever held by two philosophers.

Proof: Let \(P_i\) be the number of philosophers holding fork i, so that \(P_i = wait(fork[i]) - signal(fork[i])\). By the semaphore invariant (6.2), \(fork[i] = 1 + (-P_i)\), or \(P_i = 1 - fork[i]\). Since the value of a semaphore is non-negative (6.1), we conclude that \(P_i \leq 1 \)

Unfortunately, this solution deadlocks under an interleaving that has all philosophers pick up their left forks—execute \(wait(fork[i])\) before any of them tries to pick up a right fork. Now they are all waiting on their right forks, but no process will ever execute a signal operation.

One way of ensuring liveness in a solution to the dining philosophers problem is to limit the number of philosophers entering the dining room to four:

The addition of the semaphore room obviously does not affect the correctness of the safety properties we have proved.

Theorem 6.4 The algorithm is free from starvation.

Proof: We must assume that the semaphore room is a blocked-queue semaphore so that any philosopher waiting to enter the room will eventually do so. The fork semaphores need only be blocked-set semaphores since only two philosophers use each one. If philosopher i is starved, she is blocked forever on a semaphore. There are three cases depending on whether she is blocked on \(fork[i]\), \(fork[i+1]\) or room.

Case 1: Philosopher i is blocked on her left fork. Then philosopher \( i - 1 \) holds \(fork[i]\) as her right fork, that is, philosopher \( i - 1 \) has successfully executed both her wait statements and is either eating, or about to signal her left or right fork semaphores. By progress and the fact that there are only two processes executing operations on a fork semaphore, eventually she will release philosopher i.

Case 2: Philosopher \(i\) is blocked on her right fork. This means that philosopher \( i + 1 \) has successfully taken her left fork \((fork[i+1])\) and will never release it. By progress of eating and signaling, philosopher \( i + 1 \) must be blocked forever on her right fork. By induction, it follows that if i is blocked on her right fork, then so must all the other philosophers: \( i + j, 1 < j < 4 \). However, by the semaphore invariant on room, for some \(i\), philosopher \(i + j\) is not in the room, thus obviously not blocked on a fork semaphore.

Case 3: We assume that the room semaphore is a blocked-queue semaphore, so philosopher i can be blocked on room only if its value is zero indefinitely. By the semaphore invariant, there are at most four philosophers executing the statements between wait(room) and signal(room). The previous cases showed that these philosophers are never blocked indefinitely, so one of them will eventually execute signal(room). I

Another solution that is free from starvation is an asymmetric algorithm, which has the first four philosophers execute the original solution, but the fifth philosopher waits first for the right fork and then for the left fork:

Again it is obvious that the correctness properties on eating are satisfied. Proofs of freedom from deadlock and freedom from starvation are similar to those of the previous algorithm and are left as an exercise.

A solution to the dining philosophers problem by Lehmann and Rabin uses random numbers. Each philosopher “flips a coin” to decide whether to take her left or right fork first. It can be shown that with probability one no philosopher starves [48, Section 11.4].