Promela Source Code

Model: peterson

Information

Model Name	peterson
Description	A classical algorithm of mutual exclusion problem. Devised by Peterson.
Source Code	peterson.pml
出典	K. Alagarsamy and K. Vidyasankar. Fair and Efficient Mutual Exclusion Algorithms (Extended Abstract). Lecture Notes In Computer Science; Vol. 1693, pages 166-179, 1999.

Algorithm

shared variable
	pos: array[1..N] of integer
	step: array[1..N] of integer

process i /* 1 <= i <= N */

private variable
	j, k: 1..N

while true do
1:	Noncritical Section;
2:	for j = 1 to N - 1 do
3:		pos[i] := j;
4:		step[j] := i;
5:		await (∀k != i, pos[k] < j) ∨ (step[j] != i)
6:	od;
7:	Critical Section;
8:	pos[i] := 0;
od

Parameters

プロセス数

性質記述

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

使用例

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

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

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

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

戻る

最終更新日：2008/08/25