Model Name | mutex_QL |
Description | simple queue-lock mutual exclusion algorithm. |
Source Code | mutex_QL.pml |
出典 | T. E. Anderson. The Performance of Spin Lock Alternatives for Shared-Money Multiprocessors IEEE Trans. Parallel Distrib. Syst. pages 6-16, 1990. |
Init: flags[0] = HAS_LOCK; flags[1] = .. = flags[P-1] = MUST_WAIT; queueLast = 0; Lock: myPlace = ReadAndIncrement(queueLast); while(flags[myPlace % P] == MUST_WAIT) ; flags[myPlace % P] = MUST_WAIT; Unlock: flags[(myPlace+1) % P] = HAS_LOCK;
N | プロセス数 |
ERROR | エラーの有無 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | mutex_QL.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | mutex_QL.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | mutex_QL.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | mutex_QL.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=5 -N mutex_QL.safe1 mutex_QL.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=4 -DERROR -N mutex_QL.live3 mutex_QL.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/24