同時に動くと数が合わない
競合状態とは、2つの処理が同じデータを同時に触り、動く順序しだいで結果が変わる誤りです。順序が悪いときだけ起きるので、何度テストしても見つからないことがあります。
コンビニのレジ2台が、同じ在庫表を更新します。在庫は2個で、各レジが1個ずつ売ります。2個売れたのに在庫が1個残る、という順序があります。SPIN は、その順序を探し出します。
このレッスンのゴール
メモ
トレースを読んで、2つのプロセスの競合を見つけられる。
重要な言葉
| ことば | いみ | れい |
|---|---|---|
| プロセス | 他と並んで動く、1本の処理の流れ | レジ1台 |
| 共有変数 | 複数のプロセスが読み書きする値 | stock |
| インターリーブ | 2つの流れを、順序を守って混ぜた並び | |
| 競合状態 | 順序しだいで結果が変わる誤り | |
| アサーション | ここで必ず真のはず、という検査の式 | |
| トレース | 誤りに至るまでの、1歩ずつの記録 |
学生が入力するセルは、このプレビューでは空白です。
2台のレジが在庫を書き換える
各レジは3つの動きをします。在庫を読んで覚え、覚えた数から1を引いて書き戻し、売上を1増やします。
問題は、「読む」と「書く」のあいだに、もう1台のレジが割り込めることです。両方が2を読んでから書くと、どちらも1を書きます。在庫は0でなく1になり、1個分の更新が消えます。
更新が消える順序の例
| 順 | 動くプロセス | すること | stock |
|---|---|---|---|
| 1 | 1 | 在庫を読む（2を覚える） | 2 |
| 2 | 0 | 在庫を読む（2を覚える） | 2 |
| 3 | 1 | 覚えた2から1を引いて書く | 1 |
| 4 | 1 | 売上を1増やす | 1 |
| 5 | 0 | 覚えた2から1を引いて書く | 1 |
| 6 | 0 | 売上を1増やす | 1 |
学生が入力するセルは、このプレビューでは空白です。
混ぜ方は思ったより多い
2つのプロセスが2歩ずつなら、順序を守った混ぜ方は6通りです。3歩ずつなら20通り、10歩ずつなら184756通りになります。
テストで試せるのは、そのごく一部です。モデル検査器は、全部の混ぜ方を調べます。誤りの出る順序が1つだけでも、見逃しません。
1つのプロセスの歩数と混ぜ方
| 各プロセスの歩数 | 混ぜ方の数 |
|---|---|
| 2 | 6 |
| 3 | 20 |
| 4 | 70 |
| 5 | 252 |
| 10 | 184756 |
学生が入力するセルは、このプレビューでは空白です。
Promelaでレジをモデルにする
SPIN は、Promela という言語で書いたモデルを調べます。active [2] proctype cashier() は、同じ動きをするプロセスを2つ作ります。
audit は、2台が売り終わるまで待ち、assert で在庫が0かを確かめます。sold == 2; のような式だけの文は、真になるまでそのプロセスを止めます。
レジ2台のモデル
byte stock = 2;
byte sold = 0;
active [2] proctype cashier() {
byte seen;
seen = stock;
stock = seen - 1;
sold++;
}
active proctype audit() {
sold == 2;
assert(stock == 0);
}
練習用のフォルダを作る
mkdir -p practice/shopここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
モデルのファイルを書く
printf '%s\n' "byte stock = 2;" "byte sold = 0;" "active [2] proctype cashier() {" " byte seen;" " seen = stock;" " stock = seen - 1;" " sold++;" "}" "active proctype audit() {" " sold == 2;" " assert(stock == 0);" "}" > practice/shop/shop.pmlここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
SPINで全部の順序を調べる
spinrun practice/shop/shop.pml | grep -E "violated|errors:"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
トレースは誤りまでの記録
SPIN は、誤りに至る順序を、トレースとして残します。spin -t -p は、そのトレースを1歩ずつ出し直します。
各行の proc 0 と proc 1 が、動いたレジです。最初の6歩を見ましょう。続けて、終わったときの値を取り出します。
トレースの最初の6歩
spin -t -p practice/shop/shop.pml | grep -E "^ +[0-9]+:" | head -n 6ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
終わったときの値を見る
spin -t -p practice/shop/shop.pml | grep -E "^[[:space:]]+(stock|sold) = "ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
よくある間違い
注意
同じプログラムは、動かすたびに同じ結果になる、と思いがちです。1台で動く間はそうです。複数のプロセスが共有変数を触ると、順序が毎回変わりえます。1000回通っても、1001回目に壊れることがあります。
さらに挑戦: 在庫を3個にする
shop.pml を別の名前でコピーし、stock = 2 を3にして、レジを3台にしましょう。audit は sold == 3 を待ち、assert(stock == 0) を調べます。
errors: 1 は変わるでしょうか。トレースの手数は何歩になるかを、予想してから spinrun で確かめましょう。