\chapter{評価}
\label{chapter4}

実装したDining Philosophers Problemのタブロー展開および、
線形時相論理による検証を組み込んだタブロー展開の評価を行う。

また、検証を組み込んだタブロー展開においては他の検証ツールとの比較を行う。

比較の対象としては、SPIN と Java PathFinder を用いる。CbCによる記述と合わせて、
Dining Philosophers Problemの状態空間の探索にかかる時間を測定した。


\section{実行環境と評価方法}
実行環境として表\ref{tab:machine_spec}を用いた。

%評価に使用したマシンのスペック
\begin{table}
    \centering
    \begin{tabular}{|c|l|} \hline
	OS & FedoraCore6 \\ \hline
	CPU & Intel(R) Pentium4 2.8GHz \\ \hline
	MEMORY & 1GB \\ \hline
    \end{tabular}
    \caption{評価に使用したマシンのスペック}
    \label{tab:machine_spec}
\end{table}


実行時間の計測は、Unixのtimeコマンドを用いて行う。
timeコマンドは実行に要する経過時間などを計測するためのコマンドである。
正確な結果を得るため、timeコマンドで5回計測し、その平均値を取る。

\section{Dining Philosophers Problemのタブロー展開}
CbCで実装したDining Philosophers Problemに対してタブロー展開を適用した。
プロセス(哲学者)が3〜8個の場合の計測結果は表\ref{tab:dpp_tableau}のようになった。

%\begin{table}
%    \centering
%    \begin{tabular}{|r|r|r|} \hline
%	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
%	3 & 1,340 & 0.01 \\ \hline
%	4 & 6,115 & 0.08 \\ \hline
%	5 & 38,984 & 0.66 \\ \hline
%	6 & 159,299 & 3.79 \\ \hline
%	7 & 845,529 & 27.59 \\ \hline
%	8 & 3915,727 & 199.80 \\ \hline
%    \end{tabular}
%    \caption{Dining Philosophers Problemのタブロー展開結果}
%    \label{tab:dpp_tableau}
%\end{table}

表\ref{tab:dpp_tableau}を見ると、プロセス数に対して状態数が
指数オーダーで増加していることがわかる。
また、実行時間も同様に増加している。

しかし、プロセス数が5個と6個の場合の実行時間がそれぞれ0.66秒、3.79秒と速く、
実用レベルであると言える。

\section{線形時相論理を用いた検証}
Dining Philosophers Problemのデッドロックを検知するためのコードセグメントを組み込んで
タブロー展開を行う。
また、他の検証ツールとの比較を行う。
\\

プロセスが5〜8個の場合の計測結果は表\ref{tab:ltl_tableau}のようになった。

検証用のコードセグメントを組み込んでのタブロー展開は、
組み込む前のものと比べて実行時間はあまり変わっていない。

また、プロセスが5個の場合の実行結果は以下のようになっている。

\begin{center}
\begin{itembox}[l]{プロセスが5個の場合の実行結果}
\begin{verbatim}
found 38984
no more branch 38984
All done count 38984
	memory_header 117030
	memcmp_count 2383597
	memory_body 1120
	restore_count 467820
	restore_size 6237600
	range_count 15
	range_size 200
[]~p is not valid.
\end{verbatim}
\end{itembox}
\end{center}

この実行結果より、プロセスが5個の場合の状態数が38,984個であることがわかる。
また、\verb|[]~p is not valid.|という結果からデッドロックが検知されたことがわかる。
これは、命題pを「デッドロックが起きる」と定義し、
\verb|[]~p|つまり決してpが起きないことを検査した結果、
pが起きてしまったことを表している。

\subsection{SPINによるDining Philosophers Problemの検証}
SPINでDining Philosophers Problemの検証を行う。

まず、Dining Philosophers Problemをモデル化したプログラムをPROMELAで記述する。
そして、SPINによって検証器であるpan.cを生成しそれをコンパイル、実行する。

ソースコード\ref{src:dpp.prm}にPROMELAによるDining Philosophers Problemのモデルの
記述を示す。

