|
6
|
1 \chapter{評価}
|
|
1
|
2 \label{chapter4}
|
|
6
|
3
|
|
|
4 実装したDining Philosophers Problemのタブロー展開および、
|
|
|
5 線形時相論理による検証を組み込んだタブロー展開の評価を行う。
|
|
|
6
|
|
|
7 また、検証を組み込んだタブロー展開においては他の検証ツールとの比較を行う。
|
|
|
8
|
|
12
|
9 比較の対象としては、SPIN と Java PathFinder を用いる。CbCによる記述と合わせて、
|
|
|
10 Dining Philosophers Problemの状態空間の探索にかかる時間を測定した。
|
|
11
|
11
|
|
|
12
|
|
6
|
13 \section{実行環境と評価方法}
|
|
|
14 実行環境として表\ref{tab:machine_spec}を用いた。
|
|
|
15
|
|
0
|
16 %評価に使用したマシンのスペック
|
|
6
|
17 \begin{table}
|
|
|
18 \centering
|
|
|
19 \begin{tabular}{|c|l|} \hline
|
|
|
20 OS & FedoraCore6 \\ \hline
|
|
|
21 CPU & Intel(R) Pentium4 2.8GHz \\ \hline
|
|
|
22 MEMORY & 1GB \\ \hline
|
|
|
23 \end{tabular}
|
|
|
24 \caption{評価に使用したマシンのスペック}
|
|
|
25 \label{tab:machine_spec}
|
|
|
26 \end{table}
|
|
|
27
|
|
|
28
|
|
|
29 実行時間の計測は、Unixのtimeコマンドを用いて行う。
|
|
|
30 timeコマンドは実行に要する経過時間などを計測するためのコマンドである。
|
|
|
31 正確な結果を得るため、timeコマンドで5回計測し、その平均値を取る。
|
|
0
|
32
|
|
|
33 \section{Dining Philosophers Problemのタブロー展開}
|
|
|
34 CbCで実装したDining Philosophers Problemに対してタブロー展開を適用した。
|
|
12
|
35 プロセス(哲学者)が3〜8個の場合の計測結果は表\ref{tab:dpp_tableau}のようになった。
|
|
0
|
36
|
|
12
|
37 %\begin{table}
|
|
|
38 % \centering
|
|
|
39 % \begin{tabular}{|r|r|r|} \hline
|
|
|
40 % プロセス数 & 状態数 & 実行時間(秒) \\ \hline
|
|
|
41 % 3 & 1,340 & 0.01 \\ \hline
|
|
|
42 % 4 & 6,115 & 0.08 \\ \hline
|
|
|
43 % 5 & 38,984 & 0.66 \\ \hline
|
|
|
44 % 6 & 159,299 & 3.79 \\ \hline
|
|
|
45 % 7 & 845,529 & 27.59 \\ \hline
|
|
|
46 % 8 & 3915,727 & 199.80 \\ \hline
|
|
|
47 % \end{tabular}
|
|
|
48 % \caption{Dining Philosophers Problemのタブロー展開結果}
|
|
|
49 % \label{tab:dpp_tableau}
|
|
|
50 %\end{table}
|
|
0
|
51
|
|
6
|
52 表\ref{tab:dpp_tableau}を見ると、プロセス数に対して状態数が
|
|
|
53 指数オーダーで増加していることがわかる。
|
|
|
54 また、実行時間も同様に増加している。
|
|
|
55
|
|
10
|
56 しかし、プロセス数が5個と6個の場合の実行時間がそれぞれ0.66秒、3.79秒と速く、
|
|
6
|
57 実用レベルであると言える。
|
|
0
|
58
|
|
|
59 \section{線形時相論理を用いた検証}
|
|
|
60 Dining Philosophers Problemのデッドロックを検知するためのコードセグメントを組み込んで
|
|
6
|
61 タブロー展開を行う。
|
|
|
62 また、他の検証ツールとの比較を行う。
|
|
|
63 \\
|
|
|
64
|
|
12
|
65 プロセスが5〜8個の場合の計測結果は表\ref{tab:ltl_tableau}のようになった。
|
|
0
|
66
|
|
7
|
67 検証用のコードセグメントを組み込んでのタブロー展開は、
|
|
|
68 組み込む前のものと比べて実行時間はあまり変わっていない。
|
|
6
|
69
|
|
7
|
70 また、プロセスが5個の場合の実行結果は以下のようになっている。
|
|
|
71
|
|
|
72 \begin{center}
|
|
|
73 \begin{itembox}[l]{プロセスが5個の場合の実行結果}
|
|
|
74 \begin{verbatim}
|
|
|
75 found 38984
|
|
|
76 no more branch 38984
|
|
|
77 All done count 38984
|
|
|
78 memory_header 117030
|
|
|
79 memcmp_count 2383597
|
|
|
80 memory_body 1120
|
|
|
81 restore_count 467820
|
|
|
82 restore_size 6237600
|
|
|
83 range_count 15
|
|
|
84 range_size 200
|
|
|
85 []~p is not valid.
|
|
|
86 \end{verbatim}
|
|
|
87 \end{itembox}
|
|
|
88 \end{center}
|
|
|
89
|
|
|
90 この実行結果より、プロセスが5個の場合の状態数が38,984個であることがわかる。
|
|
|
91 また、\verb|[]~p is not valid.|という結果からデッドロックが検知されたことがわかる。
|
|
|
92 これは、命題pを「デッドロックが起きる」と定義し、
|
|
|
93 \verb|[]~p|つまり決してpが起きないことを検査した結果、
|
|
|
94 pが起きてしまったことを表している。
|
|
|
95
|
|
|
96 \subsection{SPINによるDining Philosophers Problemの検証}
|
|
|
97 SPINでDining Philosophers Problemの検証を行う。
|
|
|
98
|
|
|
99 まず、Dining Philosophers Problemをモデル化したプログラムをPROMELAで記述する。
|
|
10
|
100 そして、SPINによって検証器であるpan.cを生成しそれをコンパイル、実行する。
|
|
7
|
101
|
|
|
102 ソースコード\ref{src:dpp.prm}にPROMELAによるDining Philosophers Problemのモデルの
|
|
|
103 記述を示す。
|
|
|
104
|
|
|
105 \lstinputlisting[caption=PROMELAによるDining Philosophers Problemの記述,label=src:dpp.prm]{src/dpp.prm}
|
|
|
106
|
|
10
|
107 ソースコード\ref{src:dpp.prm}をSPINにかけるとpan.cなどのファイルが生成される。
|
|
|
108 これをgccでコンパイルすることで、実行ファイルが生成される。
|
|
7
|
109
|
|
12
|
110 プロセスが5〜8個の場合の計測結果は表\ref{tab:spin_dpp}のようになった。
|
|
7
|
111
|
|
|
112 また、プロセスが5個の場合のSPINで生成された検証器の実行結果は以下のようになった。
|
|
|
113
|
|
|
114 \begin{center}
|
|
|
115 \begin{itembox}[l]{SPINのプロセスが5個の場合の実行結果}
|
|
|
116 \begin{verbatim}
|
|
|
117 pan: assertion violated 0 (at depth 44)
|
|
|
118 (Spin Version 4.2.5 -- 2 April 2005)
|
|
|
119 + Partial Order Reduction
|
|
|
120
|
|
|
121 Full statespace search for:
|
|
|
122 never claim - (none specified)
|
|
|
123 assertion violations +
|
|
|
124 acceptance cycles - (not selected)
|
|
|
125 invalid end states +
|
|
|
126
|
|
|
127 State-vector 44 byte, depth reached 44, errors: 1
|
|
|
128 46 states, stored
|
|
|
129 16 states, matched
|
|
|
130 62 transitions (= stored+matched)
|
|
|
131 0 atomic steps
|
|
|
132 hash conflicts: 0 (resolved)
|
|
|
133
|
|
|
134 2.622 memory usage (Mbyte)
|
|
|
135 \end{verbatim}
|
|
|
136 \end{itembox}
|
|
|
137 \end{center}
|
|
|
138
|
|
|
139 \verb|assertion violated 0 (at depth 56)|がデッドロック検知を報告している部分である。
|
|
|
140 \verb|212 states, stored|が生成されたユニークな状態の数である。
|
|
|
141
|
|
|
142 \subsection{Java PathFinderによるDining Philosophers Problemの検証}
|
|
12
|
143 JPFには、例題としてDiningPhil.java\cite{bib:jpf}が用意されているのでこれを用いる。
|
|
|
144 %ソースコード\ref{src:dpp.java}はJava PathFinderのWebページ\cite{bib:jpf}
|
|
|
145 %から引用したJavaによるDining Philosophers Problemの記述である。
|
|
|
146
|
|
|
147 \lstinputlisting[caption=JavaによるDining Philosophers Problemの記述,label=src:dpp.java]{src/DiningPhil.java}
|
|
7
|
148
|
|
|
149 使い方としては、\verb|javac|によりJavaのバイトコードを生成して、
|
|
|
150 それを\verb|jpf|で実行するだけである。
|
|
|
151
|
|
10
|
152 JPFの実行結果は、状態数が出力されないため実行時間のみ比較する。
|
|
|
153 表\ref{tab:jpf_dpp}に計測結果を示す。
|
|
7
|
154
|
|
12
|
155 \begin{table}[htbp]
|
|
|
156 \begin{center}
|
|
|
157 \caption{Dining Philosophers Problemのタブロー展開結果}
|
|
|
158 \begin{tabular}{|r|r|r|} \hline
|
|
|
159 プロセス数 & 状態数 & 実行時間(秒) \\ \hline
|
|
|
160 3 & 1,340 & 0.01 \\ \hline
|
|
|
161 4 & 6,115 & 0.08 \\ \hline
|
|
|
162 5 & 38,984 & 0.66 \\ \hline
|
|
|
163 6 & 159,299 & 3.79 \\ \hline
|
|
|
164 7 & 845,529 & 27.59 \\ \hline
|
|
|
165 8 & 3915,727 & 199.80 \\ \hline
|
|
|
166 \end{tabular}
|
|
|
167 \end{center}
|
|
|
168 \label{tab:dpp_tableau}
|
|
|
169 %\end{table}
|
|
|
170
|
|
|
171 %\begin{table}
|
|
|
172 \begin{center}
|
|
|
173 \caption{Dining Philosophers Problemにデッドロック検知を組み込んだ計測結果}
|
|
|
174 \begin{tabular}{|r|r|r|} \hline
|
|
|
175 プロセス数 & 状態数 & 実行時間(秒) \\ \hline
|
|
|
176 5 & 38,984 & 0.68 \\ \hline
|
|
|
177 6 & 159,299 & 3.90 \\ \hline
|
|
|
178 7 & 845,529 & 28.48 \\ \hline
|
|
17
|
179 8 & 3,915,727 & 201.04 \\ \hline
|
|
12
|
180 \end{tabular}
|
|
|
181 \end{center}
|
|
|
182 \label{tab:ltl_tableau}
|
|
|
183 %\end{table}
|
|
|
184
|
|
|
185 %\begin{table}
|
|
|
186 \begin{center}
|
|
|
187 \caption{SPINによるDining Philosophers Problemの検証の計測結果}
|
|
|
188 \begin{tabular}{|r|r|r|} \hline
|
|
|
189 プロセス数 & 状態数 & 実行時間(秒) \\ \hline
|
|
|
190 5 & 94 & 0.008 \\ \hline
|
|
|
191 6 & 212 & 0.01 \\ \hline
|
|
|
192 7 & 494 & 0.03 \\ \hline
|
|
17
|
193 8 & 1,172 & 0.04 \\ \hline
|
|
12
|
194 \end{tabular}
|
|
|
195 \end{center}
|
|
|
196 \label{tab:spin_dpp}
|
|
|
197 %\end{table}
|
|
|
198
|
|
|
199 %\begin{table}
|
|
|
200 \begin{center}
|
|
|
201 \caption{JPFによるDining Philosophers Problemの検証の計測結果}
|
|
7
|
202 \begin{tabular}{|r|r|} \hline
|
|
|
203 プロセス数 & 実行時間(秒) \\ \hline
|
|
|
204 5 & 3.98 \\ \hline
|
|
|
205 6 & 7.33 \\ \hline
|
|
12
|
206 7 & 26.29 \\ \hline
|
|
|
207 8 & 123.16 \\ \hline
|
|
7
|
208 \end{tabular}
|
|
12
|
209 \end{center}
|
|
7
|
210 \label{tab:jpf_dpp}
|
|
|
211 \end{table}
|
|
|
212
|
|
11
|
213
|
|
12
|
214 \newpage
|
|
11
|
215 \subsection{状態数と探索時間に関する考察}
|
|
|
216
|
|
|
217 SPINによる結果は、
|
|
|
218 CbCでの検証と比べて、状態数が少ない。
|
|
12
|
219 生成される状態数が少ないことが探索時間の短さにつながっていると考えられる。
|
|
11
|
220
|
|
|
221 PROMELAの記述では、Philosopher 内部での状態遷移記述は、\verb+do/od+
|
|
|
222 の中に閉じ込められており、\verb+atomic+の内部は複数の状態に分割されない。
|
|
|
223 また、変数は{\tt fork}の配列のみなのでメモリの量的にも少なくなっている。
|
|
|
224 SPINでは PROMELAをCに変換して探索を行うので、探索自体がコンパイル
|
|
|
225 されて実行するようになっており高速である。
|
|
|
226
|
|
|
227 CbCの場合は、実際に実行可能なプログラムであり、プログラムで渡される
|
|
|
228 引数全体と大域変数全体がメモリの量となる。CbC では、
|
|
|
229 継続を表すコードセグメントへのポインタが状態を表す。CbC での記述では、
|
|
12
|
230 Philosopher の状態は8つあるので、状態数自体も指数関数的に多くなっている。
|
|
11
|
231
|
|
12
|
232 JPFは、Javaのスレッドを使った記述を使っており、Interleaving はJavaの
|
|
|
233 バイトコード単位で起きる。もちろん、完全なバイトコード単位のInterleaving
|
|
|
234 を調べているわけではなく、複数のスレッドが相互に干渉する場合の
|
|
11
|
235 組合せを調べることになる。
|
|
|
236
|
|
|
237 Java による記述ではプログラム中のオブジェクトのインスタンス変数
|
|
|
238 全体がメモリの量となる。状態は実行しているバイトコードのアドレス
|
|
|
239 によって表される。さらに、{\tt synchronized} などの記述には、
|
|
|
240 それに対応したロックがあり、それを実現するためのメモリ領域が必要である。
|
|
|
241
|
|
12
|
242 JPFの探索時間が、プロセス数が6個まではCbCの探索時間よりも遅く、
|
|
|
243 プロセス数が7個以上になるとCbCより速いのは、
|
|
|
244 CbCの実装によるものだと推測される。
|
|
|
245 CbCの実装では、メモリのBinary Treeをバランスさせていないため、
|
|
|
246 探索時間が長くなっていると考えられる。
|
|
|
247 %JPF の探索時間がCbCの探索時間よりも遅いのは、JPFがbyte code の
|
|
|
248 %実行をSimulateしていることが大きい。また、メモリ量自体と状態数もCbCに
|
|
|
249 %よる記述よりも多いと推定される。状態数自体は JPFに測定する昨日が
|
|
|
250 %ないので、これは推定である。
|
|
11
|
251
|
|
|
252 \subsection{CbCによる検証方法の利点と欠点}
|
|
|
253
|
|
|
254 [プログラムの記述方法]
|
|
|
255
|
|
|
256 SPINは、PROMELAを用いた抽象的な記述を用いているので、
|
|
|
257 検証するアルゴリズムと性質を PROMELA で書き直す必要がある。
|
|
|
258 PROMELAでは、検証する部分だけを記述することになる。
|
|
|
259 それにより探索空間自体が小さくなり、
|
|
|
260 SPINのコンパイラ的な実装とも合わせて高速な検証が可能になっている。
|
|
|
261
|
|
|
262 しかし、PROMELAでは、実際のプログラムのバグを直接見つけるこ
|
|
|
263 とは出来ない。実際、PROMELAへの変換でミスが出る場合もある。
|
|
|
264 PROMELA自体は非決定性を含む抽象的な言語であり、{\tt atomic}
|
|
|
265 の意味や、チャネルの動作などを理解するのは難しい。
|
|
|
266
|
|
|
267 CbC では、実際のプログラムの{\tt goto}文を変換する形で
|
|
|
268 検証系を生成する。したがって、PROMELAのような別な言語に
|
|
|
269 変換する必要はない。それは、つまり、新しい言語を習得する
|
|
|
270 必要がないということである。CbC言語は、Cのサブセットなので、
|
|
|
271 Cを理解しているプログラマには用意に理解できる。これは
|
|
|
272 CbCによる検証の利点である。
|
|
|
273
|
|
|
274 [同期の抽象度]
|
|
|
275
|
|
|
276 PROMELAは、もともと抽象的な言語であり、抽象的な同期を
|
|
|
277 小さく記述するのに優れている。
|
|
|
278
|
|
|
279 今回作成した検証系は、CbC のコードセグメント単位で
|
|
|
280 並列実行(Interleaving)を行う。これは実際にマルチスレッド
|
|
|
281 なので実行される並列実行とは異なる。しかし、コードセグメント
|
|
|
282 単位の実行なので、探索するべき状態遷移数は小さくなる。
|
|
|
283
|
|
|
284 実際のプログラムの並列実行と、コードセグメント単位の並列
|
|
|
285 実行は、一般的には一致しない。それらを一致させるためには、
|
|
|
286 スレッドの同期機構や、同期のための機械語を用いる必要がある。
|
|
|
287 この部分でエラーが出る可能性はある。このため、この検証系で
|
|
|
288 エラーが出ないことが、実際のCbCの並列でエラーが出ないことを
|
|
|
289 保証するわけではない。今回のCbCの検証手法は、コードセグメント
|
|
|
290 単位の同期という抽象化が入っており、抽象化された分の誤差
|
|
|
291 が入るという欠点がある。
|
|
|
292
|
|
12
|
293 JPFによる検証は、実際のプログラムをバイトコードレベルで実行する
|
|
11
|
294 ので、より正確な検証が可能である。しかし、そのために状態数
|
|
12
|
295 は多くなり、バイトコードシミュレータのオーバヘッドもあって、
|
|
11
|
296 検証に要する時間とメモリが大きくなってしまっている。
|
|
|
297
|
|
12
|
298 JPFはバイトコードによるシミュレーションであり、SPINはPROMELA を
|
|
|
299 コンパイルしたCのコードによるシミュレータにより検証を行っている。
|
|
11
|
300 CbC は、他の二つと異なり、コードセグメント部分は直接実行
|
|
|
301 される。この部分にエラーが入ることはないのがCbCによる
|
|
|
302 検証の利点であると言える。
|
|
|
303
|
|
|
304 [検証する性質の記述]
|
|
|
305
|
|
|
306 検証するときには、検証する性質を記述する必要がある。
|
|
|
307 SPINでは、LTLをPROMLEAに変換するプログラムがあり、
|
|
12
|
308 LTLにより、性質を記述する。しかし、これにより
|
|
11
|
309 状態数自体は増えるが、変換したPROMELAの記述は
|
|
|
310 Cのコンパイルされるので比較的高速にチェックすることが
|
|
|
311 可能である。
|
|
|
312 また、PROMELA中に
|
|
|
313 assert を使って式の検証をすることも出来る。
|
|
|
314
|
|
|
315 JPFでは、もっぱらassertを使った性質の記述を用いる。
|
|
|
316 時相論理的な記述は自分で、それをチェックするプログラム
|
|
|
317 をスレッドで記述する必要がある。
|
|
|
318
|
|
|
319 CbCでは、性質の記述はCbCそのもので行う。本論文で示したように
|
|
12
|
320 タブロー展開と同時に(限られた)時相論理で記述された性質を
|
|
11
|
321 ほとんどオーバヘッドなくチェックすることが出来る。
|
|
|
322 これは時相論理式のチェック自体がCbCプログラムとして
|
|
|
323 コンパイルされているからである。
|
|
|
324 これは検証系自体が、検証される言語と同じ言語で記述されている
|
|
12
|
325 ことの利点である。タブロー展開を行う{\tt goto文}
|
|
11
|
326 を適切に選択することにより、同期の抽象度を選択できることも
|
|
|
327 利点であると言える。
|
|
|
328
|
|
|
329 JPFでは一見同じ言語で検証系を記述しているように見えるが、
|
|
12
|
330 実際の検証対象はJava バイトコードであり、実装はインタプリタ
|
|
11
|
331 的にならざるを得ない。つまり、JPFでは、検証の抽象度を
|
|
|
332 上げて、状態数を少なくすると言うことが出来ない。
|
|
7
|
333
|
|
|
334
|
|
|
335 %%%end%%%
|
