Promela Source Code

Model: mutex_F

Information

Model Name	mutex_F
Description	A simple timing-based mutual exclusion algorithm by Fischer.
Source Code	mutex_F.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 Y : 0..N initially 0

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

while true do
1:	Noncritical Section;
	repeat
2:		await Y = 0 ;
3:		Y := p;
4:		delay(Δ)
5:	until Y = p;
6:	Critical Section;
7:	Y := 0
od

Parameters

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

性質記述

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

使用例

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

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

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

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

戻る

最終更新日：2008/08/24