\lstinputlisting[caption=PROMELAによるDining Philosophers Problemの記述,label=src:dpp.prm]{src/dpp.prm}

ソースコード\ref{src:dpp.prm}をSPINにかけるとpan.cなどのファイルが生成される。
これをgccでコンパイルすることで、実行ファイルが生成される。

プロセスが5〜8個の場合の計測結果は表\ref{tab:spin_dpp}のようになった。

また、プロセスが5個の場合のSPINで生成された検証器の実行結果は以下のようになった。

\begin{center}
\begin{itembox}[l]{SPINのプロセスが5個の場合の実行結果}
\begin{verbatim}
pan: assertion violated 0 (at depth 44)
(Spin Version 4.2.5 -- 2 April 2005)
        + Partial Order Reduction

Full statespace search for:
	never claim             - (none specified)
	assertion violations    +
	acceptance   cycles     - (not selected)
	invalid end states      +

State-vector 44 byte, depth reached 44, errors: 1
	46 states, stored
	16 states, matched
	62 transitions (= stored+matched)
	  0 atomic steps
hash conflicts: 0 (resolved)

2.622   memory usage (Mbyte)
\end{verbatim}
\end{itembox}
\end{center}

\verb|assertion violated 0 (at depth 56)|がデッドロック検知を報告している部分である。
\verb|212 states, stored|が生成されたユニークな状態の数である。

\subsection{Java PathFinderによるDining Philosophers Problemの検証}
JPFには、例題としてDiningPhil.java\cite{bib:jpf}が用意されているのでこれを用いる。
%ソースコード\ref{src:dpp.java}はJava PathFinderのWebページ\cite{bib:jpf}
%から引用したJavaによるDining Philosophers Problemの記述である。

\lstinputlisting[caption=JavaによるDining Philosophers Problemの記述,label=src:dpp.java]{src/DiningPhil.java}

使い方としては、\verb|javac|によりJavaのバイトコードを生成して、
それを\verb|jpf|で実行するだけである。

JPFの実行結果は、状態数が出力されないため実行時間のみ比較する。
表\ref{tab:jpf_dpp}に計測結果を示す。

\begin{table}[htbp]
    \begin{center}
    \caption{Dining Philosophers Problemのタブロー展開結果}
    \begin{tabular}{|r|r|r|} \hline
	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
	3 & 1,340 & 0.01 \\ \hline
	4 & 6,115 & 0.08 \\ \hline
	5 & 38,984 & 0.66 \\ \hline
	6 & 159,299 & 3.79 \\ \hline
	7 & 845,529 & 27.59 \\ \hline
	8 & 3915,727 & 199.80 \\ \hline
    \end{tabular}
    \end{center}
    \label{tab:dpp_tableau}
%\end{table}

%\begin{table}
    \begin{center}
    \caption{Dining Philosophers Problemにデッドロック検知を組み込んだ計測結果}
    \begin{tabular}{|r|r|r|} \hline
	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
	5 & 38,984 & 0.68 \\ \hline
	6 & 159,299 & 3.90 \\ \hline
	7 & 845,529 & 28.48 \\ \hline
	8 & 3,915,727 & 201.04 \\ \hline
    \end{tabular}
    \end{center}
    \label{tab:ltl_tableau}
%\end{table}

%\begin{table}
    \begin{center}
    \caption{SPINによるDining Philosophers Problemの検証の計測結果}
    \begin{tabular}{|r|r|r|} \hline
	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
	5 & 94 & 0.008 \\ \hline
	6 & 212 & 0.01 \\ \hline
	7 & 494 & 0.03 \\ \hline
	8 & 1,172 & 0.04 \\ \hline
    \end{tabular}
    \end{center}
    \label{tab:spin_dpp}
%\end{table}

