Promela Source Code

Model: mutex_QL

Information

Model Name	mutex_QL
Description	simple queue-lock mutual exclusion algorithm.
Source Code	mutex_QL.pml
出典	T. E. Anderson. The Performance of Spin Lock Alternatives for Shared-Money Multiprocessors IEEE Trans. Parallel Distrib. Syst. pages 6-16, 1990.

Algorithm

	Init:
	  flags[0] = HAS_LOCK;
	  flags[1] = .. = flags[P-1] = MUST_WAIT;
	  queueLast = 0;
	Lock:
	  myPlace = ReadAndIncrement(queueLast);
	  while(flags[myPlace % P] == MUST_WAIT) ;
	  flags[myPlace % P] = MUST_WAIT;
	Unlock:
	  flags[(myPlace+1) % P] = HAS_LOCK;

Parameters

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

性質記述

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

使用例

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

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

プロセス数: 4，エラー: あり，性質: liveness3

	$ spin -a -DN=4 -DERROR -N mutex_QL.live3 mutex_QL.pml
	$ gcc -o pan pan.c
	$ ./pan -a

戻る

最終更新日：2008/08/24