# HG changeset patch
# User atsuki
# Date 1202971393 -32400
# Node ID 1bf023e03779993de2434985c18bbfa1bf6f8af6
# Parent  db0d95f0b2e0c3f3223754d15f5ecf4130bbefe8
*** empty log message ***

diff -r db0d95f0b2e0 -r 1bf023e03779 paper/chapter3.tex
--- a/paper/chapter3.tex	Thu Feb 14 05:30:52 2008 +0900
+++ b/paper/chapter3.tex	Thu Feb 14 15:43:13 2008 +0900
@@ -170,7 +170,7 @@
 \subsection{タブロー展開器の実装}
 CbCプログラムの状態を自動的に展開するためのツールを作成した。
 これをタブロー展開器と呼ぶ。
-
+\\
 
 タブロー展開器は、スケジューラと同様にCbCプログラムに組み込み、
 複数プロセスを制御することで並列実行をシミュレーションすることができる。
@@ -188,7 +188,7 @@
 \end{figure}
 
 探索が終了すると、すべての状態が展開されたことになる。
-
+\\
 
 タブロー展開器の具体的な実装について説明する。
 
@@ -204,9 +204,22 @@
     \label{fig:memory_pattern}
 \end{figure}
 
+メモリパターンのノードは、メモリ領域のアドレスとそのサイズ、
+メモリ領域をコピーしたもののアドレス、メモリ領域のハッシュ値、
+左右の子ノードのポインタで構成されている(図\ref{fig:mem_pat_structure})。
+メモリ領域のアドレスは登録された変数のアドレスである。
+
+\begin{figure}[htpb]
+    \begin{center}
+	\includegraphics[scale=.8]{figure/mem_pat_structure.pdf}
+    \end{center}
+    \caption{メモリパターンのノードの構造とメモリ領域}
+    \label{fig:mem_pat_structure}
+\end{figure}
+
 新たに追加される変数がメモリパターンに既に登録されている場合、
 その変数は登録されない。
-
+\\
 
 メモリパターンは変数の集合である。
 コードセグメントを実行することでいくつかの変数が変化した場合、
diff -r db0d95f0b2e0 -r 1bf023e03779 paper/chapter4.tex
--- a/paper/chapter4.tex	Thu Feb 14 05:30:52 2008 +0900
+++ b/paper/chapter4.tex	Thu Feb 14 15:43:13 2008 +0900
@@ -1,30 +1,75 @@
-\chapter{評価および考察}
+\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に対してタブロー展開を適用した。
-プロセス(哲学者)が5〜7人の場合の結果は表\ref{tab:dpp_tableau}のようになった。
+プロセス(哲学者)が3〜7個の場合の結果は表\ref{tab:dpp_tableau}のようになった。
 
 \begin{table}
     \centering
     \begin{tabular}{|r|r|r|} \hline
-	プロセス数 & 状態数 & 時間(秒) \\ \hline
-	5 & 38,984 & 0.76 \\ \hline
-	6 & 159,299 & 4.21 \\ \hline
-	7 & 845,529 & 31.01 \\ \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}
 
-\section{他の検証ツールとの比較}
-SPINはモデル検査ツールであるため、検証対象をモデル化しそれをPROMELAで記述する必要がある。
+\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}
 
-CbCでの検証は、実際に動作するプログラムに対して行うことができる。
+
diff -r db0d95f0b2e0 -r 1bf023e03779 paper/figure/mem_pat_structure.bb
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/figure/mem_pat_structure.bb	Thu Feb 14 15:43:13 2008 +0900
@@ -0,0 +1,5 @@
+%%Title: ./mem_pat_structure.pdf
+%%Creator: ebb Version 0.5.2
+%%BoundingBox: 0 0 405 233
+%%CreationDate: Thu Feb 14 13:26:55 2008
+
diff -r db0d95f0b2e0 -r 1bf023e03779 paper/figure/mem_pat_structure.pdf
Binary file paper/figure/mem_pat_structure.pdf has changed