Model Name | mutex_AT |
Description | A fast timing-based mutual exclusion algorithm by Alur and Taubenfeld. |
Source Code | mutex_AT.pml |
出典 | James H. Anderson and Yong-jik Kim. Shared-memory mutual exclusion: Major research trends since (1986). Distributed Computing, pages 75-110, 2003. |
shared variables X: 1..N; Y : 0..N initially 0; Z: boolean initially false process p /* 1 <= p <= N */ while true do 1: Noncritical Section; Start: 2: X := p; 3: await Y = 0 ; 4: Y := p; 5: if X != p then 6: delay(2・Δ); 7: if Y != p then go to Start fi; 8: await ¬Z else 9: Z := true fi; 10: Critical Section; 11: Z := false; 12: if Y = p then 13: Y := 0 fi od
N | プロセス数 |
ERROR | エラーの有無 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | mutex_AT.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | mutex_AT.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | mutex_AT.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | mutex_AT.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=5 -N mutex_AT.safe1 mutex_AT.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=7 -DERROR -N mutex_AT.live1 mutex_AT.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/24