cloverrose's blog

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

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

Readers/Writers Algorithmについて

Readers-writers problem - Wikipedia, the free encyclopedia

このアルゴリズムの中で一番シンプルなAlgorithm1は、誰かが読込中なら書き込みはしないとか書き込み中なら読み込みはしないという安全性は満たしているんだけど、一旦Readerがセマフォwrtを獲得して、別のReaderが次々に読み込み始めるとWriterがいつまでも書き込めないという欠陥があります。

SPINモデル検査の題材として今回はこれを選んでやってみました。

参考論文

Proving Ptolemy Right: Environment Abstraction Principle for Model Checking Concurrent Systems
http://www.cs.cmu.edu/~tmurali/publications.html

Concurrent control with “readers” and “writers”
http://dl.acm.org/citation.cfm?id=362813

ソース

#define NR 2
#define NW 1
int m=0;
int w=0;
int readcount=0;
int rpc[NR];
int wpc[NW];

proctype reader(int index){
  int Nw;
  int Nm;
  int Nreadcount;
  int Nrpc;
  rpc[index]=1;
  do
  ::true ->
         atomic{
         /* initialize Nwr, Nmr, Nreadcountr and Nrpc here */
         Nw=w;
         Nm=m;
         Nreadcount=readcount;
         Nrpc=rpc[index];
         printf("wpc[0]: %d, rpc[0]: %d, rpc[1]: %d\n", wpc[0], rpc[0], rpc[1]);
         if
         ::(rpc[index]==1 && m==0) -> Nrpc=2;Nm=1;
         ::(rpc[index]==1 && m==1) -> Nrpc=1;
         ::(rpc[index]==2) -> Nrpc=3;Nreadcount++;
         ::(rpc[index]==3 && readcount==1) -> Nrpc=4;
         ::(rpc[index]==3 && readcount!=1) -> Nrpc=5;
         ::(rpc[index]==4 && w==0) -> Nrpc=5;Nw=1;
         ::(rpc[index]==4 && w==1) -> Nrpc=4;
         ::(rpc[index]==5) -> Nrpc=6;Nm=0;printf("Reader[%d] Enter CS\n", index);
         ::(rpc[index]==6) -> Nrpc=7;printf("Reader[%d] Exit CS\n", index);
         ::(rpc[index]==7 && m==0) -> Nrpc=8;Nm=1;
         ::(rpc[index]==7 && m==1) -> Nrpc=7;
         ::(rpc[index]==8) -> Nrpc=9;Nreadcount--;
         ::(rpc[index]==9 && readcount==0) -> Nrpc=10;
         ::(rpc[index]==9 && readcount!=0) -> Nrpc=11;
         ::(rpc[index]==10) -> Nrpc=11;Nw=0;
         ::(rpc[index]==11) -> Nrpc=1;Nm=0;
         ::else->skip;
         fi;
         m=Nm;
         w=Nw;
         readcount=Nreadcount;
         rpc[index]=Nrpc;
         }
  od
}

proctype writer(int index){
  int Nw;
  int Nwpc;
  wpc[index]=1;
  do
  ::true ->
         atomic{
         /* initialize Nww and Nwpc here */
         Nw=w;
         Nwpc=wpc[index];
         printf("wpc[0]: %d, rpc[0]: %d, rpc[1]: %d\n", wpc[0], rpc[0], rpc[1]);
         if
         ::(wpc[index]==1 && w==0) -> Nwpc=2;Nw=1;printf("Writer Enter CS\n");
         ::(wpc[index]==1 && w==1) -> Nwpc=1;
         ::(wpc[index]==2) -> Nwpc=3;printf("Writer Exit CS\n");
         ::(wpc[index]==3) -> Nwpc=1;Nw=0;
         ::else->skip;
         fi;
         w=Nw;
         wpc[index]=Nwpc;
         }
  od
}

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

