Model Name | mutex_MCS |
Description | linked-list-based queue-lock mutual exclusion algorithm by Mellor-Crummey and Scott. |
Source Code | mutex_MCS.pml |
出典 | James H. Anderson and Yong-jik Kim. Shared-memory mutual exclusion: Major research trends since (1986). Distributed Computing, pages 75-110, 2003. |
type Qnode = record next: pointer to Qnode; locked: boolean end /* stored in one word */ shared variable Nodes: array[0..N - 1] of Qnode; /* Nodes[p] is stored locally to process p */ Tail : pointer to Qnode initially NIL process p /* 0 <= p < N */ private constant my_node = &Nodes[p] private variable pred: pointer to Qnode while true do 1: Noncritical Section; 2: my_node->next := NIL; 3: pred := fetch_and_store(Tail , my_node); 4: if pred != NIL then 5: my_node->locked := true; 6: pred->next := my_node; 7: await ¬my_node->locked /* spin until granted the lock by predecessor */ fi; 8: Critical Section; 9: if my_node->next = NIL then 10: if compare_and_swap(Tail , my_node, NIL) = false then 11: await my_node->next != NIL; /* spin until next field is updated */ 12: my_node->next->locked := false fi else 13: my_node->next->locked := false fi od
N | プロセス数 |
名前 | Source Code | 性質(LTL記述) | 説明 |
safety1 | mutex_MCS.safe1 | collision | クリティカルセクションに複数のプロセスが侵入してしまう. |
liveness1 | mutex_MCS.live1 | ! ([] (wait -> <> (cs))) | プロセスがwait状態にあるならば、いつかクリティカルセクションに入る. |
liveness2 | mutex_MCS.live2 | ! ([] ( (! cs) -> <> cs)) | クリティカルセクションにいないプロセスは、いつかクリティカルセクションに入ることができる. |
liveness3 | mutex_MCS.live3 | ! ([] <> someoneincs) | いつか、あるプロセスがクリティカルセクションに入る. |
$ spin -a -DN=5 -N mutex_MCS.safe1 mutex_MCS.pml $ gcc -o pan pan.c $ ./pan
$ spin -a -DN=6 -N mutex_MCS.live2 mutex_MCS.pml $ gcc -o pan pan.c $ ./pan -a
最終更新日:2008/08/24