SPINはモデルチェッカでプログラムとか仕様とかをPromelaという言語で記述して、デッドロックしないとか調べてくれるもの。たぶんプロトコルの検証に強い。
プロセス間通信はチャンネルをつかうが、ちょっと文法のバリエーションが多いのでメモった。
// SPIN/Promelaのチャンネル操作いろいろ
// Cの文法に近い。
// セミコロンはCだとターミネータで文の終わりに必要だが、
// Promelaではセパレータで文の区切りなので最後のセミコロンは不要である。
// メッセージタイプはこんな感じで定義する。enumみたいな感じ。
mtype { ok, ng }
// チャンネル a をつくる。1メッセージためこめる。1メッセージの中身はここではタイプのみ。
chan a = [1] of { mtype }
active proctype senderA()
{
// fifo send; 順番に送信
a!ok;
a!ng // recverAがa?okしてチャンネルに空きができるまで実行されない(ブロックされる)。
}
active proctype recverA()
{
// fifo receive; 順番どおりに受信
a?ok;
a?ng
}
// 2メッセージためこめる。
chan b = [2] of { mtype }
active proctype senderB()
{
b!ok;
b!ng // ok,ngの順で送信するが..
}
active proctype recverB()
{
// random receive
b??ng; // ?? はメッセージの追い越しをして受信をする。
b??ok // もし ?? じゃなくて ? だと b?ng が成功しなくてエラー(timeout)になる。
}
chan c = [2] of { mtype }
active proctype senderC()
{
c!ok;
c!ng;
}
active proctype recverC()
{
// poll
c?<ok>; // okがエンキューされるまで待つがデキューしない。
c?<ok>; // デキューしないので何度でもできる。
c?ok;
c?<ng>;
c?<ng>;
c?ng
}
chan d = [2] of { mtype }
active proctype senderD()
{
d!ok;
d!ng
}
active proctype recverD()
{
// random poll
d??<ng>; // ?? と <〜> の組み合せ技。
d??<ok>; // ??<はトライグラフなのでcppが文句をいう...
d?ok;
d?ng
}
#if 1
chan e = [2] of { mtype }
active proctype senderE()
{
e!ok;
e!ng;
}
active proctype recverE()
{
// c?[msg] はmsgがキューイングされているかの検査でtrue(1)/false(0)を返す。
#if 1
do
:: e??[ok] && e??[ng] ->
//e??[ok];
//e??[ng];
break
:: else -> skip
od;
#else
bool rdy_ng;
bool rdy_ok;
do
:: true ->
rdy_ok = e?[ng] -> true : false;
rdy_ng = e?[ok] -> true : false;
printf("%d %d\n", rdy_ng, rdy_ok);
if
:: rdy_ng && rdy_ok -> break
:: else -> skip
fi
od;
assert(rdy_ng == true);
assert(rdy_ok == true);
#endif
e?ok;
e?ng;
}
#endif
chan f = [2] of { mtype }
active proctype senderF()
{
f!ok;
f!ng;
}
active proctype recverF()
{
mtype w;
f?w;
assert(w == ok);
w = ng;
f?eval(w); // ふつうに f?w と書くと w に受信したメッセージが入ってくるが
// この場合だと f?eval(w) は f?ng になる。
}
今回の仕事ではまったのが
chan ch[NCH] = [N] of { ... }
とチャンネルの配列でやろうしてたんだが
xr ch[0]
って書けないこと。xr,xsはそのプロセスしか受信/送信しないことを宣言するもので、これを宣言しておくとSPINが検査する空間がちっちゃくなってうれしいらいい。最新のSPINだと丁寧にも xr ch_0 のように書き換えればできるよってメッセージがでてくるけど、今回はそうはいかないのでしぶしぶあきらめ。