never  {    /* <>((wpc[0]==1)&&(rpc[0]==6)&&(rpc[1]!=6)&&((wpc[0]==1)U((wpc[0]==1)&&(rpc[1]==6)))) */
T0_init:
	if
	:: (((wpc[0]==1)&&(rpc[1]==6)) && (rpc[0]==6) && (rpc[1]!=6) && (wpc[0]==1)) -> goto accept_all
	:: ((rpc[0]==6) && (rpc[1]!=6) && (wpc[0]==1)) -> goto T0_S4
	:: (1) -> goto T0_init
	fi;
T0_S4:
	if
	:: (((wpc[0]==1)&&(rpc[1]==6))) -> goto accept_all
	:: ((wpc[0]==1)) -> goto T0_S4
	fi;
accept_all:
	skip
}

説明

<>((wpc[0]==1)&&(rpc[0]==6)&&(rpc[1]!=6)&&((wpc[0]==1)U((wpc[0]==1)&&(rpc[1]==6))))

が検証したLTL式です。

rpc[idx]==6

はreaderがCS(クリティカルセクション)(読み込み中)にいるということです

wpc[idx]==1

はwriterがCS(書込み中)に入るためにセマフォwの獲得を試みているということです

(wpc[0]==1)&&(rpc[0]==6)&&(rpc[1]!=6)

はreader0がCSにいてwriter0はセマフォw待ちをしていて、reader1はCSにはいないという状態です

(wpc[0]==1)U((wpc[0]==1)&&(rpc[1]==6))

はwriterがセマフォwの獲得を試みて一度もCSに入れていないのに、reader1がCSに入ったということを表しています。

つまり式全体は、
reader0がCSに入っているのでwriter0がセマフォの開放を待っているのに、後からきたreader1がさっそうとCSに入っているということを表しています。

実行結果

$ spin -a readers_writers_algorithm1.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: end state in claim reached (at depth 489)
pan: wrote readers_writers_algorithm1.pml.trail

(Spin Version 6.1.0 -- 4 May 2011)
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 112 byte, depth reached 489, errors: 1
      198 states, stored
       25 states, matched
      223 transitions (= stored+matched)
      107 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.026	equivalent memory usage for states (stored*(State-vector + overhead))
    0.281	actual memory usage for states (unsuccessful compression: 1062.97%)
         	state-vector as stored = 1460 byte + 28 byte overhead
    4.000	memory used for hash table (-w19)
    0.534	memory used for DFS stack (-m10000)
    4.730	total actual memory usage


pan: elapsed time 0 seconds

$ spin -t -s readers_writers_algorithm1.pml
Never claim moves to line 86	[(1)]
                      wpc[0]: 0, rpc[0]: 0, rpc[1]: 1
                      /* wpc[0]==1 になるまで省略 */ 
                      wpc[0]: 0, rpc[0]: 1, rpc[1]: 11
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 2
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 3
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 4
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 5
                      Reader[1] Enter CS
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 6
                      Reader[1] Exit CS
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 7
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 8
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 9
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 10
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 11
                      wpc[0]: 1, rpc[0]: 1, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 2, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 2, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 3, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 3, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 4, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 4, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 5, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 5, rpc[1]: 1
                      Reader[0] Enter CS
Never claim moves to line 85	[((((rpc[0]==6)&&(rpc[1]!=6))&&(wpc[0]==1)))]
Never claim moves to line 91	[((wpc[0]==1))]
                      wpc[0]: 1, rpc[0]: 6, rpc[1]: 1
                      wpc[0]: 1, rpc[0]: 6, rpc[1]: 2
                      wpc[0]: 1, rpc[0]: 6, rpc[1]: 3
                      wpc[0]: 1, rpc[0]: 6, rpc[1]: 5
                      Reader[1] Enter CS
Never claim moves to line 90	[(((wpc[0]==1)&&(rpc[1]==6)))]
Never claim moves to line 94	[(1)]
spin: trail ends after 489 steps
#processes: 4
		m = 0
		w = 1
		readcount = 2
		rpc[0] = 6
		rpc[1] = 6
		wpc[0] = 1
489:	proc  3 (reader) readers_writers_algorithm1.pml:17 (state 58)
489:	proc  2 (reader) readers_writers_algorithm1.pml:17 (state 58)
489:	proc  1 (writer) readers_writers_algorithm1.pml:57 (state 24)
489:	proc  0 (:init:) readers_writers_algorithm1.pml:79 (state 4) <valid end state>
489:	proc  - (never_0) readers_writers_algorithm1.pml:95 (state 16) <valid end state>
4 processes created

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