Promela Source Code

Model: mutex_L

Information

Model Name	mutex_L
Description	This is 'fast mutual exclusion algorithm' that uses only reads and writes. It's devised by Lamport.
Source Code	mutex_L.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
	B: array[1..N] of boolean initially false;
	X: 1..N;
	Y : 0..N initially 0

process p /* 1 <= p <= N */

private variable
	j: 1..N

while true do
1:	Noncritical Section;
2:	B[p] := true;
3:	X := p;
4:	if Y != 0 then
5:		B[p] := false;
6:		await Y = 0 ; /* busy wait */
7:		goto 1
	fi;
8:	Y := p;
9:	if X != p then
10:		B[p] := false;
11:		for j := 1 to N do
12:			await ￢B[j] /* busy wait */
		od;
13:		if Y != p then
14:			await Y = 0 ; /* busy wait */
15:			goto 1
		fi
	fi;
16:	Critical Section;
17:	Y := 0;
18:	B[p] := false
od

Parameters

プロセス数

性質記述

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

使用例

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

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

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

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

戻る

最終更新日：2008/08/24