\chapter{評価}
\label{chapter4}

実装した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〜7個の場合の結果は表\ref{tab:dpp_tableau}のようになった。

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

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

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

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

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

\begin{table}
    \centering
    \begin{tabular}{|r|r|r|} \hline
	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
	5 & 38,984 & 0.83 \\ \hline
	6 & 159,299 & 4.41 \\ \hline
    \end{tabular}
    \caption{Dining Philosophers Problemにデッドロック検知を組み込んだ実行結果}
    \label{tab:ltl_tableau}
\end{table}

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

また、プロセスが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}


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

\begin{table}
    \centering
    \begin{tabular}{|r|r|r|} \hline
	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
	5 & 94 & 0.008 \\ \hline
	6 & 212 & 0.01 \\ \hline
    \end{tabular}
    \caption{SPINによるDining Philosophers Problemの検証結果}
    \label{tab:spin_dpp}
\end{table}

CbCでの検証と比べて、状態数が少ない。
そのため、実行にかかる時間も高速であった。
これは、PROMELAでのDining Philosophers Problemを抽象化して記述しているため
状態数が少ない。

CbCの場合は、実際に実行可能なプログラムを逐次実行していくことで状態を変化
させているため、モデル化した記述よりも状態数が多くなっていると考えられる。

また、プロセスが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が用意されているのでこれを用いる。

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

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

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

JPFもCbCと同様に実際に実行可能なバイトコードに対して検証が可能である。
プロセス数に対する実行時間を比較するとCbCの方が速い。


%%%end%%%