C Manual (PlusCAL)に浮気 - tyonekuraの日記

Hyperbookの4.9に入ったら、Lamport先生我慢できなくなったのか、「でもやっぱり数学的証明も必要だよね」みたいなかんじで証明モードに入ったため、ややゲッソリして PlusCALのC Manualをつまみ食い。（PlusCALには、Cっぽい文法とPascalっぽい文法の２通りある。）

以前の記事では2.5のユークリッド法まで試してあったので、2.6へ。複数プロセス間の排他制御のアルゴリズム。いままで学んだことを踏まえると、なんとか理解できる。

process (Proc \in 1..N)

がN個のプロセスで動くことを宣言する。それぞれのプロセスは、process行の後に宣言された変数をローカル変数として持ち、selfを自分のプロセス番号を示す変数として持つ。（番号、というとintっぽいけど、それは Proc \in 1..N で宣言してるからであって、文字列にすることも可能。）

LTA+に変換されると、pcがアレイになり、pc[index]で各プロセスの現在のラベルを表す模様。（まだ実際に試してみてないので、予想）

2.7 ラベルはどこにつくのか。色々とルールが有る。それほど気にする必要はなさそうだ。while文にはラベルがつく必要がある。つまり、

process (Proc \in 1..4)
{ while (True) {
   action1;
   action2;
   action3;
}}

という一番簡単なスペックがあったとすると、自動ではwhileループにのみラベルがつく。１番目のプロセス（１から４のどれか）がaction1,2,3を一回実行し、次のプロセスがaction1,2,3を実行し、... となる。

それを以下のようにラベルを付けたとしよう。

process (Proc \in 1..4)
{ a: while (True) {
   b: action1;
   c: action2;
   d: action3;
}}

すると、Process1がaを実行して、次に(Process1がbを実行するか）他のプロセスがaを実行して、と並列動作が行われる。Process1がa,b,c,dと実行してからProcess3がa,b,c,dと実行するかもしれないし、Process2がa,b,cといったところでProcess4がaを実行し、Process1がa,b,c,dと実行するかもしれない。その組み合わせをLTA+は検証してくれる。

では、実際に試してみよう。

EXTENDS Integers, TLC

(***************************************************************************
--algorithm Counter {
variables x = 0; i = 0;

process (Proc \in 1..2)
variable j;
{a: while (i < 5) {
j := x;
x := j + 1;
i := i + 1;
};
\*print <<"counter is ", x>>;
};

}
 ***************************************************************************)

(print文は邪魔なのでコメントアウトしてある。assert使ってないのでTLCはいらない)

プロセス２つで、カウンターXを５回インクリメントしたい。ループに使っているiはアトミックに i := i + 1で増やしているので必ず５回になるはず。さて、xの値は一度 jに入れて、それに１を足している。この状態でTLA+に変換し、Modelのinvariantsに以下を入れて動かしてみよう。

(\A self \in ProcSet: pc[self] = "Done")=> x = 5

つまり、終了条件になっていれば、xは5であるはず。

動かしてみると、成功する。LTA+に変換後のスペックを見るとわかるけれど、xの値はatomicに変更されている。

これを、以下のように変える。（process部分のみ載せている）

process (Proc \in 1..2)
variable j;
{a: while (i < 5) {
b: j := x;
c: x := j + 1;
i := i + 1;
};
};
 ***************************************************************************)

で、変換してモデルチェック。すると、今回は失敗してくれる。xが４になるパターンで停止して、どういう順序で実行されたらxが4で終わるかを教えてくれる。

思ったよりも期待通りの動きをしてくれた。なかなか楽しい。

さて、2.7が終わり、C Manualの３章は言語スペックに入るようなので、またHyperbookに戻ろうかと思う。