--- a/paper/chapter4.tex	Fri Feb 15 19:00:41 2008 +0900
+++ b/paper/chapter4.tex	Fri Feb 15 19:59:17 2008 +0900
@@ -6,6 +6,10 @@
 
 また、検証を組み込んだタブロー展開においては他の検証ツールとの比較を行う。
 
+比較の対象としては、SPIN と JavaPathFinder を用いる。CbCによる記述と合わせて、
+Dining Philosopher 問題の状態空間の探索にかかる時間を測定した。
+
+
 \section{実行環境と評価方法}
 実行環境として表\ref{tab:machine_spec}を用いた。
 
@@ -22,7 +26,6 @@
 \end{table}
 
 
-評価の方法については、実行時間を計測することで行う。
 実行時間の計測は、Unixのtimeコマンドを用いて行う。
 timeコマンドは実行に要する経過時間などを計測するためのコマンドである。
 正確な結果を得るため、timeコマンドで5回計測し、その平均値を取る。
@@ -128,14 +131,6 @@
     \label{tab:spin_dpp}
 \end{table}
 
-CbCでの検証と比べて、状態数が少ない。
-そのため、実行にかかる時間も高速であった。
-状態数が少ない理由として、PROMELAでのDining Philosophers Problemは
-抽象化して記述されるためだと考えられる。
-
-CbCの場合は、実際に実行可能なプログラムを逐次実行していくことで状態を変化
-させているため、モデル化した記述よりも状態数が多くなっていると考えられる。
-
 また、プロセスが5個の場合のSPINで生成された検証器の実行結果は以下のようになった。
 
 \begin{center}
@@ -186,8 +181,121 @@
     \label{tab:jpf_dpp}
 \end{table}
 
