|
11
|
1 \section{Gears Agdaによるモデル検査の流れ}
|
|
17
|
2 今回作成した Gears Agda による DPP のモデル検査の流れは以下のようになっている。
|
|
11
|
3
|
|
16
|
4 \begin{enumerate}
|
|
|
5 \item Gears Agda にて DPP の実装を行う
|
|
|
6 \item プログラムが実行中に取りうる状態の網羅をする State List を作成する
|
|
17
|
7 \item 上で実装したものを使用しつつ Meta DataGear を構築する Meta CodeGearを記述する
|
|
18
|
8 \item 上記 Meta CodeGear で作成された meta data を元に、dead lockを判定する Meta CodeGear を記述する
|
|
|
9 \item 状態を網羅した State List にある State を一つずつ Meta CodeGear に実行させて、dead lockしている状態がないか確認する
|
|
16
|
10 \end{enumerate}
|
|
11
|
11
|
|
17
|
12 先行研究では網羅した状態データを State DB に格納していた。しかし今回の Gears Agda では State List にて代替とした。これは List で行った方が Agda での実装がしやすい点にある。本来は branced tree をデータ構造に持って State を作成するほう正しい。
|
|
11
|
13
|
|
18
|
14 dead lock の定義として、全てのプロセスが他のプロセスの実行終了待ちをしている。かつ新たに状態の分岐が作成できないものとした。
|
|
|
15 そこでstep実行してもプロセスがすべて変動がなく、かつStateの分岐が作成されなかったものを dead lock としている。
|
|
11
|
16
|
|
18
|
17 最後について、今回は状態の網羅を一度終了してから dead lock の有無を検証している。しかし、これは今回のプログラムが有限オートマトンであることは事前に明らかであるためにできたことである。検証したいプログラムが無限の状態を作成する場合は、Stateを作成するたびにそれに対して dead lock や live lock などのモデル検査をすることもできる。モデル検査中に意図しない動きがあった場合に停止するようにすることで、無限の状態を作成するプログラムであっても、モデル検査ができると考える。他にも、プログラムが取る状態を制限することで有限な状態を作成するようにし、モデル検査をすることもできる。 (bounded model checking)
|
|
11
|
18
|
|
7
|
19 \section{Gears Agda によるDPPの実装}
|
|
1
|
20
|
|
17
|
21 DPP の記述の主要部分を示し、説明する。
|
|
1
|
22
|
|
17
|
23 \lstinputlisting[caption= Gears Agdaでの DPP の 哲学者の状態 , label=code:agda-dpp-state, lastline=7]{src/agda-dpp-impl.agda.replaced}
|
|
1
|
24
|
|
17
|
25 \lstinputlisting[caption= Gears Agdaでの DPP の プロセス , label=code:agda-dpp-process, firstline=9, lastline=16]{src/agda-dpp-impl.agda.replaced}
|
|
1
|
26
|
|
17
|
27 \lstinputlisting[caption= Gears Agdaでの DPP の DataGear , label=code:agda-dpp-dg, firstline=17, lastline=21]{src/agda-dpp-impl.agda.replaced}
|
|
1
|
28
|
|
17
|
29 \coderef{agda-dpp-state}は
|
|
|
30 前述した哲学者の状態を書き記して、哲学者が今行おうとしている動作を網羅している。
|
|
1
|
31
|
|
17
|
32 \coderef{agda-dpp-process}は
|
|
|
33 哲学者一人ずつの環境を持っている。
|
|
|
34 pid はその哲学者がどこに座っているかの識別子で、
|
|
|
35 right / left hand はフォークを手に持っているかを格納している。
|
|
|
36 next-code は次に行う動作を格納している。
|
|
1
|
37
|
|
17
|
38 \coderef{agda-dpp-dg} が DataGear になる。
|
|
|
39 phは前もって定義した一人の哲学者のプロセスの List になる。
|
|
|
40 List になっている理由は、哲学者が複数人いるためである。
|
|
|
41 そのため実行時にListから一人ずつ取り出して実行をしていく。
|
|
1
|
42
|
|
17
|
43 tableはテーブルに置いてあるフォークの状態のことで、
|
|
|
44 pid が1の人の右側にあるフォークが List の最初にあり、
|
|
|
45 pid が1の人の左側にあるフォーク、すなわち pid が2の人の右側にあるフォークが
|
|
|
46 その次の List に格納されていくようになっている。
|
|
|
47 また、自然数の List になっているが、
|
|
|
48 その場所のフォークがテーブルの上にある場合は自然数の0が、
|
|
|
49 誰かが所持している場合はその人の pid が格納されるようになっている。
|
|
1
|
50
|
|
17
|
51 \lstinputlisting[caption= Gears Agdaでの DPP の DataGear のinit, label=code:agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced}
|
|
1
|
52
|
|
17
|
53 \coderef{agda-dpp-init}が入力から DataGear を作成する CodeGear になる。
|
|
|
54 ここでは哲学者の人数を自然数で受け取り、人数分の List Phi と table を一つずつ作成し env を作成している。
|
|
|
55 また、最初の哲学者の状態は思考することであるため、next-code には C\_thinking を格納している。
|
|
1
|
56
|
|
|
57 \lstinputlisting[caption= Gears Agdaでの DPP の step 実行, label=agda-dpp-step, firstline=31, lastline=37]{src/agda-dpp-impl.agda.replaced}
|
|
|
58
|
|
17
|
59 Agda では並列実行を行うことができない。そのため step 単位の実行を一つずつ行うことで
|
|
|
60 並列実行をしていることとする。
|
|
1
|
61
|
|
17
|
62 この際に Env にある List Phi の中身を展開しながら一つずつ行動を処理していく。
|
|
1
|
63
|
|
17
|
64 \lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=code:agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced}
|
|
1
|
65
|
|
17
|
66 \coderef{agda-dpp-lfork}が step 実行をした際に哲学者が左側のフォークを取る記述になる。
|
|
1
|
67
|
|
17
|
68 左側のフォークを取る際には table の index は pid の次の値になっている。
|
|
|
69 \figref{DPP} を見ると直感的に理解ができる。
|
|
1
|
70
|
|
17
|
71 最後の哲学者は一番最初のフォークを参照する必要がある。
|
|
|
72 フォークの状態を確認し、値が0である場合はフォークがテーブルの上にあるので
|
|
16
|
73 それを自分の pid に書き換える。次に left-hand を true に書き換えて手に持つ
|
|
17
|
74 フォークの状態が0以外、すなわち他の哲学者がその場所のフォークを取得している場合は
|
|
|
75 状態を変化させずに処理を続ける。
|
|
|
76 このように左のフォークを取る記述をした。
|
|
1
|
77
|
|
17
|
78 右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る。
|
|
|
79 比較するべき table の List と哲学者のListは一致しているため、pickup\_lfork のように最後の哲学者が
|
|
|
80 最初のフォークを参照することもない。
|
|
1
|
81
|
|
17
|
82 似たような形で哲学者がフォークを置く putdown-lfork/rfork を実装した。
|
|
|
83 思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている。
|
|
1
|
84
|
|
7
|
85 \section{Gears Agda によるDPPの検証}
|
|
4
|
86
|
|
18
|
87 これまでの実装は一般的なDPPの実装であったため、
|
|
17
|
88 Code / DataGear の実装であった。
|
|
18
|
89 ここからは、モデル検査を行うため、Meta DataGear の定義をし、
|
|
17
|
90 それの操作を行う Meta CodeGear の実装を行っていく。
|
|
4
|
91
|
|
17
|
92 以下\coderef{dpp-mdg}がMeta DataGear の定義になる。
|
|
4
|
93
|
|
|
94 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
|
|
17
|
95 \lstinputlisting[caption=Gears Agda で DPP のモデル検査を行うための Meta DataGear, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}
|
|
4
|
96
|
|
18
|
97 この Meta DataGear の説明をすると、
|
|
17
|
98 metadataは状態の分岐数を持っておくnum-brunchがある。
|
|
|
99 MetaEnv はもとの DataGear を保持するDG(DataGearの省略)となる。
|
|
18
|
100 meta には前述したmetadataを持っており、
|
|
|
101 他には、deadlockしているかのフラグである deadlock 、
|
|
16
|
102 最後の2つは後に必要になるフラグである。
|
|
18
|
103 そのstate が step 実行済みなのかのフラグであるis-step、
|
|
17
|
104 そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている。
|
|
4
|
105
|
|
17
|
106 MetaEnv2 は1つのstate である MetaEnv の Listを metal で持てる。
|
|
|
107 加えて今まで実行していた DataGear を DG で持てる。
|
|
4
|
108
|
|
17
|
109 次に Meta DataGear を作成する Meta CodeGear の説明をする。
|
|
12
|
110
|
|
16
|
111 \begin{enumerate}
|
|
17
|
112 \item その状態から分岐できる状態数をカウントする Meta CodeGear
|
|
|
113 \item Wait List を作成する Meta CodeGear
|
|
16
|
114 \end{enumerate}
|
|
11
|
115
|
|
17
|
116 以下の \coderef{dpp-mcg-branch} が分岐できる状態数をカウントする Meta CodeGear となる。
|
|
11
|
117
|
|
|
118 %ここにコードを載せる%
|
|
17
|
119 \lstinputlisting[caption=状態の分岐数をカウントする Meta DataGear の定義, label=code:dpp-mcg-branch]{src/dpp-verif/dpp-metacode.agda.replaced}
|
|
12
|
120
|
|
11
|
121
|
|
18
|
122 実際にやっていることは、MetaEnv2 から state を取り出し、分岐を見る関数に遷移させている。その結果の List の length を meta データとしている。
|
|
4
|
123
|
|
18
|
124 つまり、この Meta CodeGear の実装にあたって新しい実装はほとんど行っていない。
|
|
11
|
125
|
|
18
|
126 Wait List の 作成も同じように取り出した state を step させて、そこで一致するnext-codeを状態が変わっていないとして Wait List に入れている。
|
|
11
|
127
|
|
12
|
128 %いちおうコード載せようかな？←棄却されました%
|
|
11
|
129
|
|
18
|
130 Wait List について、Thinking と Eathing の状態に関しては状態が変わる可能性がある。
|
|
|
131 これを Wait List に入れなければ Wait List のみで dead lock が検知できると考えられる。しかし、DPP以外の他のプログラムをモデル検査する際に、一つ一つ next-code の設定を行うのは煩雑であると考えた。そのため、step した際に状態が変化しないものを Wait List にいれた。これと分岐がない場合という条件にて、dead lock を検知する。これにより Meta CodeGear の作成が簡易化された。そのため、Thinking と Eathing のプロセスも Waithing List に入るようになっている。
|
|
11
|
132
|
|
18
|
133 deadlockの検出方法として、上記の2つのMeta CodeGear で作成したmeta データを使用する。
|
|
11
|
134
|
|
18
|
135 そして「num-brunchの値が1であり、wait Listの数がプロセス数と一致する」ということは、「その状態から別の状態に遷移することができない」として、この状態をdead lockであると定義した。
|
|
4
|
136
|
|
16
|
137 以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる。
|
|
4
|
138
|
|
18
|
139 複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て、wait-listの数がプロセス数と一致していた場合に
|
|
|
140 deadlockのフラグを立ち上げている。これが、Gears Agda におけるアサーションになっている。
|
|
4
|
141
|
|
|
142 % judge-dead-lock-pのソースコードを貼り付ける
|
|
17
|
143 \lstinputlisting[caption=DPP での dead lock を検知する Meta CodeGear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced}
|
|
5
|
144 % こいつはmetaEnv2を受け取れるように変えないと行けない
|
|
4
|
145
|
|
18
|
146 ここから前述した通り、State Listを作成する。
|
|
4
|
147
|
|
17
|
148 そのまま実行するだけでは無限に実行されるのみで停止しないと思われる。
|
|
18
|
149 しかし、分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。
|
|
|
150 存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。
|
|
4
|
151
|
|
18
|
152 Agdaには2つの record が等しいか確かめる関数などは存在せず、
|
|
17
|
153 \coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つずつ一致しているか確認する。
|
|
18
|
154 こちらはそのまま掲載すると長いので、実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。
|
|
5
|
155
|
|
17
|
156 \lstinputlisting[caption=重複しているstateを除外する Meta CodeGear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced}
|
|
5
|
157 % 手を加えているので詳細は付録を参照するように促す
|
|
|
158
|
|
18
|
159 MetaEnv2 を受け取ってその中身の state を比較するが、そこまで展開する必要がある。
|
|
|
160 loop-metaenv と loop-target-metaenv、 eq-env にてそれを行っている。
|
|
4
|
161
|
|
18
|
162 更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し、次のstateの一致を探索するように記述されている。
|
|
5
|
163
|
|
18
|
164 実際にstateの一致を見ているのは22行目のeq-env関数で、一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている。
|
|
5
|
165
|
|
17
|
166 State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている。
|
|
18
|
167 その値が一致している場合には別の値を見て、一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。
|
|
|
168 他の値である、lhandやrhandなども eq-pid と同じように記述している。
|
|
5
|
169
|
|
6
|
170
|
|
18
|
171 これらにて、まだ分岐を見ていない1つのStateの分岐を確かめる。
|
|
17
|
172 発生した分岐を step 実行させる。
|
|
|
173 step実行して作成された state が State Listに存在していないかを確かめる。
|
|
|
174 これを繰り返すことで State Listを作る。
|
|
18
|
175 State List に存在している全ての state の分岐を見たということは、
|
|
17
|
176 出現するStateを全て網羅することができたと言える。
|
|
4
|
177
|
|
17
|
178 あとは State List を dead lock の検査を行う Meta CodeGear に与えるとどの state が dead lockしているかを検証することができる。
|
|
4
|
179
|
|
7
|
180 \section{Gears Agda による live lockの検証方法について}
|
|
18
|
181 live lockとは、状態が変動しているが、その状態はループしており、実行が進んでいないことを指す。
|
|
4
|
182
|
|
18
|
183 DPPにて例を上げると、(上の哲学者のフローだと) dead lock が発生するため、フローを変更したとする。それは以下のような動作を追加する。
|
|
|
184 「右手にフォークを持っているが、左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」
|
|
|
185 とする。これで解決すると思われるが、全員が同時に食事をしようとした場合、右手のフォークを取ったり置いたりを永遠に繰り返すことになる。
|
|
4
|
186 これを live lock という
|
|
|
187
|
|
18
|
188 つまり、この状態を検知するなら、そのstateが持っているhistoryまで考慮する必要がある。つまり、今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い。
|
|
4
|
189
|
|
18
|
190 history がloopしていた際に、誰もeathingしていない場合を live lock していると定義する。
|
|
4
|
191
|
|
18
|
192 今回のはDPPであるためEatingが挙げられているが、他の実装であれば、どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在しているかを確認することで live lock を検知できる。
|
|
4
|
193
|
|
|
194
|
|
7
|
195 \section{Gears Agda でのモデル検査の評価}
|
|
4
|
196
|
|
18
|
197 SPINで行ったDPPのモデル検査に比べると、Gears Agdaの方がコードも長く、制約が多いため難解に思える。しかし、Gears Agda ではプログラムの実装も含んでいる。
|
|
4
|
198
|
|
18
|
199 さらに、Gears Agda での実装をしたあとのモデル検査を行う際の Meta CodeGear の流れは変化しないため、他のプログラムに適応できることを考えると比較的容易であると言える。
|
|
4
|
200
|
|
18
|
201 加えて、Gears Agda は CbC へコンパイルされ、高速に実行されることを踏まえると、いかに Gears Agda が検証に向いたプログラムであるか理解できる。
|
|
4
|
202
|
|
|
203 % この評価の話はまとめでしたほうがいいかもね？
|
