Promela Source Code

Model: mutex_MCS

Information

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

Algorithm

type
	Qnode = record next: pointer to Qnode; locked: boolean end /* stored in one word */

shared variable
	Nodes: array[0..N - 1] of Qnode; /* Nodes[p] is stored locally to process p */
	Tail : pointer to Qnode initially NIL

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

private constant
	my_node = &Nodes[p]

private variable
	pred: pointer to Qnode

while true do
1:	Noncritical Section;
2:	my_node->next := NIL;
3:	pred := fetch_and_store(Tail , my_node);
4:	if pred != NIL then
5:		my_node->locked := true;
6:		pred->next := my_node;
7:		await ￢my_node->locked /* spin until granted the lock by predecessor */
	fi;
8:	Critical Section;
9:	if my_node->next = NIL then
10:		if compare_and_swap(Tail , my_node, NIL) = false then
11:			await my_node->next != NIL; /* spin until next field is updated */
12:			my_node->next->locked := false
		fi
	else
13:		my_node->next->locked := false
	fi
od

Parameters

プロセス数

性質記述

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

使用例

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

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

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

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

戻る

最終更新日：2008/08/24