Model Name | phil |
Description | Classical example of multi-process synchronization problem by E. Dijkstra. |
Source Code | phil.pml |
出典 | K. M. Chandy and J. Misra The Drinking Philosophers Problem. ACM Trans, pages 632-646, 1984. |
shared variable fork: array[1..N] of boolean initially false; process p /* 0 <= p < N */ while true do request_and_get(fork[p]); request_and_get(fork[(p+1)%N]); fork[p] = false; fork[(p+1)%N] = false; od
N | プロセス数(哲学者の人数) |
SOL | デッドロックの解決方法
|
名前 | Source Code | 性質(LTL記述) | 説明 |
liveness1 | phil.live1 | ! ([] <> eat) | 哲学者はいつか食事を行うことができる. |
liveness2 | phil.live2 | ! ([] (one -> <> eat)) | フォークを1本手にしたら、いつか食事を行うことができる. |
liveness3 | phil.live3 | ! ([] <> someoneeats) | いつか、誰かは食事を行うことができる. |
$ spin -a -DN=7 phil.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=6 -DSOL=2 -N phil.live2 phil.pml $ gcc -o pan pan.c $ ./pan -a -f
最終更新日:2008/08/25