Promela Source Code

Model: phil

Information

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.

Algorithm

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

Parameters

N	プロセス数(哲学者の人数)
SOL	デッドロックの解決方法 SOL=0: 未解決 SOL=1: 他人と逆の手からフォークを取り始める． SOL=2: 2本目のフォークがとれない場合，1本目のフォークを戻すような哲学者を1人入れる．

性質記述

名前	Source Code	性質(LTL記述)	説明
liveness1	phil.live1	! ([] <> eat)	哲学者はいつか食事を行うことができる．
liveness2	phil.live2	! ([] (one -> <> eat))	フォークを1本手にしたら、いつか食事を行うことができる．
liveness3	phil.live3	! ([] <> someoneeats)	いつか、誰かは食事を行うことができる．

使用例

哲学者: 7人, 性質: デッドロック

	$ spin -a -DN=7 phil.pml
	$ gcc -o pan pan.c
	$ ./pan

哲学者: 6人, 解決方法: 2, 性質: liveness2

	$ spin -a -DN=6 -DSOL=2 -N phil.live2 phil.pml
	$ gcc -o pan pan.c
	$ ./pan -a -f

戻る

最終更新日：2008/08/25