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

cloverrose's blog

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

Readers/Writers Algorithm2でReaderが永遠に待ち続ける欠陥をSPINで検証

前回に引き続きSPINでReaders/Writers Algorithmを検証してみました。
今回はAlgorithm2で、Algorithm1とは反対にReaderが永遠に待ち続けるという問題があります。

ソース

#define NR 1
#define NW 2
int m1=0;
int m2=0;
int m3=0;
int r=0;
int w=0;
int readcount=0;
int writecount=0;
int rpc[NR];
int wpc[NW];

proctype reader(int index){
  int Nr;
  int Nw;
  int Nm1;
  int Nm2;
  int Nm3;
  int Nreadcount;
  int Nwritecount;
  int Nrpc;
  rpc[index]=1;
  do
  ::true ->
         atomic{
         /* initialize local variable here */
         Nr=r;
         Nw=w;
         Nm1=m1;
         Nm2=m2;
         Nm3=m3;
         Nreadcount=readcount;
         Nwritecount=writecount;
         Nrpc=rpc[index];
         printf("rpc[0]: %d, wpc[0]: %d, wpc[1]: %d\n", rpc[0], wpc[0], wpc[1]);
         if
         ::(rpc[index]==1 && m3==0) -> Nrpc=2;Nm3=1;
         ::(rpc[index]==1 && m3!=0) -> Nrpc=1;

         ::(rpc[index]==2 && r==0) -> Nrpc=3;Nr=1;
         ::(rpc[index]==2 && r!=0) -> Nrpc=2;

         ::(rpc[index]==3 && m1==0) -> Nrpc=4;Nm1=1;
         ::(rpc[index]==3 && m1!=0) -> Nrpc=3;

         ::(rpc[index]==4) -> Nrpc=5;Nreadcount++;

         ::(rpc[index]==5 && readcount==1) -> Nrpc=6;
         ::(rpc[index]==5 && readcount!=1) -> Nrpc=7;

         ::(rpc[index]==6 && w==0) -> Nrpc=7;Nw=1;
         ::(rpc[index]==6 && w!=0) -> Nrpc=6;

         ::(rpc[index]==7) -> Nrpc=8;Nm1=0;

         ::(rpc[index]==8) -> Nrpc=9;Nr=0;

         ::(rpc[index]==9) -> Nrpc=10;Nm3=0;printf("Reader[%d] Enter CS\n", index);

         ::(rpc[index]==10) -> Nrpc=11;printf("Reader[%d] Exit CS\n", index);

         ::(rpc[index]==11 && m1==0) -> Nrpc=12;Nm1=1;
         ::(rpc[index]==11 && m1!=0) -> Nrpc=11;

         ::(rpc[index]==12) -> Nrpc=13;Nreadcount--;

         ::(rpc[index]==13 && readcount==0) -> Nrpc=14;
         ::(rpc[index]==13 && readcount!=0) -> Nrpc=15;

         ::(rpc[index]==14) -> Nrpc=15;Nw=0;

         ::(rpc[index]==15) -> Nrpc=1;Nm1=0;
         fi;
         r=Nr;
         w=Nw;
         m1=Nm1;
         m2=Nm2;
         m3=Nm3;
         readcount=Nreadcount;
         writecount=Nwritecount;
         rpc[index]=Nrpc;
         }
  od
}

proctype writer(int index){
  int Nr;
  int Nw;
  int Nm1;
  int Nm2;
  int Nm3;
  int Nreadcount;
  int Nwritecount;
  int Nwpc;
  wpc[index]=1;

  do
  ::true ->
         atomic{
         /* initialize local variable here */
         Nr=r;
         Nw=w;
         Nm1=m1;
         Nm2=m2;
         Nm3=m3;
         Nreadcount=readcount;
         Nwritecount=writecount;
         Nwpc=wpc[index];

         printf("rpc[0]: %d, wpc[0]: %d, wpc[1]: %d\n", rpc[0], wpc[0], wpc[1]);
         if
         ::(wpc[index]==1 && m2==0) -> Nwpc=2;Nm2=1;
         ::(wpc[index]==1 && m2!=0) -> Nwpc=1;

         ::(wpc[index]==2) -> Nwpc=3;Nwritecount++;

         ::(wpc[index]==3 && writecount==1) -> Nwpc=4;
         ::(wpc[index]==3 && writecount!=1) -> Nwpc=5;

         ::(wpc[index]==4 && r==0) -> Nwpc=5;Nr=1;
         ::(wpc[index]==4 && r!=0) -> Nwpc=4;

         ::(wpc[index]==5) -> Nwpc=6;Nm2=0;

         ::(wpc[index]==6 && w==0) -> Nwpc=7;Nw=1;printf("Writer[%d] Enter CS\n", index);
         ::(wpc[index]==6 && w!=0) -> Nwpc=6;

         ::(wpc[index]==7) -> Nwpc=8;printf("Writer[%d] Exit CS\n", index);

         ::(wpc[index]==8) -> Nwpc=9;Nw=0;

         ::(wpc[index]==9 && m2==0) -> Nwpc=10;Nm2=1;
         ::(wpc[index]==9 && m2!=0) -> Nwpc=9;

         ::(wpc[index]==10) -> Nwpc=11;Nwritecount--;

         ::(wpc[index]==11 && writecount==0) -> Nwpc=12;
         ::(wpc[index]==11 && writecount!=0) -> Nwpc=13;

         ::(wpc[index]==12) -> Nwpc=13;Nr=0;

         ::(wpc[index]==13) -> Nwpc=1;Nm2=0;
         fi;

         r=Nr;
         w=Nw;
         m1=Nm1;
         m2=Nm2;
         m3=Nm3;
         readcount=Nreadcount;
         writecount=Nwritecount;
         wpc[index]=Nwpc;
         }
  od
}

