Promela Source Code

Model: mutex_TA

Information

Model Name	mutex_TA
Description	queue-lock mutual exclusion algorithm by T. Anderson.
Source Code	mutex_TA.pml
出典	James H. Anderson and Yong-jik Kim. Shared-memory mutual exclusion: Major research trends since (1986). Distributed Computing, pages 75-110, 2003.

Algorithm

const
	has_lock = 0 ;
	must_wait = 1

shared variable
	Slots: array[0..N - 1] of {has_lock, must_wait};
	Next_slot: integer initially 0

initially
	Slots[0] = has_lock ∧ (∀k : 0 < k < N :: Slots[k] = must_wait)

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

private variable
	my_place: integer

while true do
1:	Noncritical Section;
2:	my_place := fetch_and_inc(Next_slot);
3:	if my_place = N - 1 then
4:		atomic add(Next_slot, -N)
	fi;
5:	my_place := my_place mod N;
6:	await Slot[my_place] = has_lock; /* spin */
7:	Slots[my_place] := must_wait;
8:	Critical Section;
9:	Slot[my_place + 1 mod N] := has_lock
od

Parameters

プロセス数

性質記述

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

使用例

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

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

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

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

戻る

最終更新日：2008/08/24