www.prismmodelchecker.org

Randomised Mutual Exclusion

(Pnueli & Zuck)

Contents

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;
// 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
View: printable version          Download: mutual3.nm

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,3681,8023
4 27,6004,1003
5 308,8007,1493
8 3.9x10820,7363
10 4.4x101033,4943

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.580.1322
4 0.670.4828
5 0.721.2334
8 1.099.0252
10 1.4419.564

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) ]
View: printable version          Download: mutual3.pctl
  • Theorem 1 from [PZ86] (Mutual Exclusion): the model checking statistics for this property are given below.

    N:   Time (s):
    30.03
    40.04
    50.05
    80.08
    100.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:
    30.262700
    41.323600
    54.634500
    847.37200
    101279000

    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:
    30.111000
    40.521200
    51.301400
    83.872000
    106.082400

    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:
    30.232200
    41.132900
    53.353700
    828.56100
    1076.37700

    Conclusion: the property holds in all states.

Case Studies