%\begin{table}
    \begin{center}
    \caption{JPFによるDining Philosophers Problemの検証の計測結果}
    \begin{tabular}{|r|r|} \hline
	プロセス数 & 実行時間(秒) \\ \hline
	5 & 3.98 \\ \hline
	6 & 7.33 \\ \hline
	7 & 26.29 \\ \hline
	8 & 123.16 \\ \hline
    \end{tabular}
    \end{center}
    \label{tab:jpf_dpp}
\end{table}


\newpage
\subsection{状態数と探索時間に関する考察}

SPINによる結果は、
CbCでの検証と比べて、状態数が少ない。
生成される状態数が少ないことが探索時間の短さにつながっていると考えられる。

PROMELAの記述では、Philosopher 内部での状態遷移記述は、\verb+do/od+
の中に閉じ込められており、\verb+atomic+の内部は複数の状態に分割されない。
また、変数は{\tt fork}の配列のみなのでメモリの量的にも少なくなっている。
SPINでは PROMELAをCに変換して探索を行うので、探索自体がコンパイル
されて実行するようになっており高速である。

CbCの場合は、実際に実行可能なプログラムであり、プログラムで渡される
引数全体と大域変数全体がメモリの量となる。CbC では、
継続を表すコードセグメントへのポインタが状態を表す。CbC での記述では、
Philosopher の状態は8つあるので、状態数自体も指数関数的に多くなっている。

JPFは、Javaのスレッドを使った記述を使っており、Interleaving はJavaの
バイトコード単位で起きる。もちろん、完全なバイトコード単位のInterleaving
を調べているわけではなく、複数のスレッドが相互に干渉する場合の
組合せを調べることになる。

Java による記述ではプログラム中のオブジェクトのインスタンス変数
全体がメモリの量となる。状態は実行しているバイトコードのアドレス
によって表される。さらに、{\tt synchronized} などの記述には、
それに対応したロックがあり、それを実現するためのメモリ領域が必要である。

JPFの探索時間が、プロセス数が6個まではCbCの探索時間よりも遅く、
プロセス数が7個以上になるとCbCより速いのは、
CbCの実装によるものだと推測される。
CbCの実装では、メモリのBinary Treeをバランスさせていないため、
探索時間が長くなっていると考えられる。
%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による検証は、実際のプログラムをバイトコードレベルで実行する
ので、より正確な検証が可能である。しかし、そのために状態数
は多くなり、バイトコードシミュレータのオーバヘッドもあって、
検証に要する時間とメモリが大きくなってしまっている。

JPFはバイトコードによるシミュレーションであり、SPINはPROMELA を
コンパイルしたCのコードによるシミュレータにより検証を行っている。
CbC は、他の二つと異なり、コードセグメント部分は直接実行
される。この部分にエラーが入ることはないのがCbCによる
検証の利点であると言える。

[検証する性質の記述]

検証するときには、検証する性質を記述する必要がある。
SPINでは、LTLをPROMLEAに変換するプログラムがあり、
LTLにより、性質を記述する。しかし、これにより
状態数自体は増えるが、変換したPROMELAの記述は
Cのコンパイルされるので比較的高速にチェックすることが
可能である。
また、PROMELA中に
assert を使って式の検証をすることも出来る。

JPFでは、もっぱらassertを使った性質の記述を用いる。
時相論理的な記述は自分で、それをチェックするプログラム
をスレッドで記述する必要がある。

CbCでは、性質の記述はCbCそのもので行う。本論文で示したように
タブロー展開と同時に(限られた)時相論理で記述された性質を
ほとんどオーバヘッドなくチェックすることが出来る。
これは時相論理式のチェック自体がCbCプログラムとして
コンパイルされているからである。
これは検証系自体が、検証される言語と同じ言語で記述されている
ことの利点である。タブロー展開を行う{\tt goto文}
を適切に選択することにより、同期の抽象度を選択できることも
利点であると言える。

JPFでは一見同じ言語で検証系を記述しているように見えるが、
実際の検証対象はJava バイトコードであり、実装はインタプリタ
的にならざるを得ない。つまり、JPFでは、検証の抽象度を
上げて、状態数を少なくすると言うことが出来ない。


%%%end%%%