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. |
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;
N | プロセス数 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | bakery.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | bakery.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | bakery.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | bakery.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=5 -N bakery.safe1 bakery.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=6 -N bakery.live2 bakery.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/25