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?