Promela Source Code (Ver.0.1.0)

Mutual Execlusion

Queue-lock Mutual Execlusion
mutex_QL queue-lock mutex algorithm
mutex_TA T. Anderson's mutex algorithm
mutex_GT Graunke and Thakkar's mutex algorithm
mutex_MCS Mellor-Crummey and Scott's mutex algorithm
Fast Mutual Execlusion
mutex_L Lamport's fast mutual exclusion algorithm
Timing-based Algorithm
mutex_F Fischer's mutex algorithm
mutex_AT Alur and Taubenfeld's mutex algorithm
Mutual Exclusion with Nonatomic Operations
mutex_L_N1 Lamport's basic nonatomic algorithm
mutex_L_N2 Lamport's livelock-free nonatomic algorithm
mutex_L_N3 Lamport's starvation-free nonatomic algorithm
mutex_JA J. Anderson's nonatomic algorithm
Classical Problem and Algorithm
bakery Lamport's bakery algorithm
peterson Peterson's mutual exclusion algorithm.
phil dining philosophers problem

参考文献

  1. Spin - Formal Verification, 公式サイト
  2. BEEM - BEnchmarks for Explicit Model checkers, 公式サイト

戻る

最終更新日：2008/08/25