init{
  run writer(0);
  run writer(1);
  run reader(0);
}


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

実行結果

$ spin -a readers_writers_algorithm2.pml
$ gcc pan.c
$ ./a.out -a
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan:1: assertion violated  !(((rpc[0]==2)&&(wpc[1]==7))) (at depth 7286)
pan: wrote readers_writers_algorithm2.pml.trail

(Spin Version 6.2.4 -- 8 March 2013)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (never_0)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 184 byte, depth reached 7286, errors: 1
     3002 states, stored
      779 states, matched
     3781 transitions (= stored+matched)
     1758 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.607	equivalent memory usage for states (stored*(State-vector + overhead))
    0.957	actual memory usage for states
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  129.413	total actual memory usage



pan: elapsed time 0.06 seconds
pan: rate 50033.333 states/second

$ ./spin -t -s readers_writers_algorithm2.pml
starting claim 3
using statement merging
Never claim moves to line 169	[(1)]
                      rpc[0]: 1, wpc[0]: 0, wpc[1]: 0
                      /* wpc[0]==0 の区間を省略 */
                      rpc[0]: 2, wpc[0]: 0, wpc[1]: 5
                      /* wpc[0]が動き出すまで省略 */
                      rpc[0]: 2, wpc[0]: 1, wpc[1]: 5
                      rpc[0]: 1, wpc[0]: 1, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 1, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 6
                      Writer[1] Enter CS
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 7
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 7
                      Writer[1] Exit CS
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 8
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 8
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 2, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 3, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 3, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 3, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 3, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 3, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 5, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 5, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 5, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 10
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 10
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 11
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 11
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 13
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 13
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 1
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 1
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 2
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 2
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 3
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 3
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 5
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 5
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 6
                      Writer[1] Enter CS
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 7
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 7
                      Writer[1] Exit CS
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 8
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 8
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 6, wpc[1]: 9
                      Writer[0] Enter CS
Never claim moves to line 168	[(((((rpc[0]==2)&&(wpc[0]==7))&&(wpc[1]!=7))&&(rpc[0]==2)))]
Never claim moves to line 174	[((rpc[0]==2))]
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 9
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 10
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 10
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 11
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 11
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 13
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 13
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 1
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 1
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 2
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 2
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 3
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 3
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 5
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 5
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 7, wpc[1]: 6
                      Writer[0] Exit CS
                      rpc[0]: 2, wpc[0]: 8, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 8, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 8, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 9, wpc[1]: 6
                      rpc[0]: 2, wpc[0]: 9, wpc[1]: 6
                      Writer[1] Enter CS
spin: readers_writers_algorithm2.pml:173, Error: assertion violated
spin: text of failed assertion: assert(!(((rpc[0]==2)&&(wpc[1]==7))))
Never claim moves to line 173	[assert(!(((rpc[0]==2)&&(wpc[1]==7))))]
spin: trail ends after 7287 steps
#processes: 4
		m1 = 0
		m2 = 0
		m3 = 1
		r = 1
		w = 1
		readcount = 0
		writecount = 2
		rpc[0] = 2
		wpc[0] = 9
		wpc[1] = 7
7287:	proc  3 (reader) readers_writers_algorithm2.pml:25 (state 80)
7287:	proc  2 (writer) readers_writers_algorithm2.pml:97 (state 73)
7287:	proc  1 (writer) readers_writers_algorithm2.pml:99 (state 72)
7287:	proc  0 (:init:) readers_writers_algorithm2.pml:161 (state 4) <valid end state>
7287:	proc  - (never_0) readers_writers_algorithm2.pml:172 (state 16)
4 processes created

実行結果が長いですがrpc[0]: 2, wpc[0]: 7, wpc[1]: 9の状態からrpc[0]==2のままでwpc[1]==7に遷移していることがわかります。