Promela Source Code

Model: mutex_AT

Information

Model Name	mutex_AT
Description	A fast timing-based mutual exclusion algorithm by Alur and Taubenfeld.
Source Code	mutex_AT.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 variables
	X: 1..N;
	Y : 0..N initially 0;
	Z: boolean initially false
process p /* 1 <= p <= N */
while true do
1:	Noncritical Section;
	Start:
2:	X := p;
3:	await Y = 0 ;
4:	Y := p;
5:	if X != p then
6:		delay(2・Δ);
7:		if Y != p then go to Start fi;
8:		await ￢Z
	else
9:		Z := true
	fi;
10:	Critical Section;
11:	Z := false;
12:	if Y = p then
13:		Y := 0
	fi
od

Parameters

N	プロセス数
ERROR	エラーの有無

性質記述

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

使用例

プロセス数: 5, エラー: なし, 性質: safety1

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

プロセス数: 7, エラー: あり, 性質: liveness1

	$ spin -a -DN=7 -DERROR -N mutex_AT.live1 mutex_AT.pml
	$ gcc -o pan pan.c
	$ ./pan -a

戻る

最終更新日：2008/08/24