www.prismmodelchecker.org

Randomised Dining Philosophers

(Lehmann and Rabin)

Contents

Introduction

This case study is based on Lehmann and Rabin's [LR81] randomised solution to the well known dining philosophers problem. Note that this protocol has also been studies in [PZ86]. We consider both the original algorithm and the version presented in [DFP04] which removes the need to consider 'fairness' assumptions on the scheduling mechanism.


Original Algorithm

This algorithm is Lehmann and Rabin's [LR81] solution to the well known dining philosophers problem. The model is represented as an MDP. We let N denotes the number of philosophers. By way of example, the PRISM source code for the original algorithm in the case where N = 3 is given below.

// randomized dining philosophers [LR81]
// dxp/gxn 12/12/99
// atomic formulae 
// left fork free and right fork free resp.
formula lfree = (p2>=0&p2<=4)|p2=6|p2=10;
formula rfree = (p3>=0&p3<=3)|p3=5|p3=7|p3=11;

module phil1

	p1: [0..11];

	[] p1=0 -> (p1'=0); // stay thinking
	[] p1=0 -> (p1'=1); // trying
	[] p1=1 -> 0.5 : (p1'=2) + 0.5 : (p1'=3); // draw randomly
	[] p1=2 &  lfree -> (p1'=4); // pick up left
	[] p1=2 &  !lfree -> (p1'=2); // left not free
	[] p1=3 &  rfree -> (p1'=5); // pick up right
	[] p1=3 &  !rfree -> (p1'=3); // right not free
	[] p1=4 &  rfree -> (p1'=8); // pick up right (got left)
	[] p1=4 & !rfree -> (p1'=6); // right not free (got left)
	[] p1=5 &  lfree -> (p1'=8); // pick up left (got right)
	[] p1=5 & !lfree -> (p1'=7); // left not free (got right)
	[] p1=6  -> (p1'=1); // put down left
	[] p1=7  -> (p1'=1); // put down right
	[] p1=8  -> (p1'=9); // move to eating (got forks)
	[] p1=9  -> (p1'=10); // finished eating and put down left 
	[] p1=9  -> (p1'=11); // finished eating and put down right
	[] p1=10 -> (p1'=0); // put down right and return to think
	[] p1=11 -> (p1'=0); // put down left and return to think

endmodule

// construct further modules through renaming
module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
module phil3 = phil1 [ p1=p3, p2=p1, p3=p2 ] endmodule

// labels
label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8));
label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9));

View: printable version          Download: phil3.nm

Model Statistics

The table below shows statistics for the MDPs we have built for different values of the constants N and K. The tables include:

  • the number of states and transitions in the MDP representing the model;
  • both the number of nodes and leaves of the MTBDD which represents the model;
  • the construction time which equals the time taken for the system description to be parsed and converted to the MTBDD representing it, and the time to perform reachability, identify the non-reachable states and filter the MTBDD accordingly;
  • the number of iterations required to find the reachable states (which is performed via a BDD based fixpoint algorithm).
N:   Model:   MTBDD:   Construction:
States: Transitions: Nodes: Leaves: Time (s): Iter.s:
3 956 3,696 910 30.12418
4 9,440 48,656 1,958 30.14124
5 93,068 599,600 3,335 30.31130
6 917,424 7,092,696 5,008 30.78236
7 9,043,420 81,568,144 6,968 31.56842
8 89,144,512 918,913,056 9,215 32.94248
9 878,732,012 10190,342,448 11,749 35.02554
108,662,001,936111,611,282,28014,570 37.53260
158.06e+15 1.56e+17 32,980 337.8590
207.50e+19 1.93e+21 58,565 3105.3120
256.98e+24 2.24e+26 91,325 31,000150
306.45e+29 2.51e+31 13,126032,719180

Model Checking

When model checking, we have the following requirement:

  • Scheduler-Liveness: "For each time t and any philosopher Pi, there exists a time t' > t in which Pi makes a move."

This corresponds to the conditions on the adversary/scheduler which we impose by model checking against only fair adversaries.

We have model checked the following liveness property: 'If a philosopher is hungry, then eventually some philosopher eats'.

// liveness (if a philosopher is hungry then eventually some philosopher eats)
"hungry" => P>=1 [ true U "eat"]
View: printable version          Download: phil3.pctl
Model checking times:

N:   Precomputation:   Main Algorithm:
Time (s): Iterations: Time (s): Iterations:
3 0.016--
4 0.036--
5 0.076--
6 0.086--
7 0.136--
8 0.176--
9 0.236--
100.296--
150.736--
201.366--
252.206--
305.226--

Conclusion: the property holds in all states


Algorithm Without Fairness Assumptions

This algorithm is the version of Lehmann and Rabin's dining philosopher algorithm presented in [DFP04] and does not require any fairness assumptions. The model is represented as an MDP. We let N denotes the number of philosophers. By way of example, the PRISM source code for the algorithm of [DFP04] in the case of 3 philosophers is given below. The difference between this algorithm and that originally presented by Lehmann and Rabin is that the philosophers cannot be scheduled if their next transition is a 'loop', i.e. such transitions are removed from the model.

// randomized dining philosophers [LR81]
// dxp/gxn 23/01/02

// model which does not require fairness
// remove the possibility of loops:
// (1) cannot stay in thinking 
// (2) if first fork not free then cannot move (another philosopher must more)

mdp

// atomic formulae 
// left fork free and right fork free resp.
formula lfree = (p2>=0&p2<=4)|p2=6|p2=10;
formula rfree = (p3>=0&p3<=3)|p3=5|p3=7|p3=11;

module phil1

	p1: [0..11];

	[] p1=0 -> (p1'=1); // trying
	[] p1=1 -> 0.5 : (p1'=2) + 0.5 : (p1'=3); // draw randomly
	[] p1=2 &  lfree -> (p1'=4); // pick up left
	[] p1=3 &  rfree -> (p1'=5); // pick up right
	[] p1=4 &  rfree -> (p1'=8); // pick up right (got left)
	[] p1=4 & !rfree -> (p1'=6); // right not free (got left)
	[] p1=5 &  lfree -> (p1'=8); // pick up left (got right)
	[] p1=5 & !lfree -> (p1'=7); // left not free (got right)
	[] p1=6  -> (p1'=1); // put down left
	[] p1=7  -> (p1'=1); // put down right
	[] p1=8  -> (p1'=9); // move to eating (got forks)
	[] p1=9  -> (p1'=10); // finished eating and put down left 
	[] p1=9  -> (p1'=11); // finished eating and put down right
	[] p1=10 -> (p1'=0); // put down right and return to think
	[] p1=11 -> (p1'=0); // put down left and return to think

endmodule

// construct further modules through renaming
module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
module phil3 = phil1 [ p1=p3, p2=p1, p3=p2 ] endmodule

// rewards (number of steps)
rewards "num_steps"
	[] true : 1;
endrewards
// labels
label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8));
label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9));


View: printable version          Download: phil-nofair3.nm

Model Statistics

The table below shows statistics for the MDPs we have built for different values of the constants N and K. The tables include:

  • the number of states and transitions in the MDP representing the model;
  • both the number of nodes and leaves of the MTBDD which represents the model;
  • the construction time which equals the time taken for the system description to be parsed and converted to the MTBDD representing it, and the time to perform reachability, identify the non-reachable states and filter the MTBDD accordingly;
  • the number of iterations required to find the reachable states (which is performed via a BDD based fixpoint algorithm).
N:   Model:   MTBDD:   Construction:
States: Transitions: Nodes: Leaves: Time (s): Iter.s:
3 956 3,048 765 30.06518
4 9,440 40,120 1,650 30.12124
5 93,068 494,420 2,854 30.25930
6 917,424 5,848,524 4,339 30.61236
7 9,043,420 67,259,808 6,101 31.18 42
8 89,144,512 757,721,264 8,150 32.31 48
9 878,732,012 8,402,796,252 10,48633.74 54
108,662,001,93692,032,909,54013,10935.83 60

Model Checking

We have model checked the following properties:

const int K; // discrete time bound

// liveness (if a philosopher is hungry then eventually some philosopher eats)
"hungry" => P>=1 [ true U "eat"]

// bounded waiting (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps)
Pmin=?[true U<=K "eat" {"hungry"}{min}]

// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats)
Rmax=?[F "eat" {"hungry"}{max}]
View: printable version          Download: phil-nofair3.pctl
  • Liveness: the model checking statistics for this property are given below.

    N:   Precomputation:   Main Algorithm:
    Time (s): Iterations: Time (s): Iterations:
    3 0.03 20 --
    4 0.34 34 --
    5 1.70 54 --
    6 8.20 74 --
    7 33.2 100--
    8 122 130--
    9 818 166--
    101,673202--

    Conclusion: the property holds in all states
  • Bounded waiting: in the graph below we have plotted these probabilities as L varies for a range of values of N.

    plot: the minimum probability of some philosopher eating within L steps
  • Expected time: in the graph below we have plotted these expected values as N varies.

    plot: maximum expected number of steps until between a philosopher becoming hungry and some philosopher eating

Case Studies