Promela Source Code

Model: mutex_JA

Information

Model Name	mutex_JA
Description	Mutual exclusion with nonatomic operations by J. Anderson.
Source Code	mutex_JA.pml
出典	James H. Anderson and Yong-jik Kim. Shared-memory mutual exclusion: Major research trends since (1986). Distributed Computing, pages 75-110, 2003.

Algorithm

/* Two-process case */
shared variable P, Q, T: array[u, v] of boolean initially true

process u

private variable x: boolean
initially x = T[u]

while true do
1:	Noncritical Section;
2:	P[u] := false;
3:	Q[u] := false;
4:	x := T[v];
5:	T[u] := x;
6:	if x then
7:		P[u] := true;
8:		await P[v]
	else
9:		Q[u] := true;
10:		await Q[v]
	fi;
11:	Critical Section;
12:	P[u] := true;
13:	Q[u] := true
od

process v

private variable x: boolean
initially x = T[v]

while true do
1:	Noncritical Section;
2:	P[v] := false;
3:	Q[v] := false;
4:	x := ￢T[u];
5:	T[v] := x;
6:	if x then
7:		Q[v] := true;
8:		await P[u]
	else
9:		P[v] := true;
10		await Q[u]
	fi;
11:	Critical Section;
12:	P[v] := true;
13:	Q[v] := true
od


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

while true do
	Noncritical Section;
	for i := 0 to N - 1 do
		if i != p then ENTRY(p, i)
	od;
	Critical Section;
	for i := 0 to N - 1 do
		if i != p then EXIT(p, i)
	od
od

Parameters

プロセス数

性質記述

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

使用例

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

	$ spin -a -DN=3 -N mutex_JA.safe1 mutex_JA.pml
	$ gcc -o pan pan.c
	$ ./pan

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

	$ spin -a -DN=4 -N mutex_JA.live2 mutex_JA.pml
	$ gcc -o pan pan.c
	$ ./pan -a

戻る

最終更新日：2008/08/24