鍵をかけるのにも順序がある
ロックとは、同じ部分を同時に1つのプロセスしか実行できないようにする仕組みです。共有のデータを守るために使いますが、書き方が悪いと、ロックそのものに競合が起きます。
レジの鍵が空いているかを調べ、空いていれば鍵をかけます。この2つを別々の歩にすると、2台が同時に「空いている」と見て、両方が入ってしまいます。SPIN で、その誤りと直し方を確かめます。
このレッスンのゴール
メモ
ロックを書いて、SPIN がエラーなしと報告するようにできる。
重要な言葉
| ことば | いみ | れい |
|---|---|---|
| ロック | 同時に1つだけが入れるようにする鍵 | |
| クリティカルセクション | 同時に1つだけが実行してよい部分 | |
| 相互排除 | 2つが同時にその部分へ入らない性質 | |
| アトミック | 途中で割り込まれない、1つの歩 | atomic { ... } |
| デッドロック | 全員が待ち、誰も進めなくなること | |
| 不正な終了状態 | 終わるはずなのに、進めずに止まった状態 | invalid end state |
学生が入力するセルは、このプレビューでは空白です。
調べると取るを別々にした鍵
till は鍵です。0が空き、1が使用中です。till == 0; は鍵が空くまで待つ文で、till = 1; が鍵をかけます。
inside は、いまレジの中にいる人数です。inside++ から inside-- までがクリティカルセクションで、そこに入れるのは1台だけのはずです。assert(inside == 1) が、それを見張ります。
2歩の鍵のモデル
bit till = 0;
byte inside = 0;
active [2] proctype cashier() {
till == 0;
till = 1;
inside++;
assert(inside == 1);
inside--;
till = 0;
}
練習用のフォルダを作る
mkdir -p practice/tillここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
2歩の鍵のファイルを書く
printf '%s\n' "bit till = 0;" "byte inside = 0;" "active [2] proctype cashier() {" " till == 0;" " till = 1;" " inside++;" " assert(inside == 1);" " inside--;" " till = 0;" "}" > practice/till/twostep.pmlここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
SPINに2歩の鍵を調べさせる
spinrun practice/till/twostep.pml | grep -E "violated|errors:"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
2台とも空いていると見る
errors: 1 は、鍵があるのに、2台が同時に入れる順序がある、という意味です。トレースを見ましょう。
最初の7歩を出します。8歩目で assertion violated になります。両方が till == 0 を通ってから、どちらも鍵をかけています。鍵をかけた時点では、もう手遅れです。
トレースの最初の7歩
spin -t -p practice/till/twostep.pml | grep -E "^ +[0-9]+:" | head -n 7ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
入り込む順序の表
| 順 | 動くプロセス | すること | till | inside |
|---|---|---|---|---|
| 1 | 1 | till == 0 を通る（空き） | 0 | 0 |
| 2 | 0 | till == 0 を通る（空き） | 0 | 0 |
| 3 | 1 | till = 1（鍵をかける） | 1 | 0 |
| 4 | 1 | inside を増やす | 1 | 1 |
| 5 | 1 | assert は成り立つ | 1 | 1 |
| 6 | 0 | till = 1（鍵をかける） | 1 | 1 |
| 7 | 0 | inside を増やす | 1 | 2 |
| 8 | 0 | assert が破れる | 1 | 2 |
学生が入力するセルは、このプレビューでは空白です。
調べて取るを1歩にする
直し方は、調べることと取ることを、割り込まれない1歩にまとめることです。Promela では、atomic { ... } で囲みます。
atomic { till == 0; till = 1 } なら、空いているのを見た直後に、鍵をかけるところまでが1歩です。そのあいだに、もう1台は動けません。次に、この鍵を書いて調べます。
atomicの鍵のファイルを書く
printf '%s\n' "bit till = 0;" "byte inside = 0;" "active [2] proctype cashier() {" " atomic { till == 0; till = 1 }" " inside++;" " assert(inside == 1);" " inside--;" " till = 0;" "}" > practice/till/atomic.pmlここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
SPINにatomicの鍵を調べさせる
spinrun practice/till/atomic.pml | grep -E "violated|errors:"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
鍵を返し忘れると全員が止まる
相互排除が守られても、鍵を返し忘れれば、次のレジは待ち続けます。デッドロックです。
SPIN は、errors: 1 と並べて invalid end state と報告します。アサーションは破れていません。進めずに止まった状態が見つかった、という意味です。
返し忘れのファイルを書く
printf '%s\n' "bit till = 0;" "byte inside = 0;" "active [2] proctype cashier() {" " atomic { till == 0; till = 1 }" " inside++;" " assert(inside == 1);" " inside--;" "}" > practice/till/leak.pmlここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
SPINに返し忘れを調べさせる
spinrun practice/till/leak.pml | grep -E "state \(|errors:"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
よくある間違い
注意
errors: 0 と出たら、ロックは完璧だ、と思いがちです。errors: 0 は、書いたアサーションが破れず、止まる状態もない、という意味だけです。アサーションが、鍵なしでは破れることを先に確かめましょう。破れないアサーションは、何も保証しません。
さらに挑戦: 3台目のレジ
atomic.pml を別の名前でコピーし、active [2] を active [3] に変えて、spinrun で調べましょう。errors は変わるでしょうか。
次に、inside--; の行を消して調べます。何が起き、どのアサーションが破れるかを、トレースで読みましょう。