5.1. Dining Philosophers

The dining philosophers problem is a well known and intensely studied problem in concurrent programming. Five philosophers sit around a circular table. Each philosopher has two forks that she shares with her neighbors (giving five forks in total). Philosophers think until they become hungry. A hungry philosopher picks up both forks, one at a time, eats, puts down both forks, and then resumes thinking. Without further refinement, this scenario allows deadlock; if all philosophers become hungry and pick up their left-hand forks simultaneously, no philosopher will be able to pick up her right-hand fork to eat. Lehmann and Rabin's solution [3], which we implement, requires that each philosopher pick up her forks in a random order. If the second fork is not immediately available, the philosopher must set down both forks and try again. While livelock is still possible if all philosophers take forks in the same order, randomization makes this possibility vanishingly unlikely.

{- Dining Philosophers -}

{- Randomly swap order of fork pick-up -}
def shuffle(a,b) = if (Random(2) = 1) then (a,b) else (b,a)

def take((a,b)) =    
  a.acquire() >> b.acquireD() ;
  a.release() >> take(shuffle(a,b))
def drop(a,b) = (a.release(), b.release()) >> signal

{- Define a philosopher -}
def phil(n,a,b) =
  def thinking() = 
    Println(n + " thinking") >> 
    (if (Random(10) <: 9)
      then Rwait(Random(1000))
      else stop)
  def hungry() = take((a,b))
  def eating() = 
    Println(n + " eating") >> 
    Rwait(Random(1000)) >> 
    Println(n + " done eating") >> 
  thinking() >> hungry() >> eating() >> phil(n,a,b)

def philosophers(1,a,b) = phil(1,a,b)
def philosophers(n,a,b) =
  val c = Semaphore(1)
  philosophers(n-1,a,c) | phil(n,c,b)

{- Test the definitions -}
val fork = Semaphore(1)

5 thinking
4 thinking
3 thinking
2 thinking
1 thinking
1 eating
4 eating

The phil function simulates a single philosopher. It takes as arguments two binary semaphores representing the philosopher's forks, and calls the thinking, hungry, and eating functions in a continuous loop. A thinking philosopher waits for a random amount of time, with a 10% chance of thinking forever. A hungry philosopher uses the take function to acquire two forks. An eating philosopher waits for a random time interval and then uses the drop function to relinquish ownership of her forks.

Calling take(a,b) attempts to acquire a pair of forks (a,b) in two steps: wait for fork a to become available, then immediately attempt to acquire fork b. The call b.acquireD() either acquires b and responds immediately, or halts if b is not available. If b is acquired, signal success; otherwise, release a, and then try again, randomly changing the order in which the forks are acquired using the auxiliary function shuffle.

The function call philosophers(n,a,b) recursively creates a chain of n philosophers, bounded by fork a on the left and b on the right. The goal expression of the program calls philosophers to create a chain of five philosophers bounded on the left and right by the same fork; hence, a ring.

This Orc solution has several nice properties. The overall structure of the program is functional, with each behavior encapsulated in its own function, making the program easy to understand and modify. Mutable state is isolated to the "fork" semaphores and associated take and get functions, simplifying the implementation of the philosophers. The program never manipulates threads explicitly, but instead expresses relationships between activities using Orc's combinators.

[3] Daniel Lehmann and Michael O. Rabin. 1981. On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '81). ACM, New York, NY, USA, 133-138.