0; void threadZero() { while (true) { while (thread1inside) {} ...OtherTask... thread0inside = 1; ...CriticalRegionOfThreadZero... thread0inside = 0; ...OtherTask... } } void threadOne() { while (true) { while (thread0inside) {} ...OtherTask... thread1inside = 1; ...CriticalRegionOfThreadOne... thread1inside = 0; ...OtherTask... } } MODULE main VAR thread0inside : boolean; thread1inside : boolean; th0pc : 1..5; th1pc : 1..5; ASSIGN init(thread0inside) := FALSE; init(thread1inside) := FALSE; init(th0pc) := 1; init(th1pc) := 1; next(thread0inside) := case th0pc = 2 : TRUE; th0pc = 4 : FALSE; TRUE : thread0inside; esac; next(thread1inside) := case th1pc = 2 : TRUE; th1pc = 4 : FALSE; TRUE : thread1inside; esac; next(th0pc) := case th0pc = 1 & thread1inside = FALSE : {1, 2}; th0pc > 1 & th0pc < 5 : th0pc + 1; th0pc = 5 : {5, 1}; TRUE : th0pc; esac; スピンロックのコード 状態遷移モデル化しSMVで記述 Cadence SMV でモデル検査 デッドロックの 有無を確認