Cadence SMVによるアルゴリズムの検査

先日、Cadence SMVによるモデル検査を扱う機会があった。アルゴリズムの検証で有用だと感じたので 復習がてら簡単に使ってみたい。

検査

今回は、並行コンピューティング技法で紹介されているスピンロックのバグの実装例をモデル検査で検証する。
その検査対象の擬似コードは以下の通り。2つのスレッドがスピンロックでそれぞれのCriticalRegionの保護しながら動作する。当然ながらこのロックには欠陥がある。

int thread0inside = 0;
int thread1inside = 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...
	}
}

検査手段と目標

検査手段としては、冒頭のCadence SMVを用いる。
今回はあくまで例示であるため、CriticalRegionOfThreadZero、CriticalRegionOfThreadOneが同時実行されないことをモデル検査で検証する

SMVの記述

SMVは状態遷移を記述する。各コードを抽象化して、スレッド内のプログラムカウンタ（もっと簡便に説明するなら行番号）の値を状態とし、プログラムカウンタが進んだりループしたりするのを状態遷移と見なす。
SMVのコードは次のようになる。

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;
	next(th1pc) :=
		case
			th1pc = 1 & thread0inside = FALSE : {1, 2};
			th1pc > 1 & th1pc < 5 : th1pc + 1;
			th1pc = 5 : {5, 1};
			TRUE : th1pc;
		esac;
SPEC
	AG(!(th1pc = 3 & th0pc = 3))

th1pc、th0pcが各スレッドのプログラムカウンタで、1にスピンロックのスピン、2にロックのフラグ更新、3にCriticalRegionの処理、4にロックを解除するフラグ更新、5にCriticalRegionと無関係な処理があるとする。
th1pc、th0pcが同時に3になるとバグとなる。

実行結果

上記のSMVのコードをCadense SMVのモデル検査器で検査すると、以下の様な出力結果が得られる。

(中略)
Model checking results
======================
(AG $$$_mc_0)..............................................................false
(中略)

これはスピンロックで保護しているはずのCriticalRegionOfThreadZero、CriticalRegionOfThreadOneが同時実行される欠陥があることを示している。
なおcadense SMV実行時に生成される「*.out」ファイルに、どのような遷移で同時実行状態になるかのパス情報が記述されている。