Model Name | mutex_F |
Description | A simple timing-based mutual exclusion algorithm by Fischer. |
Source Code | mutex_F.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 Y : 0..N initially 0 process p /* 1 <= p <= N */ while true do 1: Noncritical Section; repeat 2: await Y = 0 ; 3: Y := p; 4: delay(Δ) 5: until Y = p; 6: Critical Section; 7: Y := 0 od
N | プロセス数 |
ERROR | エラーの有無 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | mutex_F.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | mutex_F.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | mutex_F.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | mutex_F.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=5 -N mutex_F.safe1 mutex_F.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=7 -DERROR -N mutex_F.live1 mutex_F.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/24