Model Name | mutex_L |
Description | This is 'fast mutual exclusion algorithm' that uses only reads and writes. It's devised by Lamport. |
Source Code | mutex_L.pml |
出典 | James H. Anderson and Yong-jik Kim. Shared-memory mutual exclusion: Major research trends since (1986). Distributed Computing, pages 75-110, 2003. |
shared variable B: array[1..N] of boolean initially false; X: 1..N; Y : 0..N initially 0 process p /* 1 <= p <= N */ private variable j: 1..N while true do 1: Noncritical Section; 2: B[p] := true; 3: X := p; 4: if Y != 0 then 5: B[p] := false; 6: await Y = 0 ; /* busy wait */ 7: goto 1 fi; 8: Y := p; 9: if X != p then 10: B[p] := false; 11: for j := 1 to N do 12: await ¬B[j] /* busy wait */ od; 13: if Y != p then 14: await Y = 0 ; /* busy wait */ 15: goto 1 fi fi; 16: Critical Section; 17: Y := 0; 18: B[p] := false od
N | プロセス数 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | mutex_L.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | mutex_L.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | mutex_L.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | mutex_L.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=5 -N mutex_L.safe1 mutex_L.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=6 -N mutex_L.live2 mutex_L.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/24