# Randomised Mutual Exclusion

(Pnueli & Zuck)

### Introduction

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;
formula some_a	 = p2=14..15 | p3=14..15;
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
```

### Model Statistics

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

### Model Construction Times

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

### Model Checking

When model checking, we have the following requirement:

• Scheduler-Liveness: for each time t and any process Pi not in its remainder phase at time t, 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 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

Conclusion: the property holds in all states
• 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

Conclusion: the property holds in all states.
• 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

Conclusion: the property holds in all states.
• 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

Conclusion: the property holds in all states.