PlusCALで2フェーズコミット
PlusCAL Manualは、実は読み終わったのですが、後半はわりとつまらないのでここには書きません。Hyperbook は時間があれば読み進める予定。iPadで読みにくいのが難点。
さて、実践編その１としまして、AWSの人が書いた２フェーズコミットのブログ記事があるので、それを見て行きたいと思います。
Exploring TLA+ with two-phase commit - Marc's Blog
ひと通りPlusCALの文法を抑えた今なら何をしてるのかわかりますね。でも、いざブログを頼りに動くスペックを書こうとすると、エラーの嵐。細かいところは覚えてないのである程度試行錯誤が必要なのですが。。
面倒なので、PlusCALと、変換後のTLA+を両方載せてしまいますね。
-------------------------------- MODULE 2pc --------------------------------
(***************************************************************************
--algorithm 2pc {
variables
managers = { "bob", "chuck", "dave" };
restaurant_stage = [ i \in managers |-> "start" ];
process (Restaurant \in managers) {
c: await restaurant_stage[self] = "propose";
either {
restaurant_stage[self] := "accept";
} or {
restaurant_stage[self] := "refuse";
};
c1: await (restaurant_stage[self] = "commit")
\/ (restaurant_stage[self] = "abort");
if (restaurant_stage[self] = "commit") {
restaurant_stage[self] := "committed";
} else {
restaurant_stage[self] := "aborted";
};
};
process (Controller = "alice")
variable k, aborted = FALSE;
{
n: k := managers;
n2: while (k # {}) {
with (p \in k) {
restaurant_stage[p] := "propose";
k := k \ {p};
};
};
k := managers;
n3: while (k # {}) {
with (p \in k) {
await (restaurant_stage[p] = "accept")
\/ (restaurant_stage[p] = "refuse");
if (restaurant_stage[p] = "refuse") {
aborted := TRUE;
};
k := k \ {p};
};
};
k := managers;
if (aborted = TRUE) {
n6: while (k # {}) {
with (p \in k) {
restaurant_stage[p] := "abort";
k := k \ {p};
};
};
} else {
n4: while (k # {}) {
with (p \in k) {
restaurant_stage[p] := "commit";
k := k \ {p};
};
};
};
};
}
***************************************************************************)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES managers, restaurant_stage, pc, k, aborted
vars == << managers, restaurant_stage, pc, k, aborted >>
ProcSet == (managers) \cup {"alice"}
Init == (* Global variables *)
/\ managers = { "bob", "chuck", "dave" }
/\ restaurant_stage = [ i \in managers |-> "start" ]
(* Process Controller *)
/\ k = defaultInitValue
/\ aborted = FALSE
/\ pc = [self \in ProcSet |-> CASE self \in managers -> "c"
[] self = "alice" -> "n"]
c(self) == /\ pc[self] = "c"
/\ restaurant_stage[self] = "propose"
/\ \/ /\ restaurant_stage' = [restaurant_stage EXCEPT ![self] = "accept"]
\/ /\ restaurant_stage' = [restaurant_stage EXCEPT ![self] = "refuse"]
/\ pc' = [pc EXCEPT ![self] = "c1"]
/\ UNCHANGED << managers, k, aborted >>
c1(self) == /\ pc[self] = "c1"
/\ (restaurant_stage[self] = "commit")
\/ (restaurant_stage[self] = "abort")
/\ IF restaurant_stage[self] = "commit"
THEN /\ restaurant_stage' = [restaurant_stage EXCEPT ![self] = "committed"]
ELSE /\ restaurant_stage' = [restaurant_stage EXCEPT ![self] = "aborted"]
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << managers, k, aborted >>
Restaurant(self) == c(self) \/ c1(self)
n == /\ pc["alice"] = "n"
/\ k' = managers
/\ pc' = [pc EXCEPT !["alice"] = "n2"]
/\ UNCHANGED << managers, restaurant_stage, aborted >>
n2 == /\ pc["alice"] = "n2"
/\ IF k # {}
THEN /\ \E p \in k:
/\ restaurant_stage' = [restaurant_stage EXCEPT ![p] = "propose"]
/\ k' = k \ {p}
/\ pc' = [pc EXCEPT !["alice"] = "n2"]
ELSE /\ k' = managers
/\ pc' = [pc EXCEPT !["alice"] = "n3"]
/\ UNCHANGED restaurant_stage
/\ UNCHANGED << managers, aborted >>
n3 == /\ pc["alice"] = "n3"
/\ IF k # {}
THEN /\ \E p \in k:
/\ (restaurant_stage[p] = "accept")
\/ (restaurant_stage[p] = "refuse")
/\ IF restaurant_stage[p] = "refuse"
THEN /\ aborted' = TRUE
ELSE /\ TRUE
/\ UNCHANGED aborted
/\ k' = k \ {p}
/\ pc' = [pc EXCEPT !["alice"] = "n3"]
ELSE /\ k' = managers
/\ IF aborted = TRUE
THEN /\ pc' = [pc EXCEPT !["alice"] = "n6"]
ELSE /\ pc' = [pc EXCEPT !["alice"] = "n4"]
/\ UNCHANGED aborted
/\ UNCHANGED << managers, restaurant_stage >>
n6 == /\ pc["alice"] = "n6"
/\ IF k # {}
THEN /\ \E p \in k:
/\ restaurant_stage' = [restaurant_stage EXCEPT ![p] = "abort"]
/\ k' = k \ {p}
/\ pc' = [pc EXCEPT !["alice"] = "n6"]
ELSE /\ pc' = [pc EXCEPT !["alice"] = "Done"]
/\ UNCHANGED << restaurant_stage, k >>
/\ UNCHANGED << managers, aborted >>
n4 == /\ pc["alice"] = "n4"
/\ IF k # {}
THEN /\ \E p \in k:
/\ restaurant_stage' = [restaurant_stage EXCEPT ![p] = "commit"]
/\ k' = k \ {p}
/\ pc' = [pc EXCEPT !["alice"] = "n4"]
ELSE /\ pc' = [pc EXCEPT !["alice"] = "Done"]
/\ UNCHANGED << restaurant_stage, k >>
/\ UNCHANGED << managers, aborted >>
Controller == n \/ n2 \/ n3 \/ n6 \/ n4
Next == Controller
\/ (\E self \in managers: Restaurant(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================ブログ中、まずTLA+のところにvariablesを定義するぜ、とかいってるけどどう見てもそれでは動かない。なので、少し変えてあります。
一番困ったのがmacroの書き方。どこに書けばいいのかわからない。それと、C Manualをみると、macroにはwhileは使えないと書いてある。（なぜなら、macroの中にラベルを持てないから）それにもかかわらず、便利なmacroをつかうぜ！とかいってるのでわけわかめ。しょうがないので手で展開して書きました。
あとは、ハマリポイントとしては、 }のあとに；がいるのかいらないのかいちいち判別がつかん。面倒なので orで繋がる場合などをのぞき、すべて;をつけておきました。
できあがったものをとりあえず何もinvariant check無しでモデルチェックにかけると、無事ブログと同じ、718 states, 296 distinct states、となりました。checkの追加は後ほど。
一番謎なのは、これだと Aliceが各マネージャのステージをpropose, commit, abortにするところはatomicになってるんですが、それでいいの？という疑問。じつはこれ、2PCを昔見た時からずっと疑問なので、僕でもわかるように誰か教えて下さい。
