Model Name | mutex_L_N3 |
Description | Mutual exclusion with nonatomic operations by Lamport. This algorithm is starvation-free. |
Source Code | mutex_L_N3.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 P: array[0..N - 1] of boolean initially false; E: array[0..N - 1] of boolean initially false; T: array[0..N - 1] of boolean process p /* 0 <= p < N */ private variable i, k: 0..N - 1; temp: boolean while true do 1: Noncritical Section; 2: P[p] := true; 3: E[p] := true; 4: k := low(T,E); 5: if k != p then 6: for i := k cyclically to (p - 1) mod N do 7: if E[i] then 8: P[p] := false; 9: go to 3 fi od fi; 10: if ¬P[p] then go to 2 fi; 11: for i := p + 1 cyclically to (k - 1) mod N do 12: if P[i] then go to 2 fi od; 13: Critical Section; 14: temp := ¬T[p]; 15: T[p] := temp; 16: P[p] := false; 17: E[p] := false od
N | プロセス数 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | mutex_L_N3.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | mutex_L_N3.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | mutex_L_N3.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | mutex_L_N3.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=5 -N mutex_L_N3.safe1 mutex_L_N3.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=6 -N mutex_L_N3.live2 mutex_L_N3.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/24