Alloy による排他制御のモデリング

alloy_exclusion.als

// ************************************
//   排他制御のモデル
// ************************************

// Time シグネチャに全順序構造を導入
open util/ordering [Time]

// 時刻を表すシグネチャ
sig Time {}

// リソースを表すシグネチャ
sig Resource {}

// プロセスを表すシグネチャ
sig Process {
    connect : some Resource,   // タスク実行に必要となるリソース全体
    lock    : connect -> Time  // ある時刻にロックしているリソース全体
}

// リソースの確保 : 時刻 t から t' の間にプロセス p がリソース r を確保
pred acquire (t, t' : Time, p : Process, r : Resource) {
    // r は事前状態 t においてどのプロセスからもロックされていない
    r not in Process.lock.t
    // p がロックしているリソースに r が追加される
    p.lock.t' = p.lock.t + r
    // p 以外のプロセスのロックに関しては変化なし
    all p0 : Process - p | p0.lock.t' = p0.lock.t
}

// リソースの解放 : 時刻 t から t' の間にプロセス p がリソースを解放
pred release (t, t' : Time, p : Process) {
    // p は事前状態 t において必要なリソースをすべて確保していた
    p.lock.t  = p.connect
    // p は事後状態 t' においてロックを掛けていない
    p.lock.t' = none
    // p 以外のプロセスのロックに関しては変化なし
    all p0 : Process - p | p0.lock.t' = p0.lock.t
}

// 何も起こらない : 時刻 t から t' の間にシステムの状態が変化しない
pred skip (t, t' : Time) {
    // すべてのプロセスのロックに関して変化なし
    all p : Process | p.lock.t' = p.lock.t
}

// システムの初期状態
pred init (t : Time) {
    // どのプロセスもロックを掛けていない
    all p : Process | p.lock.t = none
}

// タスクは即座に完了する
fact immediateAction {
    // ある時刻に必要リソースをすべてロックできた場合、直後に解放が発生
    all t : Time - last | let t' = t.next |
        all p : Process | p.lock.t = p.connect => release [t, t', p]
}

// システムの状態は可能ならば必ず進行し、無意味に待たない
fact bestEffortProgress {
    // 新たにリソースを確保しにいけるプロセスが一つでも存在すれば、無意味に待たない
    all t : Time - last | let t' = t.next |
        (some p : Process | p.connect - Process.lock.t != none)
            => not skip [t, t']
}

// 状態遷移に関する制約
fact traces {
    // 初期時刻において初期状態が成立
    init [first]
    // リソース確保か、解放か、何もしないかのいずれかで時間が経過する
    all t : Time - last | let t' = t.next |
        some p : Process, r : Resource |
            acquire [t, t', p, r] or release [t, t', p] or skip [t, t']
}

// 検査したい性質 : システムの状態は必ず進行しつづける
assert progress {
    all t : Time - last | let t' = t.next | not skip [t, t']
}
// 上の性質が成り立つかどうかを検査 (反例が検出される)
check progress for 2 Resource, 2 Process, 4 Time