Model Name | mutex_GT |
Description | array-based queue-lock mutual exclusion algorithm by Graunke and Thakkar. |
Source Code | mutex_GT.pml |
出典 | James H. Anderson and Yong-jik Kim. Shared-memory mutual exclusion: Major research trends since (1986). Distributed Computing, pages 75-110, 2003. |
type Tailtype = record last: pointer to boolean; bit : boolean end /* stored in one word */ shared variable Slots: array[0..N - 1] of boolean initially true; Tail : Tailtype initially (&Slots[0], false) process p /* 0 <= p < N */ private variable prev: pointer to boolean; bit , temp: boolean while true do 1: Noncritical Section; 2: (prev, bit) := fetch_and_store(Tail , (&Slots[p], Slots[p])); 3: await *prev != bit ; /* spin until toggle */ 4: Critical Section; 5: temp := ¬Slots[p]; 6: Slots[p] := temp od
N | プロセス数 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | mutex_GT.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | mutex_GT.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | mutex_GT.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | mutex_GT.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=5 -N mutex_GT.safe1 mutex_GT.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=6 -N mutex_GT.live2 mutex_GT.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/24