spin1

Spin は Promela で制御する
演習室の PC には Spin がすでにインストールされている

hello.pml を作成

proctype Hello() {
  printf("Hello process, my pid is: %d\n", _pid);
}

init {
  run Hello();
}

実行

spin hello.pml
          Hello process, my pid is: 1
2 processes created

プロセスはproctypeからはじめる、返り値はなし
initプロセス(Cでいうところのmain())でrun プロセス名; でインスタンス化される

Spin入門

通信プロトコルを表現するPromelaを処理するもの

Prolema

通信路の情報の定義
通信するオブジェクトの定義
プログラムのひとつひとつをプロセスとしてかけば、OSの動作を模倣できる

hello02.pmlを作成

proctype Hello() {
  printf("Hello process, my pid is: %d\n", _pid);
}

init {
  int lastpid;
  printf("Init process, my pids is: %d\n",_pid);
  lastpid = run Hello();
  printf("Process %d run.\n",lastpid);
  lastpid = run Hello();
  printf("Process %d run.\n",lastpid);
}

実行結果

$ spin hello02.pml
      Init process, my pids is: 0
          Hello process, my pid is: 1
      Process 1 run.
      Process 2 run.
              Hello process, my pid is: 2
3 processes created

実行するごとに実行結果が変わる
各プロセスは「並列」に上から処理されるが、どのタイミングで切り替わるのかはランダム

pid が 1 までのとき、プロセス1が終了し、lastpid = run hello() で3つめのプロセスがディスパッチ。

spin は並列処理されているプロセスがどの順序で実行されていても検証可能なシステム→したがって、ランダムに行われる。

動作のシミュレートも行われる。

spin は処理の切り替え順を固定するオプションがある

[オプション -n]

nの右に数値をしていすることで、乱数シードを指定

$ spin -n333 hello02.pml

promelaでhyぷげんされたシステムをSPINで実行するときの時間の単位：ティック

実行中にディスパッチ(切り替え)が発生すると困る処理をatomic命令で範囲を指定して、ディスパッチを回避

atomicを使用してみる。hello03.pml

proctype Hello() {
  printf("Hello process, my pid is: %d\n", _pid);
}

init {
  int lastpid;
  printf("Init process, my pids is: %d\n",_pid);
  atomic {
    lastpid = run Hello();
    printf("Process %d run.\n",lastpid);
    lastpid = run Hello();
    printf("Process %d run.\n",lastpid);
  }
}

atomicで囲まれた部分は実行しても常に固定される！

promelaの変数は全て整数。変数はすべて初期値は0となる。
C言語の構造体を、promelaではレコードとよぶ

typedef レコード名 {
  変数宣言
};

hello04.pmlをつくる

typedef Test {
  bool flag;
  int value;
};

init {
  Test rr;
  rr.flag = true;
  rr.value = 128;
}
~

実行

$ spin hello04.pml
1 process created

C言語の列挙型に似たものがpromelaのメッセージタイプ(mtype)である

mtype = {定義したい値を,で区切って並べる};

e.g.

mtype = {ON, OFF};
mtype = {C,D};

レコードは独自の型を定義
mtypeは独自の値を定義、型の名前はmtype

promela の制御命令
promelaは各命令の実行時にティックを消費することを常に留意する

promelaではすべての文が実行可能orブロックのどちらかの状態にある
代入は常に実行可能
単独数式

計算結果が0のときブロック
0以外のとき実行可能(x+3; のとき、x=-3ならすぐブロックされる)
条件式
条件式が正しくなるとき、条件式は0となり、ブロックされる
skip
1ティックだけ動かす。常に実行可能
printf
printfの内部に数式があるとき、その数式が実行可能なら、実行可能
run
プロセス数の上限に超えるまでは実行可能。返り値はプロセスID
break
ifやdoのネストをひとつだけ抜ける。

promela の if

if
:: choice1 -> stat1.1; stat1.2; stat1.3; ...
:: choice2 -> ...
:: else
if

choiceはelseでないかぎり、重複する条件を書いて良い。そのときの処理はランダム

if
:: x==0 -> a=1;
:: x==0 -> a=2;
:: else ->
fi

これなら、aは1か2のランダム
elseはすべてのchoiceがブロックされたとき、選択される
&&や||も使用可能

promelaは文と文の間にセミコロンを打つ必要があるので、文末にセミコロンが不要のときもある

promela の do

do
:: choice -> stat; stat; ...
:: choice -> stat; ...
od;

do文では該当する条件が満たされる行のいずれかが、ランダムに実行される
doを抜けるにはbreakを使う

do の練習 trafficLight.pml

mtype = { GREEN, RED, YELLOW };

proctype TrafficLight() {
  byte state = GREEN;
  do
  :: state == GREEN -> state = YELLOW;
  :: state == YELLOW -> state = RED;
  :: state == RED -> state = GREEN;
  od
}

init {
  run TrafficLight();
  run TrafficLight();
}

spin には実行回数を予め指定できる
[-u**] **に数値を指定すればティック数の上限を指定
[-p]-pをかけば実行の詳細を記載する

spin -p -u20 trafficLight.pml