Promela Source Code

Model: mutex_L_N3

Information

Model Name	mutex_L_N3
Description	Mutual exclusion with nonatomic operations by Lamport. This algorithm is starvation-free.
Source Code	mutex_L_N3.pml
出典	James H. Anderson and Yong-jik Kim. Shared-memory mutual exclusion: Major research trends since (1986). Distributed Computing, pages 75-110, 2003.

Algorithm

shared variable
	P: array[0..N - 1] of boolean initially false;
	E: array[0..N - 1] of boolean initially false;
	T: array[0..N - 1] of boolean

process p /* 0 <= p < N */

private variable
	i, k: 0..N - 1;
	temp: boolean

while true do
1:	Noncritical Section;
2:	P[p] := true;
3:	E[p] := true;
4:	k := low(T,E);
5:	if k != p then
6:		for i := k cyclically to (p - 1) mod N do
7:			if E[i] then
8:				P[p] := false;
9:				go to 3
			fi
		od
	fi;
10:	if ￢P[p] then go to 2 fi;
11:	for i := p + 1 cyclically to (k - 1) mod N do
12:		if P[i] then go to 2 fi
	od;
13:	Critical Section;
14:	temp := ￢T[p];
15:	T[p] := temp;
16:	P[p] := false;
17:	E[p] := false
od

Parameters

プロセス数

性質記述

名前	Source Code	性質(LTL記述)	説明
safety1	mutex_L_N3.safe1	collision	クリティカルセクションに複数のプロセスが侵入してしまう．
liveness1	mutex_L_N3.live1	! ([] (wait -> <> (cs)))	プロセスがwait状態にあるならば、いつかクリティカルセクションに入る．
liveness2	mutex_L_N3.live2	! ([] ( (! cs) -> <> cs))	クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる．
liveness3	mutex_L_N3.live3	! ([] <> someoneincs)	いつか、あるプロセスがクリティカルセクションに入る．

使用例

プロセス数: 5, 性質: safety1

	$ spin -a -DN=5 -N mutex_L_N3.safe1 mutex_L_N3.pml
	$ gcc -o pan pan.c
	$ ./pan

プロセス数: 6, 性質: liveness2

	$ spin -a -DN=6 -N mutex_L_N3.live2 mutex_L_N3.pml
	$ gcc -o pan pan.c
	$ ./pan -a

戻る

最終更新日：2008/08/24