第６章 提案手法の適用実験 36
6.2 典型的なモデル例への適用
56
修正後のモデルに対して，反例・正例出力ツールの実行結果は以下に示す．
適用実験の結果，解析ツールがモデルの誤り箇所が正しく特定できた．解析ツー ルはプロセス数が１０個程度のモデルに適用できることが分かった．また，解析に １分間未満で終了できたため，当モデル例と同じレベルのモデルに適用する時に，
性能的に問題がないことが確認できた．
57
「評価例の説明」
この評価例にインターネット上公開された並行プログレミング教科書 [8] に載 ってあるモデル例．モデルには並行システムによくある複数プロセスが同じ共有変 数に対するカウントアップ処理が記述されている．複数プロセスが全て立ち上げ，
かつカウントアップ処理が実行された後に共有変数の値がプロセスの数になる性 質が表明で書かれている．
「実験の目的」
本実験では，自作モデルではなく，教科書に載ってあるrace conditions問題のモ デルをそのまま解析ツールの入力にし，適用できるかを評価する．
反例・正例出力ツールの実行結果は以下に示す．
24 run incrementer(i);
25 i++
26 :: i >= NUMPROCS -> break 27 od;
28 }
29 atomic { 30 i = 0;
31 sum = 0;
32 do
33 :: i < NUMPROCS ->
34 sum = sum + progress[i];
35 i++
36 :: i >= NUMPROCS -> break 37 od;
38 assert(sum < NUMPROCS || counter == NUMPROCS) 39 }
40 }
$ ce incrementer 反例出力の結果：
【出力数】1
【出力先】/Users/chinteki/spin/env/incrementer_dir/NG/
正例出力の結果：
【出力数】26
【出力先】/Users/chinteki/spin/env/incrementer_dir/OK/
出力所要時間：1.790 秒
58 誤り特定ツールの適用結果は以下に示す．
誤り特定ツールが提示した修正方法でモデルを下記のように修正する．
$ java CEAnalysis incrementer 誤り箇所特定の結果：
【誤り箇所1】
次の 2 ステップがアトミック処理になっていない:
[incrementer:10行目〜incrementer:11行目]
正しい実行例: /Users/chinteki/spin/env/incrementer_dir/OK/incrementer10.trail.txt 解析所要時間 0.722秒
1 #define NUMPROCS 2 2
3 byte counter = 0;
4 byte progress[NUMPROCS];
5
6 proctype incrementer(byte me) 7 {
8 int temp;
9
10 d_step{temp = counter;
11 counter = temp + 1;}
12 progress[me] = 1;
13 } 14 15 init { 16 int i = 0;
17 int sum = 0;
18
19 atomic { 20 i = 0;
21 do
22 :: i < NUMPROCS ->
23 progress[i] = 0;
24 run incrementer(i);
25 i++
59
修正後のモデルに対して，反例・正例出力ツールの実行結果は以下に示す．
適用実験の結果，解析ツールがrace conditions問題における典型的な「並行シス テムの変数更新問題」モデルにある誤り箇所が正しく特定できることが分かった．
26 :: i >= NUMPROCS -> break 27 od;
28 }
29 atomic { 30 i = 0;
31 sum = 0;
32 do
33 :: i < NUMPROCS ->
34 sum = sum + progress[i];
35 i++
36 :: i >= NUMPROCS -> break 37 od;
38 assert(sum < NUMPROCS || counter == NUMPROCS) 39 }
40 }
$ ce incrementer_fix
指定したモデルから反例が出力されませんでした.
60
6.2.2 「読み手書き手問題」モデルへの適用
評価に使用したモデル「rw」は以下に示す．
1 #define semaphore byte 2
3 semaphore db= 1, mutex =1;
4
5 int rc = 0;
6
7 active[2] proctype reader(){
8 again:
9 if
10 ::rc==0 && db > 0 ->
11 db --;
12 rc = rc+1;
13 ::d_step{rc>0 ->
14 rc = rc+1;}
15 fi;
16
17 // "read_data_base";
18 19 if
20 ::rc==1 ->
21 db++;
22 rc = rc -1;
23 ::rc>1 ->
24 rc = rc -1;
25 fi;
26 goto again 27 }
28
29 active[1] proctype writer(){
30 again:
31 skip;
32 d_step{
33 db > 0-> db --;
34
35 // "write_data_base";
36
37 assert(rc==0);
38 db++;
39 }
40 goto again 41 }
61
「評価例の説明」
この評価例は並行システムによくあるリーダライタ問題のモデルである．
システムの振る舞いに以下な特徴を持つことを予想されている．
・ ２つの読み手と１つの書き手がいって，DBに対するアクセスをする
・ ２つの読み手が同時にDBへの読み込み可能
・ 書き手の書き込みをしている間に読み手の読み込処理は不可
提案手法の有効性を評価するため，読み手プロセスがデータベースへの読込みを する前後の処理に，本来アトミックにするべき４箇所のうち，１箇所（13行目~
14行目）をアトミックにして，残りの３箇所（10行目~11行目，20行目~22行 目，23行目~24行目）を意図的に割込まれるようにさせている．
「実験の目的」
本実験に使用しているモデルの振る舞いは比較的に複雑である．また，読み手と 書き手の処理は循環に行われる．本実験は解析ツールがこのようなモデルに対して も適用できることを評価する．また，既にアトミックにしている部分について，誤 って修正方法として提示しないことも確認する．
反例・正例出力ツールの実行結果は以下に示す．
評価に使う読み手書き手モデルの処理が循環に行われるため，反例・正例出力ツー ルで反例・正例を出力させる時に，解析に必要以上の出力を抑止するため，状態空 間の探索深さを40にして出力させた．
$ ce rw 40
反例出力の結果：
【出力数】2633
【出力先】/Users/chinteki/spin/env/rw_dir/NG/
正例出力の結果：
【出力数】732
【出力先】/Users/chinteki/spin/env/rw_dir/OK/
出力所要時間：84.499 秒
62 誤り特定ツールの適用結果は以下に示す．
誤り特定ツールが提示した修正方法でモデルを下記のように修正する．
$ java CEAnalysis rw 誤り箇所特定の結果：
【誤り箇所1】
次の 3 ステップがアトミック処理になっていない: [rw:20行目〜rw:22行目]
正しい実行例: /Users/chinteki/spin/env/rw_dir/OK/rw706.trail.txt
【誤り箇所2】
次の 2 ステップがアトミック処理になっていない: [rw:23行目〜rw:24行目]
正しい実行例: /Users/chinteki/spin/env/rw_dir/OK/rw715.trail.txt
【誤り箇所3】
次の 2 ステップがアトミック処理になっていない: [rw:10行目〜rw:11行目]
正しい実行例: /Users/chinteki/spin/env/rw_dir/OK/rw98.trail.txt 解析所要時間 18.297秒
1 #define semaphore byte 2
3 semaphore db= 1, mutex =1;
4
5 int rc = 0;
6
7 active[2] proctype reader(){
8 again:
9 if
10 ::d_step{rc==0 && db > 0 ->
11 db --;}
12 rc = rc+1;
13 ::d_step{rc>0 ->
14 rc = rc+1;}
15 fi;
16
17 // "read_data_base";
18 19 if
63
修正後のモデルに対して，反例・正例出力ツールの実行結果は以下に示す．
適用実験の結果，解析ツールがrace conditions問題における典型的な「読み手書 き手問題」モデルにある誤り箇所が正しく特定でき，ツールが提示した修正方法も 予想と一致する結果になっている．