Dining Philosophers Deadlock Example Using Bluespec

The dining philosophers were invented in 1965 by Edsger Dijkstra and the problem they pose has become the classical example of a system that is liable to deadlock.



Five philosophers are evenly spaced around a round table.   Each has a bowl of soup but there are only five spoons and each needs (for some strange reason) two spoons to eat.  So they cannot all eat at once, but must take it in turns.



In Bluespec Verilog, a spoon is easily coded as follows. The pickup method is blocking, so any philosopher attempting to pickup a fork that is already held by his neighbour will wait until his neighbour puts it down.

interface Spoon_if;
  method Action pickup();
  method Action putdown();
endinterface

module spoon (Spoon_if) ;

  Reg#(Bool) inuse <- mkReg(?);

  method Action pickup() if (!inuse);
   action
     inuse <= True;
   endaction
  endmethod

  method Action putdown();
   action
     inuse <= False;
   endaction
  endmethod

endmodule 

The complete system can be described as follows:

(*synthesize *)
module philoBENCH (Empty) ;

       Spoon_if spoon0 <- spoon;
       Spoon_if spoon1 <- spoon;
       Spoon_if spoon2 <- spoon;
       Spoon_if spoon3 <- spoon;
       Spoon_if spoon4 <- spoon;

       Diner_if din0 <- mkDiner (3, 7, spoon0, spoon1);
       Diner_if din1 <- mkDiner (4, 4, spoon1, spoon2);
       Diner_if din2 <- mkDiner (2, 9, spoon2, spoon3);
       Diner_if din3 <- mkDiner (3, 6, spoon3, spoon4);
       Diner_if din4 <- mkDiner (3, 6, spoon4, spoon0);

endmodule: philoBENCH

And the behaviour of an individual philosopher can be coded as follows:

module mkDiner #(UInt#(15) on, UInt#(15) seed) (Spoon_if left, Spoon_if right, Diner_if i);

  Reg#(Bool) eating <- mkReg(?);
  Reg#(UInt#(15)) timer <- mkReg(0);

  Random_if gen <- mkRandom_gen(seed);

  rule foo (timer != 0);
     timer <= timer - 1;
  endrule


  Stmt seq_behaviour =
  (seq while (True) seq
     action UInt#(15) x <- gen.gen(); timer<=x & 31; endaction await(timer== 0);

     left.pickup();
     noAction;

     action UInt#(15) x <- gen.gen(); timer<=x & 31; endaction await(timer== 0);

     right.pickup();

     eating <= True;
     timer <= on; await(timer==0);
     eating <= False;

     noAction;

     left.putdown();
     noAction;
     right.putdown();
     noAction;
  endseq endseq);

  FSM fsm <- mkFSM (seq_behaviour);

  rule kickoff  ;
     fsm.start;
  endrule


endmodule

What happens ?

Not suprisingly, after a little while the system reaches deadlock, as shown in this waveform trace:

The obvious source of deadlock is that each philosopher first picks up his left fork and then tries for his right.  This is clearly a bad policy: in concurrency terms, each spoon is a lock and the resulting cyclic ring of dependencies is known as a `knot' in the lock graph.


The Solution ?

There are many solutions the problem:  one that appears to work is for one philosopher to first pick up his right fork.  We change the system configuration as follows:

       Diner_if din0 <- mkDiner (3, 7, spoon0, spoon1);
       Diner_if din1 <- mkDiner (4, 4, spoon1, spoon2);
       Diner_if din2 <- mkDiner (2, 9, spoon3, spoon2); // <-- Spoon swap!
       Diner_if din3 <- mkDiner (3, 6, spoon3, spoon4);
       Diner_if din4 <- mkDiner (3, 6, spoon4, spoon0);

Now when we run the system, it does not seem to lock up however long we simulate for. Here's some example output:

A good and permanent fix ?

But can we be sure this system is now deadlock free?