NuSMVを試す [SMV]
モデル検査ツールのNuSMVを試してみた。
例題として基本的な排他制御を書いてみる。
MODULE lock
VAR
locked-by : {nobody, 0, 1};
ASSIGN
init(locked-by) := nobody;
MODULE proc(id, lock)
VAR
status: {normal, trying, critical};
ASSIGN
init(status) := normal;
next(status) :=
case
(status = normal) : {trying, normal};
(status = trying) & (lock.locked-by = nobody) : critical;
(status = critical) : {critical, normal};
TRUE : status;
esac;
next(lock.locked-by) :=
case
(next(status) = critical) : id;
(status = critical & next(status) = normal) : nobody;
TRUE : lock.locked-by;
esac;
MODULE main
VAR
lock: process lock;
proc0: process proc(0, lock);
proc1: process proc(1, lock);
-- safety: at most one process can enter ciritcal section.
LTLSPEC G !((proc0.status = critical) & (proc1.status = critical))
lockモジュールはlocked-byという変数だけを持つ。 これはロックを所有しているプロセスID(誰もロックをとっていない場合はnobody)を示す。
procモジュールはプロセスの現在の状態をstatusという変数で持つ。 normalは何もしていない状態、tryingはロックを取得しようとしている状態、criticalはロックを取得した状態である。
statusの初期状態はnormalで、状態遷移はnext(status) := ...
で定義される。
normalの場合は、そのままnormalにとどまるか、非決定的にtryingに遷移する。
tryingで、かつロックが誰にも取得されていなければcriticalに遷移する。
criticalの場合は、そのままcriticalにとどまるか、非決定的にnormalに遷移する。
procモジュールの中でロックの状態の更新も行っている。 statusがcriticalの場合は自身のプロセスIDで置き換える。 criticalからnormalに遷移した場合は所有者をnobodyに戻す。
mainはlockと2つのprocを結びつける。procの引数にはプロセスIDとロックを与える。
LTLSPECはこのモデルが満たすべき仕様(最大1つのプロセスしかクリティカルセクションに入れない)を時相論理式で定義している。
$ NuSMV mutex.smv
*** This is NuSMV 2.5.4 (compiled on Sun Aug 24 14:27:46 UTC 2014)
(中略)
WARNING *** Processes are still supported, but deprecated. ***
WARNING *** In the future processes may be no longer supported. ***
WARNING *** The model contains PROCESSes or ISAs. ***
WARNING *** The HRC hierarchy will not be usable. ***
-- specification G !(proc0.status = critical & proc1.status = critical) is true
最後の行で仕様が満たされたことがわかる。
このようなモデルの書き方がもう廃止候補になっていることが警告されるのだけど、 その背景や代替の書き方などについて知識がないのでとりあえずこのままいくことにする。
次に新たな仕様として、飢餓状態が起こらないことを表現したい。 これはそれぞれのプロセスについて 「どんな場合でも一度tryingになったらいつかはcriticalに入れる」 と宣言することで表現できる。 そこでMODULE procの最後に次の仕様を記述する。
LTLSPEC G ((status = trying) -> F (status = critical))
これで実行してみると仕様が満たされないことが報告され、その反例が示される。
$ NuSMV mutex.smv
*** This is NuSMV 2.5.4 (compiled on Sun Aug 24 14:27:46 UTC 2014)
(中略)
-- specification G (status = trying -> F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
lock.locked-by = nobody
proc0.status = normal
proc1.status = normal
-> Input: 1.2 <-
_process_selector_ = proc0
running = FALSE
proc1.running = FALSE
proc0.running = TRUE
lock.running = FALSE
-> State: 1.2 <-
proc0.status = trying
-> Input: 1.3 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-> State: 1.3 <-
proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
lock.locked-by = 1
proc1.status = critical
-> Input: 1.5 <-
_process_selector_ = main
running = TRUE
proc1.running = FALSE
-> State: 1.5 <-
-- specification G (status = trying -> F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
lock.locked-by = nobody
proc0.status = normal
proc1.status = normal
-> Input: 2.2 <-
_process_selector_ = proc1
running = FALSE
proc1.running = TRUE
proc0.running = FALSE
lock.running = FALSE
-> State: 2.2 <-
proc1.status = trying
-> Input: 2.3 <-
_process_selector_ = main
running = TRUE
proc1.running = FALSE
-> State: 2.3 <-
-> Input: 2.4 <-
_process_selector_ = proc0
running = FALSE
proc0.running = TRUE
-- Loop starts here
-> State: 2.4 <-
proc0.status = trying
-> Input: 2.5 <-
_process_selector_ = main
running = TRUE
proc0.running = FALSE
-- Loop starts here
-> State: 2.5 <-
-> Input: 2.6 <-
_process_selector_ = lock
running = FALSE
lock.running = TRUE
-> State: 2.6 <-
-- specification G !(proc0.status = critical & proc1.status = critical) is true
この反例はちょっとつまらない、NuSMVの使い方に関するともいえるものだ。 この反例ではState: 1.2やState: 2.2で各プロセスがtryingになったあと、一度もそのプロセスに実行権が回ってきていないのである。
ここではOSのスケジューラがプロセスに対してある程度公平な扱いをすることを前提にしたい。 このためには、MODULE procに次の行を追加する。
FAIRNESS running
runningはプロセスが実行されていることを示す暗黙の変数で、先ほどの反例のトレース中にも現れていた。 FAIRNESSというのはその式が「いつも『いつかは成立する』」(その式が永遠に成立しないような経路を排除する)ということを条件として与えるものだ。
これで実行してもまだ反例が見つかる。
$ NuSMV mutex.smv
(中略)
-- specification G (status = trying -> F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
lock.locked-by = nobody
proc0.status = normal
proc1.status = normal
-> Input: 1.2 <-
_process_selector_ = proc0
running = FALSE
proc1.running = FALSE
proc0.running = TRUE
lock.running = FALSE
-> State: 1.2 <-
proc0.status = trying
-> Input: 1.3 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-> State: 1.3 <-
proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
lock.locked-by = 1
proc1.status = critical
-> Input: 1.5 <-
_process_selector_ = main
running = TRUE
proc1.running = FALSE
-- Loop starts here
-> State: 1.5 <-
-> Input: 1.6 <-
_process_selector_ = proc0
running = FALSE
proc0.running = TRUE
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-- Loop starts here
-> State: 1.7 <-
-> Input: 1.8 <-
_process_selector_ = main
running = TRUE
proc1.running = FALSE
-> State: 1.8 <-
-- specification G (status = trying -> F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
lock.locked-by = nobody
proc0.status = normal
proc1.status = normal
-> Input: 2.2 <-
_process_selector_ = proc0
running = FALSE
proc1.running = FALSE
proc0.running = TRUE
lock.running = FALSE
-> State: 2.2 <-
proc0.status = trying
-> Input: 2.3 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-> State: 2.3 <-
proc1.status = trying
-> Input: 2.4 <-
_process_selector_ = main
running = TRUE
proc1.running = FALSE
-> State: 2.4 <-
-> Input: 2.5 <-
_process_selector_ = proc0
running = FALSE
proc0.running = TRUE
-- Loop starts here
-> State: 2.5 <-
lock.locked-by = 0
proc0.status = critical
-> Input: 2.6 <-
-- Loop starts here
-> State: 2.6 <-
-> Input: 2.7 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-- Loop starts here
-> State: 2.7 <-
-> Input: 2.8 <-
_process_selector_ = main
running = TRUE
proc1.running = FALSE
-> State: 2.8 <-
-- specification G !(proc0.status = critical & proc1.status = critical) is true
これは何かというと、自分がtryingのときにもう一方のプロセスがロックを取得し、そのままずっと離さないことを示している。 我々のモデルには「ロックはいつか解放される」とは表現されていなかったのでこのようなことが起こる。
解決方法はおそらく2通りあり、FAIRNESSを使ってロックが永遠に離されない経路を排除するか、 ロックが有限ステップ内で解放されるようにASSIGNの定義を変えることだ。 ここでは後者の方法を選択することにし、プロセスはロックを取得したら次のステップで解放するようにする。
(status = critical) : normal;
また実行するとまた反例が見つかる。
$ NuSMV mutex.smv
(中略)
-- specification G (status = trying -> F status = critical) IN proc0 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
lock.locked-by = nobody
proc0.status = normal
proc1.status = normal
-> Input: 1.2 <-
_process_selector_ = proc0
running = FALSE
proc1.running = FALSE
proc0.running = TRUE
lock.running = FALSE
-> State: 1.2 <-
proc0.status = trying
-> Input: 1.3 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-> State: 1.3 <-
proc1.status = trying
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
lock.locked-by = 1
proc1.status = critical
-> Input: 1.5 <-
_process_selector_ = main
running = TRUE
proc1.running = FALSE
-- Loop starts here
-> State: 1.5 <-
-> Input: 1.6 <-
_process_selector_ = proc0
running = FALSE
proc0.running = TRUE
-- Loop starts here
-> State: 1.6 <-
-> Input: 1.7 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-> State: 1.7 <-
lock.locked-by = nobody
proc1.status = normal
-> Input: 1.8 <-
-> State: 1.8 <-
proc1.status = trying
-> Input: 1.9 <-
-> State: 1.9 <-
lock.locked-by = 1
proc1.status = critical
-- specification G (status = trying -> F status = critical) IN proc1 is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
lock.locked-by = nobody
proc0.status = normal
proc1.status = normal
-> Input: 2.2 <-
_process_selector_ = proc0
running = FALSE
proc1.running = FALSE
proc0.running = TRUE
lock.running = FALSE
-> State: 2.2 <-
proc0.status = trying
-> Input: 2.3 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-> State: 2.3 <-
proc1.status = trying
-> Input: 2.4 <-
_process_selector_ = main
running = TRUE
proc1.running = FALSE
-> State: 2.4 <-
-> Input: 2.5 <-
_process_selector_ = proc0
running = FALSE
proc0.running = TRUE
-- Loop starts here
-> State: 2.5 <-
lock.locked-by = 0
proc0.status = critical
-> Input: 2.6 <-
-> State: 2.6 <-
lock.locked-by = nobody
proc0.status = normal
-> Input: 2.7 <-
-> State: 2.7 <-
proc0.status = trying
-> Input: 2.8 <-
-- Loop starts here
-> State: 2.8 <-
lock.locked-by = 0
proc0.status = critical
-> Input: 2.9 <-
_process_selector_ = proc1
proc1.running = TRUE
proc0.running = FALSE
-- Loop starts here
-> State: 2.9 <-
-> Input: 2.10 <-
-> State: 2.10 <-
-- specification G !(proc0.status = critical & proc1.status = critical) is true
これは何かというと、自分がtryingの間もう一方のプロセスがロック取得・解放を延々と繰り返していてずっと割り込めないでいるのだ。
だからOSのスケジューラの公平さとは別に、ロックの動作自体に公平さをもたらす必要があることがわかる。 これはちょっと大仕事になる。
とりあえずtryingからcriticalに遷移していいかどうかの判断をprocから切り離してlockプロセスに移動する。 waitingという配列を導入して、procがtryingになるときにTRUEにする。 procはtrying中にlocked-byが自分自身になったときにcriticalに遷移できるが、locked-byを選ぶのはlockプロセスの仕事にする。 つまり、procはロックに応募するだけで、当選者を決めるのはlockの仕事である。
MODULE lock
VAR
locked-by : {nobody, 0, 1};
waiting : array 0..1 of boolean;
ASSIGN
init(locked-by) := nobody;
next(locked-by) :=
case
(locked-by = nobody & waiting[0] = TRUE) : 0;
(locked-by = nobody & waiting[1] = TRUE) : 1;
TRUE : locked-by;
esac;
next(waiting[0]) :=
case
(next(locked-by) = 0) : FALSE;
TRUE : waiting[0];
esac;
next(waiting[1]) :=
case
(next(locked-by) = 1) : FALSE;
TRUE : waiting[1];
esac;
FAIRNESS running
MODULE proc(id, lock)
VAR
status: {normal, trying, critical};
ASSIGN
init(status) := normal;
init(lock.waiting[id]) := FALSE;
next(status) :=
case
(status = normal) : {trying, normal};
(status = trying) & (lock.locked-by = id) : critical;
(status = critical) : normal;
TRUE : status;
esac;
next(lock.waiting[id]) :=
case
(status = normal & next(status) = trying) : TRUE;
TRUE : lock.waiting[id];
esac;
next(lock.locked-by) :=
case
(status = critical & next(status) = normal) : nobody;
TRUE : lock.locked-by;
esac;
FAIRNESS running
LTLSPEC G ((status = trying) -> F (status = critical))
MODULE main
VAR
lock: process lock;
proc0: process proc(0, lock);
proc1: process proc(1, lock);
-- safety: at most one process can enter ciritcal section.
LTLSPEC G !((proc0.status = critical) & (proc1.status = critical))
lockプロセスはwaitingがTRUEになっているプロセスのなかからlocked-byにするプロセスを選択するとともに、そのプロセスのwaitingをFALSEに戻す。
ここで next(waiting[0]) := ...
と添え字ごとに書いている箇所は添え字部分を変数にしてforeachみたいな構文で書きたいのだが、まだ調査不足でやりかたがわからない。
これを実行するとproc0については仕様が成立し、proc1については成立しない結果となるが、 lockプロセスのプロセス選択が不公平だからだ。このモデルでは両方がtryingのとき必ずproc0を優先することになっている。
ここでturnという変数を導入する。turnはプロセス数を範囲とするカウンタであり、ロックが取得されていないときは1ずつ上がっていく。 waitingからロックを与えるプロセスを決めるときはturnと一致するプロセスがtryingであるかどうかを見る。 つまりプロセスを順番に見て行って一番最初にtryingとして見つかったものにロックを与える。
MODULE lock
VAR
locked-by : {nobody, 0, 1};
waiting : array 0..1 of boolean;
turn : 0..1;
ASSIGN
init(locked-by) := nobody;
next(locked-by) :=
case
(locked-by = nobody & waiting[turn] = TRUE) : turn;
TRUE : locked-by;
esac;
next(waiting[0]) :=
case
(next(locked-by) = 0) : FALSE;
TRUE : waiting[0];
esac;
next(waiting[1]) :=
case
(next(locked-by) = 1) : FALSE;
TRUE : waiting[1];
esac;
next(turn) :=
case
(locked-by = nobody) : (turn + 1) mod 2;
TRUE : turn;
esac;
FAIRNESS running
このモデルを検証するとようやくすべての仕様が満たされた。
$ NuSMV mutex2.smv
(中略)
-- specification G (status = trying -> F status = critical) IN proc0 is true
-- specification G (status = trying -> F status = critical) IN proc1 is true
-- specification G !(proc0.status = critical & proc1.status = critical) is true
調査不足かつ情報もあまり多くないので、まだよくわかっていない部分も多い。 こうかけたらいいのに、という部分はところどころあるが、NuSMV自体の制約かもしれないし知らないだけかもしれない。
コメント 0