(Pnueli & Zuck)
This case study is based on Pnueli and Zuck's [PZ86] probabilistic symmetric solution to the n-process mutual exclusion problem. The model is represented as an MDP. We let N denotes the number of processes. By way of example, the PRISM source code for the case where N = 3 is given below.
// mutual exclusion [PZ82] // dxp/gxn 19/12/99 mdp // atomic formula // none in low, high, tie formula none_lht = p2!=4..13 & p3!=4..13; // some in admit formula some_a = p2=14..15 | p3=14..15; // some in high, admit formula some_ha = p2=4..5,10..15 | p3=4..5,10..15; // none in high, tie, admit formula none_hta = p2=0..3,7..8 & p3=0..3,7..8; // none in enter formula none_e = p2!=2..3 & p3!=2..3; // process 1 module process1 p1: [0..15]; [] p1=0 -> (p1'=0); [] p1=0 -> (p1'=1); [] p1=1 -> (p1'=2); [] p1=2 & (none_lht | some_a) -> (p1'=3); [] p1=2 & !(none_lht | some_a) -> (p1'=2); [] p1=3 -> (p1'=4); [] p1=3 -> (p1'=7); [] p1=4 & some_ha -> (p1'=5); [] p1=4 & !some_ha -> (p1'=10); [] p1=5 -> (p1'=6); [] p1=6 & some_ha -> (p1'=6); [] p1=6 & !some_ha -> (p1'=9); [] p1=7 & none_hta -> (p1'=8); [] p1=7 & !none_hta -> (p1'=7); [] p1=8 -> (p1'=9); [] p1=9 -> 0.5 : (p1'=4) + 0.5 : (p1'=7); [] p1=10 -> (p1'=11); [] p1=11 & none_lht -> (p1'=13); [] p1=11 & !none_lht -> (p1'=12); [] p1=12 -> (p1'=0); [] p1=13 -> (p1'=14); [] p1=14 & none_e -> (p1'=15); [] p1=14 & !none_e -> (p1'=14); [] p1=15 -> (p1'=0); endmodule // construct further modules through renaming module process2 = process1 [p1=p2, p2=p1] endmodule module process3 = process1 [p1=p3, p3=p1] endmodule
The table below shows statistics for each model we have built. The first section gives the number of states in the MDP representing the model. The second part refers to the MTBDD which represents this MDP: the total number of nodes and the number of leaves (terminal nodes).
| N: | Model: | MTBDD: | |||
| States: | Nodes: | Leaves: | |||
| 3 | 2,368 | 1,802 | 3 | ||
| 4 | 27,600 | 4,100 | 3 | ||
| 5 | 308,800 | 7,149 | 3 | ||
| 8 | 3.9x108 | 20,736 | 3 | ||
| 10 | 4.4x1010 | 33,494 | 3 | ||
The table below gives the times taken to construct the models. There are two stages. Firstly, the system description (in our module based language) is parsed and converted to the MTBDD representing it. Secondly, reachability is performed to identify non-reachable states and the MTBDD is filtered accordingly. Reachability is performed using a BDD based fixpoint algorithm. The number of iterations for this process is also given.
| N: | Construction: | Reachability: | |||
| Time (s): | Time (s): | Iter.s: | |||
| 3 | 0.58 | 0.13 | 22 | ||
| 4 | 0.67 | 0.48 | 28 | ||
| 5 | 0.72 | 1.23 | 34 | ||
| 8 | 1.09 | 9.02 | 52 | ||
| 10 | 1.44 | 19.5 | 64 | ||
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 properties:
// theorem 1 (mutual exclusion) !((p1>9) & (p2>9)) & !((p1>9) & (p3>9)) & !((p2>9) & (p3>9)) // theorem 2 (liveness - if process 1 tries then eventually it enters the critical section) (p1=1) => P>=1 [ true U (p1=10) ] // lemma c (if the crical section is occupied then eventually it becomes clear) (p1>9) | (p2>9) | (p3>9) => P>=1 [ true U (p1<10) & (p2<10) & (p3<10) ] // lemma d (if a process is between 4 and 13 (in our version) then eventually some process gets to 14) ((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) => P>=1 [ true U (p1=14) | (p2=14) | (p3=14) ]
Theorem 1 from [PZ86] (Mutual Exclusion): the model checking statistics for this property are given below.
| N: | Time (s): | |
| 3 | 0.03 | |
| 4 | 0.04 | |
| 5 | 0.05 | |
| 8 | 0.08 | |
| 10 | 0.11 |
Theorem 2 from [PZ86] (Liveness): the model checking statistics for this property are given below.
| N: | Precomputation: | Main Algorithm: | ||||
| Time (s): | Iterations: | Time (s): | Iterations: | |||
| 3 | 0.26 | 27 | 0 | 0 | ||
| 4 | 1.32 | 36 | 0 | 0 | ||
| 5 | 4.63 | 45 | 0 | 0 | ||
| 8 | 47.3 | 72 | 0 | 0 | ||
| 10 | 127 | 90 | 0 | 0 | ||
Lemma C from [PZ86]: the model checking statistics for this property are given below.
| N: | Precomputation: | Main Algorithm: | ||||
| Time (s): | Iterations: | Time (s): | Iterations: | |||
| 3 | 0.11 | 10 | 0 | 0 | ||
| 4 | 0.52 | 12 | 0 | 0 | ||
| 5 | 1.30 | 14 | 0 | 0 | ||
| 8 | 3.87 | 20 | 0 | 0 | ||
| 10 | 6.08 | 24 | 0 | 0 | ||
Lemma D from [PZ86]: the model checking statistics for this property are given below.
| N: | Precomputation: | Main Algorithm: | ||||
| Time (s): | Iterations: | Time (s): | Iterations: | |||
| 3 | 0.23 | 22 | 0 | 0 | ||
| 4 | 1.13 | 29 | 0 | 0 | ||
| 5 | 3.35 | 37 | 0 | 0 | ||
| 8 | 28.5 | 61 | 0 | 0 | ||
| 10 | 76.3 | 77 | 0 | 0 | ||