Model Name | mutex_JA |
Description | Mutual exclusion with nonatomic operations by J. Anderson. |
Source Code | mutex_JA.pml |
出典 | James H. Anderson and Yong-jik Kim. Shared-memory mutual exclusion: Major research trends since (1986). Distributed Computing, pages 75-110, 2003. |
/* Two-process case */ shared variable P, Q, T: array[u, v] of boolean initially true process u private variable x: boolean initially x = T[u] while true do 1: Noncritical Section; 2: P[u] := false; 3: Q[u] := false; 4: x := T[v]; 5: T[u] := x; 6: if x then 7: P[u] := true; 8: await P[v] else 9: Q[u] := true; 10: await Q[v] fi; 11: Critical Section; 12: P[u] := true; 13: Q[u] := true od process v private variable x: boolean initially x = T[v] while true do 1: Noncritical Section; 2: P[v] := false; 3: Q[v] := false; 4: x := ¬T[u]; 5: T[v] := x; 6: if x then 7: Q[v] := true; 8: await P[u] else 9: P[v] := true; 10 await Q[u] fi; 11: Critical Section; 12: P[v] := true; 13: Q[v] := true od /* N-process */ process p /* 0 <= p < N */ while true do Noncritical Section; for i := 0 to N - 1 do if i != p then ENTRY(p, i) od; Critical Section; for i := 0 to N - 1 do if i != p then EXIT(p, i) od od
N | プロセス数 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | mutex_JA.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | mutex_JA.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | mutex_JA.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | mutex_JA.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=3 -N mutex_JA.safe1 mutex_JA.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=4 -N mutex_JA.live2 mutex_JA.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/24