Randomised Mutual Exclusion

(Rabin)

Contents

• Introduction
• The Model
• Model Checking

Introduction

This case study is based on Rabin's solution to the well known mutual exclusion problem [Rab82].

Let P₁ ... P_n be n processes that from time to time need to execute a critical section in which exactly one of them is allowed to employ a shared resource. The processes can coordinate their activities by use of a common resource.

A solution to this problem is an algorithm that guarantees freedom from deadlock and freedom from lockout.

The Model

The model is represented as an MDP. We let N denotes the number of processes. The PRISM source code for the case where N = 3 is show below:

// N-processor mutual exclusion [Rab82]
// with global variables to remove sychronization 
// gxn/dxp 02/02/00

mdp

// size of shared counter
const int K = 6; // 4+ceil(log_2 N)

// global variables (all modules can read and write)
// c=0 critical section free
// c=1 critical section not free
// b current highest draw
// r current round 

global c : [0..1];
global b : [0..K];
global r : [1..2];

// local variables: process i 
// state: pi
//  0 remainder
//  1 trying
//  2 critical section
// current draw: bi
// current round: ri

// atomic formula for process 1 drawing
formula draw = p1=1 & (b<b1 | r!=r1);

module process1

	p1 : [0..2];
	b1 : [0..K];
	r1 : [0..2];

	// remain in remainder
	[] p1=0 -> (p1'=0);
	// enter trying
	[] p1=0 -> (p1'=1);
	// make a draw
	[] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1))
	         + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2))
	         + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3))
	         + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4))
	         + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5))
	         + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6));
	// enter critical section and randomly set r to 1 or 2
	[] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2)
	                             + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2);
	// loop when trying and cannot make a draw or enter critical section
	[] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1);
	// leave crictical section
	[] p1=2 -> (p1'=0) & (c'=0);
	// stay in critical section
	[] p1=2 -> (p1'=2);
	
endmodule

// construct further modules through renaming
module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule
module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule

// formulas/labels for use in properties:

// number of processes in critical section
formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0);

// one of the processes is trying
label "one_trying" = p1=1|p2=1|p3=1;

// one of the processes is in the critical section
label "one_critical" = p1=2|p2=2|p3=2;

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		10,744		30,009	7
4		201,828		70,447	7
5		6,769,448		148,010	8
6		1.31x108		224,991	8
8		4.51x1010		420,779	8
10		4.65x1013		1,062,323	9

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.89		1.04	15
4		1.25		3.41	17
5		1.78		18.6	19
6		2.94		28.3	21
8		5.96		104	25
10		17.28		261	29

Model Checking

When model checking, we have the following requirements:

• Scheduler-Liveness: for each time t and any process P_i not in its remainder phase at time t, there exists a time t' > t in which P_i makes a move.
• Fault freeness: if a process P_i moves into its critical section phase then eventually P_i moves from this phase to its exit phase and from its exit phase to its remainder phase.

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

Below the PCTL properties that we have verified are satisfied in all states of the model.

// Mutual exclusion: at any time t there is at most one process in its critical section phase
num_procs_in_crit <= 1

// Liveness: if a process is trying, then eventually a process enters the critical section
"one_trying" => P>=1 [ F "one_critical" ]

One requirement that we have been unable to verify is:

• k-Bounded-Waiting: if M processes participate in a trying round, then each process has probability at least 1/kM of entering the critical section at the end of the trying round."

The problem is that this requirement cannot be expressed by a PCTL formula as property corresponds to the probability of a conjunction of path formulae (expressing the properties a process participates in a round, M processes participate in a round and a process enters the critical section) being greater than a certain bound. However, in PCTL we are restricted to comparing only the probability of single path formulae with bounds.

On the other hand, this property could be expressed in PCTL*, but we would still need to consider a different formula for each possible value of M (M ranges from 1 up to the number of processes).

We note that Saias [Sai92] proved that this property does not hold. Furthermore, Kushilevitz and Rabin [KR92] have presented a modified version of this algorithm which solves this problem.