spin によるモデル検証。 ただしここでは、モデルを記述するための言語 PROMELA ではなく、検証ツール spin のコマンドライン引数に重点をおいて記述。
最小の PROMELA コードは以下のようになる。
/* ex01.pml */
init {
skip;
}
このコードを検証する spin コマンド呼び出しは以下のようになる。
spin ex01.pml
現在のバージョンで実行すると画面に表示される結果は、
1 process created
で終わり。このコードに対して指定できるオプションとしては -v と -p がある。-v を指定すると、
Starting :init: with pid 0 1: proc 0 (:init:) line 2 "ex01.pml" (state 1) [(1)] 1 process created
と少し詳細な情報が表示される。-p を指定すると、
Starting :init: with pid 0 0: proc - (:root:) creates proc 0 (:init:) 1: proc 0 (:init:) line 2 "ex01.pml" (state 1) [(1)] 1: proc 0 (:init:) terminates 1 process created
とさらに詳しい情報が表示される。
プロセスを生成するコードは以下のようになる。proctype でプロセスの動作を記述し、run で起動する。
/* ex02.pml */
proctype A() {
skip;
}
proctype B() {
skip;
}
init {
run A();
run B();
}
最小構成と比較して指定できるコマンドライン引数が増えるわけではないので、ここはスルー。
プロセスは、各プロセスが共有するグローバル変数と、宣言したプロセス内でのみアクセスできるローカル変数を利用できる。
/* ex03.pml */
byte turn = 0;
proctype A() {
byte a;
a = turn;
turn = a + 1;
}
proctype B() {
byte b;
b = turn + 1;
turn = b;
}
init {
run A();
run B()
}
最小構成から使える -v はここでも指定できるが、さらに -g や -l を指定することで、グローバル変数やローカル変数を 合わせて表示することができる。-v を指定したとき、
spin -v ex03.pml
例えば以下のように表示される。
Starting :init: with pid 0 Starting A with pid 1 1: proc 0 (:init:) line 17 "ex03.pml" (state 1) [(run A())] Starting B with pid 2 2: proc 0 (:init:) line 18 "ex03.pml" (state 2) [(run B())] 3: proc 2 (B) line 12 "ex03.pml" (state 1) [b = (turn+1)] 4: proc 2 (B) line 13 "ex03.pml" (state 2) [turn = b] 5: proc 1 (A) line 6 "ex03.pml" (state 1) [a = turn] 6: proc 1 (A) line 7 "ex03.pml" (state 2) [turn = (a+1)] 3 processes created
ここで、 -g を合わせて指定すると、
spin -v -g ex03.pml
以下のように、グローバル変数である turn の内容がステップごとに表示される。
Starting :init: with pid 0
Starting A with pid 1
1: proc 0 (:init:) line 17 "ex03.pml" (state 1) [(run A())]
turn = 0
Starting B with pid 2
2: proc 0 (:init:) line 18 "ex03.pml" (state 2) [(run B())]
turn = 0
3: proc 1 (A) line 6 "ex03.pml" (state 1) [a = turn]
turn = 0
4: proc 1 (A) line 7 "ex03.pml" (state 2) [turn = (a+1)]
turn = 1
5: proc 2 (B) line 12 "ex03.pml" (state 1) [b = (turn+1)]
turn = 1
6: proc 2 (B) line 13 "ex03.pml" (state 2) [turn = b]
turn = 2
3 processes created
また、-l を合わせて指定した場合は以下のように、各プロセスのローカル変数が表示される。
Starting :init: with pid 0
Starting A with pid 1
1: proc 0 (:init:) line 17 "ex03.pml" (state 1) [(run A())]
Starting B with pid 2
2: proc 0 (:init:) line 18 "ex03.pml" (state 2) [(run B())]
3: proc 2 (B) line 12 "ex03.pml" (state 1) [b = (turn+1)]
B(2):b = 1
4: proc 2 (B) line 13 "ex03.pml" (state 2) [turn = b]
B(2):b = 1
5: proc 1 (A) line 6 "ex03.pml" (state 1) [a = turn]
A(1):a = 1
6: proc 1 (A) line 7 "ex03.pml" (state 2) [turn = (a+1)]
A(1):a = 1
3 processes created
両方 (-l -g) 指定した場合は、両方を表示する。
上の例のように spin をそのまま実行した場合、プロセスの実行順序によって複数の状態を取りうるコードの場合は、 spin の実行ごとにどれか一つの状態遷移を行い、その内容を表示する。 取りうる状態を対話的に選択していく方法として -i が用意されており、 動作を確認しながら、という時には有効であるが、本来の目的であるモデル検証を行う場合には表示される情報量が多すぎ、 全状態を確認するために複数回実行するのは効率が悪い。
コードが取りうるすべての状態を検証するために spin は、PROMELA コードを C コードに変換してコンパイルし、 ネイティブアプリとして実行する形で実行速度を確保している。 そしてモデル検証を自動的に行うため PROMELA コードには状態を確認する命令を置き、 あらかじめ指定した条件に適合しない状態になった場合をエラーとして通知して、後から解析する形としている。
PROMELA コードを C コードに変換してコンパイルし、実行するには、以下のコマンドを順に実行する。
spin -a ex03.pml gcc -o pan pan.c ./pan
結果は以下のように表示される。
hint: this search is more efficient if pan.c is compiled -DSAFETY
(Spin Version 5.1.6 -- 9 May 2008)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 12 byte, depth reached 2, errors: 0
3 states, stored
0 states, matched
3 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
2.501 memory usage (Mbyte)
unreached in proctype :init:
(0 of 2 states)
pan: elapsed time 0 seconds
ここで、pan.c をコンパイルする場合にマクロ定義で動作を変更する方法と、 コンパイラで生成されたコマンド ( pan ) に渡すコマンドライン引数、 さらに pan コマンド実行中に検出したエラーを解析するために使用する spin コマンドのコマンドライン引数と、 説明を続けるつもりだったが、今日はここまで。
pan.c -> pan (PAN: Process ANalyzer) と進む前に、channel について。
channel は、プロセス間のデータのやりとりを抽象化したものとなる。
/* ex04.pml */
mtype = {ping, pong};
proctype A(chan ch)
{
ch!ping; /* (a) */
ch?pong; /* (b) */
}
proctype B(chan ch)
{
ch?ping;
ch!pong;
}
init {
chan ch = [1] of {mtype}; /* (c) */
run A(ch);
run B(ch);
}
上のコードの (a) がデータの送信、(b) がデータの受信を表す。 受信の引数で定数((b) では pong)を指定した場合、その定数が受信できるまでプロセスの実行はブロックされる。
channel の生成は (c) で行っている。ここでは、channel ch が mtype (整数をシンボルで定義した、Cで言う enum のようなもの) をやりとりする、キューのサイズが 1 の channel であることを示している。
これを実行すると、process A() は ping を送信して pong 受信を待ち、process B() は ping 受信を待って pong を送信する動作を行う。
channel のやり取りを見るために spin には -r , -s , -c , -C といったオプションがある。-r , -s はそれぞれ channel の受信／送信したデータを表示する。
spin -r ex04.pml
を実行すると、
4: proc 2 (B) line 12 "ex04.pml" Recv ping <- queue 1 (ch) 6: proc 1 (A) line 7 "ex04.pml" Recv pong <- queue 1 (ch)
と表示され、
spin -s ex04.pml
を実行すると、
3: proc 1 (A) line 6 "ex04.pml" Send ping -> queue 1 (ch) 5: proc 2 (B) line 13 "ex04.pml" Send pong -> queue 1 (ch)
と表示される。また、
spin -r -s ex04.pml
のように同時に指定することも出来、この時は、
3: proc 1 (A) line 6 "ex04.pml" Send ping -> queue 1 (ch) 4: proc 2 (B) line 12 "ex04.pml" Recv ping <- queue 1 (ch) 5: proc 2 (B) line 13 "ex04.pml" Send pong -> queue 1 (ch) 6: proc 1 (A) line 7 "ex04.pml" Recv pong <- queue 1 (ch)
というように受信、送信を合わせて表示する形となる。(表示される先頭の数字は、実行するごとに異なる)
別形式で整形した表示を、-c を指定する事で行うことができる。
spin -c ex04.pml
で、
proc 0 = :init: proc 1 = A proc 2 = B q\p 0 1 2 1 . ch!ping 1 . . ch?ping 1 . . ch!pong 1 . ch?pong ------------- final state: ------------- 3 processes created
といった表示になる。
使用している channel のデータは、-C と -g を組み合わせて表示する。
spin -C -g ex04.pml
で、
chan A-ch
imported as proctype parameter by: A par 1
received from by: A
sent to by: A
chan B-ch
imported as proctype parameter by: B par 1
received from by: B
sent to by: B
chan :init:-ch
exported as run parameter by: :init: to B par 1, :init: to A par 1
と言うように、channel の名前(プロセス名-チャンネル名)、どこから指定されたものか、送受信はどこで行うかといった情報が表示される。
4月に買った SPIN の本が、引越しの荷物に紛れて見つからない。英語版は発掘済みなのに。
PAN (Process ANalyser) をコンパイルするときに、いくつかの定義を渡すことで使用メモリのサイズや対応する機能などを変更できる。
動作を変更するコンパイルオプションとして、例えば以下がある。
gcc -DNP -o pan pan.c
これは non-progress サイクルを検出する検証器を含んだコードを生成する。
pan の実行時にもいくつかのオプションを渡すことができる。
例えばコンパイル時に -DNP を指定し、pan 実行時にオプション -l を渡すことで、 non-progress cycle を検出する。
pan -l
で、だいたい動かし方が分かってきたところで PROMELA について、 と行きたい所だが、WEB に結構情報があるので(例えば、Basic Spin Manual など)、 次の例題を考え中。
基本的な形は、複数のプロセスが共通の資源(グローバル変数や channel など)に対して操作を行うモデルを実装し、以下の点を検証する形となる。
処理のその時点で満たすべき条件を確認する。条件を満たさない場合をエラーとして検出する。
assert(判定条件)
デッドロックでは無い終了状態に到達することを確認する。そのために、プログラム中で終了状態とみなす箇所を追加する構文がある。 (何も指定していないと、生成した全てのプロセスが最後まで実行され、かつ全ての channel が空であるときを終了状態とみなす)
end: /* end〜 と言うように end の3文字で始まるユニークな名前のラベルで指定する */
処理が進む(無限ループに陥らない)ことを確認する。そのために、プログラム中のループで処理が進む箇所を示す構文がある。 処理が進まないループがある (= non-progress cycles がある)事を検出するには、pan.c をコンパイルするときのオプションで -DNP を渡し、 pan -l を実行する。
progress: /* progress〜 と言うように progress の8文字で始まるユニークな名前のラベルで指定する */
後はよく分かっていない。