Promela Source Code

Model: bakery

Information

Model Name	bakery
Description	Lamport's bakery algorithm is a classical algorithm of mutual exclusion.
Source Code	bakery.pml
出典	Leslie Lamport. A New Solution of Dijkstra's Concurrent Programming Problem. Communications of the ACM 17,8 , pages 453-455, August 1974.

Algorithm

shared variable
	choosing: array[1..N] of boolean initially 0;
	number: array[1..N] of integer initially 0;

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

private variable
	i, j: 1..N

while true do
	Noncritical Section;
	choosing [i] : = 1;
	number[i] := 1 + maximum(number[1] ,..., number[N]);
	choosing[i] := 0;
	for j = 1 to N do
L1:		if choosing[j] != 0 then goto L1;
L2:		if number[j] != 0 and (number[j], j) < (number[i], i) then goto L2;
	od;
	Critical Section;
	number[i] := O
od;

Parameters

プロセス数

性質記述

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

使用例

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

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

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

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

戻る

最終更新日：2008/08/25