Mercurial > hg > Papers > 2008 > atsuki-master
changeset 6:1bf023e03779
*** empty log message ***
| author | atsuki |
|---|---|
| date | Thu, 14 Feb 2008 15:43:13 +0900 |
| parents | db0d95f0b2e0 |
| children | 8de3a0461beb |
| files | paper/chapter3.tex paper/chapter4.tex paper/figure/mem_pat_structure.bb paper/figure/mem_pat_structure.pdf |
| diffstat | 4 files changed, 76 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- 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} + 新たに追加される変数がメモリパターンに既に登録されている場合、 その変数は登録されない。 - +\\ メモリパターンは変数の集合である。 コードセグメントを実行することでいくつかの変数が変化した場合、
--- 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での検証は、実際に動作するプログラムに対して行うことができる。 +