-JPFもCbCと同様に実際に実行可能なバイトコードに対して検証が可能である。
-プロセス数に対する実行時間を比較するとCbCの方が速いことがわかる。
+
+\subsection{状態数と探索時間に関する考察}
+
+SPINによる結果は、
+CbCでの検証と比べて、状態数が少ない。
+生成される状態数が少ないことが探索時間の短さにつながっている
+考えられる。
+
+PROMELAの記述では、Philosopher 内部での状態遷移記述は、\verb+do/od+
+の中に閉じ込められており、\verb+atomic+の内部は複数の状態に分割されない。
+また、変数は{\tt fork}の配列のみなのでメモリの量的にも少なくなっている。
+SPINでは PROMELAをCに変換して探索を行うので、探索自体がコンパイル
+されて実行するようになっており高速である。
+
+CbCの場合は、実際に実行可能なプログラムであり、プログラムで渡される
+引数全体と大域変数全体がメモリの量となる。CbC では、
+継続を表すコードセグメントへのポインタが状態を表す。CbC での記述では、
+Philosopher の状態は5つあるので、状態数自体も指数関数的に多くなっている。
+
+JPFは、JavaのThreadを使った記述を使っており、Interleaving はJavaの
+byte code 単位で起きる。もちろん、完全なbyte code 単位のInterleaving
+を調べているわけではなく、複数のThreadが相互に干渉する場合の
+組合せを調べることになる。
+
+Java による記述ではプログラム中のオブジェクトのインスタンス変数
+全体がメモリの量となる。状態は実行しているバイトコードのアドレス
+によって表される。さらに、{\tt synchronized} などの記述には、
+それに対応したロックがあり、それを実現するためのメモリ領域が必要である。
+
+JPF の探索時間がCbCの探索時間よりも遅いのは、JPFがbyte code の
+実行をSimulateしていることが大きい。また、メモリ量自体と状態数もCbCに
+よる記述よりも多いと推定される。状態数自体は JPFに測定する昨日が
+ないので、これは推定である。
+
+\subsection{CbCによる検証方法の利点と欠点}
+
+[プログラムの記述方法]
+
+SPINは、PROMELAを用いた抽象的な記述を用いているので、
+検証するアルゴリズムと性質を PROMELA で書き直す必要がある。
+PROMELAでは、検証する部分だけを記述することになる。
+それにより探索空間自体が小さくなり、
+SPINのコンパイラ的な実装とも合わせて高速な検証が可能になっている。
+
+しかし、PROMELAでは、実際のプログラムのバグを直接見つけるこ
+とは出来ない。実際、PROMELAへの変換でミスが出る場合もある。
+PROMELA自体は非決定性を含む抽象的な言語であり、{\tt atomic}
+の意味や、チャネルの動作などを理解するのは難しい。
+
+CbC では、実際のプログラムの{\tt goto}文を変換する形で
+検証系を生成する。したがって、PROMELAのような別な言語に
+変換する必要はない。それは、つまり、新しい言語を習得する
+必要がないということである。CbC言語は、Cのサブセットなので、
+Cを理解しているプログラマには用意に理解できる。これは
+CbCによる検証の利点である。
+
+[同期の抽象度]
+
+PROMELAは、もともと抽象的な言語であり、抽象的な同期を
+小さく記述するのに優れている。
+
+今回作成した検証系は、CbC のコードセグメント単位で
+並列実行(Interleaving)を行う。これは実際にマルチスレッド
+なので実行される並列実行とは異なる。しかし、コードセグメント
+単位の実行なので、探索するべき状態遷移数は小さくなる。
+
+実際のプログラムの並列実行と、コードセグメント単位の並列
+実行は、一般的には一致しない。それらを一致させるためには、
+スレッドの同期機構や、同期のための機械語を用いる必要がある。
+この部分でエラーが出る可能性はある。このため、この検証系で
+エラーが出ないことが、実際のCbCの並列でエラーが出ないことを
+保証するわけではない。今回のCbCの検証手法は、コードセグメント
+単位の同期という抽象化が入っており、抽象化された分の誤差
+が入るという欠点がある。
+
+JPFによる検証は、実際のプログラムをbyte code levelで実行する
+ので、より正確な検証が可能である。しかし、そのために状態数
+は多くなり、byte code simulator のオーバヘッドもあって、
+検証に要する時間とメモリが大きくなってしまっている。
+
+JPFはバイトコードによるSimulationであり、SPINはPROMELA を
+コンパイルしたCのコードによるSimulatorにより検証を行っている。
+CbC は、他の二つと異なり、コードセグメント部分は直接実行
+される。この部分にエラーが入ることはないのがCbCによる
+検証の利点であると言える。
+
+[検証する性質の記述]
+
+検証するときには、検証する性質を記述する必要がある。
+SPINでは、LTLをPROMLEAに変換するプログラムがあり、
+LTLにより、性質を記述する。しかし、これにょり
+状態数自体は増えるが、変換したPROMELAの記述は
+Cのコンパイルされるので比較的高速にチェックすることが
+可能である。
+また、PROMELA中に
+assert を使って式の検証をすることも出来る。
+
+JPFでは、もっぱらassertを使った性質の記述を用いる。
+時相論理的な記述は自分で、それをチェックするプログラム
+をスレッドで記述する必要がある。
+
+CbCでは、性質の記述はCbCそのもので行う。本論文で示したように
+Tableau 展開と同時に(限られた)時相論理にで記述された性質を
+ほとんどオーバヘッドなくチェックすることが出来る。
+これは時相論理式のチェック自体がCbCプログラムとして
+コンパイルされているからである。
+これは検証系自体が、検証される言語と同じ言語で記述されている
+ことの利点である。Tableau 展開を行う{\tt goto文}
+を適切に選択することにより、同期の抽象度を選択できることも
+利点であると言える。
+
+JPFでは一見同じ言語で検証系を記述しているように見えるが、
+実際の検証対象はJava byte code であり、実装はインタプリタ
+的にならざるを得ない。つまり、JPFでは、検証の抽象度を
+上げて、状態数を少なくすると言うことが出来ない。
 
 
 %%%end%%%