Spin
Install
Ubuntu なら sudo apt install -y spin
モデル検査を行う
code:bash
# モデルのソースコードをCのソースにトランスパイルする
spin -a hoge.pml
# 生成されたコード(pan.cなど)をコンパイルする
gcc -o pan pan.c
# モデル検査を実行！
./pan
例1: Hello, world
code:hello.pml
// "proctype" でプロセスを定義できる
proctype Hello(byte i) {
printf("hello, world: i=%d\n", i);
}
// "init" は起動時に実行されるプロセス
init {
// "run" で新しいプロセスを開始できる
run Hello(1);
run Hello(2);
run Hello(3);
}
code:bash
# シミュレーションモードで実行してみる (-n1 は乱数シード)
$ spin -n1 hello.pml
hello, world: i=1
hello, world: i=2
hello, world: i=3
4 processes created
code:bash
# モデル検査してみる (何の制約も書いてないので特に意味はない)
$ spin -a hello.pml
$ gcc -o pan pan.c
$ ./pan
(Spin Version 6.4.6 -- 2 December 2016)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 20 byte, depth reached 10, errors: 0
11 states, stored
0 states, matched
11 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.001 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype Hello
(0 of 2 states)
unreached in init
(0 of 4 states)
pan: elapsed time 0 seconds
シミュレーションモードは、実際に Promela をインタプリタ上で実行するモード
printf はシミュレーションモードでは実行されるが、モデル検査モードでは実行されない
シミュレーションモードはモデルのデバッグに使うらしい
例2: Counter
code:counter.pml
// グローバル変数はプロセス間で共有される。
// 初期値が指定されていない場合はゼロで初期化される。
byte count;
// カウンタの値をインクリメントする
proctype Increment(byte index) {
// read-modify-write
byte c = count;
c = c + 1;
count = c;
}
init {
run Increment(0);
run Increment(1);
// 条件文を書いた場合、trueになるまでブロックするという意味になる。
(finished0 && finished1); // 検証！！
assert(count == 2);
}
これを Spin で検証すると errors: 1 と出力され、assertion が成立しないことがわかる。
（read-modify-write を２つのプロセスがインターリーブして実行すると count が 2 じゃなくて 1 になってしまうので）
read-modify-write している３行を次の一行に置き換えると検証が通る:
count = count + 1
また、read-modify-write している３行を atomic { ... } で囲ってもOK。これでも検証が通る。
atomic は囲われたブロックの中の文が他のプロセスとインターリーブしないという意味。
（Spin 6.4.6 だとバグっていてこの例だとエラーになる → ） 例3: デッドロック検出
プリンタとスキャナが一台ずつある。
ユーザーが２人いる。
プリンタとスキャナはそれぞれ同時に一人のユーザーしか利用できない。
そのため、利用を始める前にロックする必要がある。
ユーザーはプリンタとスキャナの両方を同時に利用したい。
したがって、ユーザーはプリンタとスキャナの両方をロックしようとする。
ユーザーがプリンタとスキャナのどちらを先にロックするかは不定である。
code:printer.pml
bool printer_locked;
bool scanner_locked;
proctype User() {
if
:: true ->
atomic { (!printer_locked) -> printer_locked = true };
atomic { (!scanner_locked) -> scanner_locked = true };
skip; // use printer and scanner
scanner_locked = false;
printer_locked = false;
:: true ->
atomic { (!scanner_locked) -> scanner_locked = true };
atomic { (!printer_locked) -> printer_locked = true };
skip; // use scanner and printer
printer_locked = false;
scanner_locked = false;
fi
}
init {
run User();
run User();
}
-> と ; は Promela では同じ意味。それっぽい方を使うとよいらしい。
TODO:
never-claim
常に false であるべき命題を与え、それをモデルが満たしているかチェックする。
命題はオートマトンとして与えることもできるし、線形時相論理の式として与えることもできる。 後者のほうが人間にとって書きやすいが、表現できるクラスが小さい。
ライブロックの検出
コードに progress ラベルを付与し、progress ラベルを通らない無限ループが存在しないことをチェックする。
typedef