SSブログ

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自体の制約かもしれないし知らないだけかもしれない。


nice!(0)  コメント(0)  トラックバック(0) 

nice! 0

コメント 0

コメントを書く

お名前:
URL:
コメント:
画像認証:
下の画像に表示されている文字を入力してください。

トラックバック 0

この広告は前回の更新から一定期間経過したブログに表示されています。更新すると自動で解除されます。