読者です 読者をやめる 読者になる 読者になる

cloverrose's blog

Python, Machine learning, Emacs, CI/CD, Webアプリなど

プロセスのローカル変数Nx系に注意

SPIN

SPINのNx系の変数をプロセスのローカル変数として定義するときは気をつけましょうという話

同時代入とNuSMVとSPINの違いについて

同時代入
x=0
y=0
x=1
y=1

書いた場合、xは1だけどyは0の状態が存在します。
一方、

x=0
y=0
x, y = (1, 1)

と書けばxが1になるのと同時にyも1になってます。これが同時代入です。

NuSMVとSPINの違い

この同時代入を表現する方法がNuSMVとSPINでは違います。(NuSMVは意識しなくても同時代入になってる)
NuSMVでは

next(x):=1;
esac;
next(y):=1;

と書いてx,yが同時に代入されるモデルが書けます。

一方SPINでは
NxやNy(Nextのxやyの値の意味)を定義して、最後に

atomic{
  x=Nx;
  y=Ny;
}

と同時代入を書きます。

SPINでつまづいたところ

変数Nxをプロセスのローカル変数として定義した時に、安全なプログラムのはずなのにクリティカルセクションに2つのプロセスが入っているというバグが見つかり悩みました。

原因はプロセスのローカル変数として定義したNxをプロセスのアトミックな実行の最初で現在のxの値を設定指定なかったからでした。


修正したReader/Writerのソースは以下

int m=0;
int w=0;
int readcount=0;
int rpc=1;
int wpc=1;

active proctype writer(){
  int Nww;
  int Nwpc;
  do
  ::true ->
         atomic{
         /* initialize Nww and Nwpc here */
         Nww=w;
         Nwpc=wpc;
         if
         ::(wpc==1 && w==0) -> Nwpc=2;
         ::(wpc==1 && w==1) -> Nwpc=1;
         ::(wpc==2) -> assert(rpc != 6);Nwpc=3;
         ::(wpc==3) -> Nwpc=1;
         ::else->skip;
         fi;
         if
         ::(wpc==1 && w==0)->Nww=1;
         ::(wpc==3)->Nww=0;
         ::else->skip;
         fi;
         w=Nww;
         wpc=Nwpc;
         }
  od
}
active proctype reader(){
  int Nwr;
  int Nmr;
  int Nreadcountr;
  int Nrpc;
  do
  ::true ->
         atomic{
         /* initialize Nwr, Nmr, Nreadcountr and Nrpc here */
         Nwr=w;
         Nmr=m;
         Nreadcountr=readcount;
         Nrpc=rpc;
         if
         ::(rpc==1 && m==0) -> Nrpc=2;
         ::(rpc==1 && m==1) -> Nrpc=1;
         ::(rpc==2) -> Nrpc=3;
         ::(rpc==3 && readcount==1) -> Nrpc=4;
         ::(rpc==3 && readcount==0) -> Nrpc=3;
         ::(rpc==4 && w==0) -> Nrpc=5;
         ::(rpc==4 && w==1) -> Nrpc=4;
         ::(rpc==5) -> Nrpc=6;
         ::(rpc==6) -> assert(wpc!=2);Nrpc=7;
         ::(rpc==7 && m==0) -> Nrpc=8;
         ::(rpc==7 && m==1) -> Nrpc=7;
         ::(rpc==8) -> Nrpc=9;
         ::(rpc==9 && readcount==0) -> Nrpc=10;
         ::(rpc==9 && readcount==1) -> Nrpc=9;
         ::(rpc==10) -> Nrpc=11;
         ::(rpc==11) -> Nrpc=1;
         ::else->skip;
         fi;
         if
         ::(rpc==1 && m==0) -> Nmr=1;
         ::(rpc==5) -> Nmr=0;
         ::(rpc==7 && m==0) -> Nmr=1;
         ::(rpc==11) -> Nmr=0;
         ::else->skip;
         fi;
         if
         ::(rpc==2) -> Nreadcountr=1;
         ::(rpc==8) -> Nreadcountr=0;
         ::else->skip;
         fi;
         if
         ::(rpc==4 && w==0) -> Nwr=1;
         ::(rpc==10) -> Nwr=0;
         ::else->skip;
         fi;
         m=Nmr;
         w=Nwr;
         readcount=Nreadcountr;
         rpc=Nrpc;
         }
  od
}

never  {    /* !([](!((rpc==6) && (wpc==2)))) */
T0_init:
	do
	:: atomic { (! ((!((rpc==6) && (wpc==2))))) -> assert(!(! ((!((rpc==6) && (wpc==2)))))) }
	:: (1) -> goto T0_init
	od;
accept_all:
	skip
}

この修正がないと、プロセスのループの最後でx=Nxの代入をした時に、else->skipでNxの値を設定していないので本来ならxの値が変わらないはずの動作でもxが別のプロセスによって更新されている場合、昔のxの値に戻してしまうという動作になってしまいます。

感想

正しいとわかってるプロトコルをモデルにして検証する場合でさえも、気をつけなければいけないポイントがいっぱいある。
実装レベルに落とすときにどこをatomicにしなければいけないか、変数の代入の順序は?といった複雑な問題を網羅的探索で解決できるのでやっぱり重要な技術だな