Mercurial > hg > Papers > 2008 > atsuki-master

changeset 9:c2a35ce4546e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author atsuki
date Fri, 15 Feb 2008 17:17:15 +0900
parents 17d019b274a5
children a4babe6179a7
files paper/chapter3.tex paper/figure/change_mem_pat.bb paper/figure/change_mem_pat.pdf paper/figure/dfs1.bb paper/figure/dfs1.pdf paper/figure/mem_pat_entry.bb paper/figure/mem_pat_entry.pdf paper/figure/mem_pat_tree.bb paper/figure/mem_pat_tree.pdf paper/figure/mem_share.bb paper/figure/mem_share.pdf paper/figure/memoryBtree.bb paper/figure/memoryBtree.pdf paper/figure/memory_pattern.bb paper/figure/memory_pattern.pdf paper/figure/stateDB.bb paper/figure/stateDB.pdf paper/figure/state_db.bb paper/figure/state_db.pdf paper/figure/task_iterator.bb paper/figure/task_iterator.pdf
diffstat 21 files changed, 99 insertions(+), 95 deletions(-) [+]
line wrap: on
line diff
--- a/paper/chapter3.tex	Fri Feb 15 17:17:15 2008 +0900
+++ b/paper/chapter3.tex	Fri Feb 15 17:17:15 2008 +0900
@@ -192,38 +192,76 @@
 
 タブロー展開器の具体的な実装について説明する。
 
-まず、始めに状態として扱う変数をすべて登録する。
-変数はBinary Tree構造で記録する(図\ref{fig:memory_pattern})。
-このBinary Treeをメモリパターンと呼ぶ。
+まず、始めに状態として扱うすべての変数のアドレスとそのレンジを
+Binary Tree構造で記録する(図\ref{fig:memoryBtree})。
+このBinary Treeをメモリツリーと呼ぶ。
+変数はメモリ領域に格納されており、メモリ領域のアドレスとそのレンジで指定される。
+新たに追加される変数がメモリツリーに既に登録されている場合、その変数は登録されない。
+
+\begin{figure}[htpb]
+    \begin{center}
+	\includegraphics[scale=.8]{figure/memoryBtree.pdf}
+    \end{center}
+    \caption{変数のアドレスとそのレンジのBinary Tree}
+    \label{fig:memoryBtree}
+\end{figure}
+
+
+すべての変数が登録されたら、次にそのメモリツリーのコピーを生成し、
+コピーを状態データベースに登録する。
+メモリツリーをコピーするとき、そのままコピーするのではなく、
+メモリのパターンに注目して同じパターンは共有されるようにコピーを生成する。
+このメモリツリーのコピーによって生成されるBinary Treeをメモリパターンツリーと呼ぶ。
+
+メモリのパターンとは、例えば変数Aと変数Bがメモリツリーに登録されているとして説明する。
+変数Aと変数Bはアドレスが違うのでメモリツリーには別々に登録されている。
+ここでもし、変数Aと変数Bの内容が両方とも0だった場合、
+アドレスは違っていてもメモリ領域の内容は同じになる(図\ref{fig:memory_pattern})。
+このメモリ領域の内容のことをメモリパターンと呼ぶ。
 
 \begin{figure}[htpb]
     \begin{center}
 	\includegraphics[scale=.8]{figure/memory_pattern.pdf}
     \end{center}
-    \caption{メモリパターンの例}
+    \caption{メモリパターン}
     \label{fig:memory_pattern}
 \end{figure}
 
-メモリパターンのノードは、メモリ領域のアドレスとそのサイズ、
-メモリ領域をコピーしたもののアドレス、メモリ領域のハッシュ値、
-左右の子ノードのポインタで構成されている(図\ref{fig:mem_pat_structure})。
-メモリ領域のアドレスは登録された変数のアドレスである。
+
+メモリパターンツリーの生成について説明する。
+
+メモリパターンツリーはメモリパターンとそのレンジを要素としたBinary Treeである。
+メモリツリーの要素をコピーし、それをメモリパターンツリーに登録していく。
+登録する際に、メモリパターンツリーに同じメモリパターンがないか検索する。
+もし、同じメモリパターンがあった場合、メモリツリーの要素をコピーせずに
+メモリパターンツリーの同じパターンの要素を指すようにする(図\ref{fig:mem_pat_tree})。
+つまり、同じ状態を共有するようにする。
+
+これにより使用するメモリ量を減らすことができる。
 
 \begin{figure}[htpb]
     \begin{center}
-	\includegraphics[scale=.8]{figure/mem_pat_structure.pdf}
+	\includegraphics[scale=.8]{figure/mem_pat_tree.pdf}
     \end{center}
-    \caption{メモリパターンのノードの構造とメモリ領域}
-    \label{fig:mem_pat_structure}
+    \caption{メモリパターンツリー}
+    \label{fig:mem_pat_tree}
 \end{figure}
 
-新たに追加される変数がメモリパターンに既に登録されている場合、
-その変数は登録されない。
-\\
+
+状態データベースとは、メモリパターンツリーとそのハッシュ値を
+要素として持つBinary Treeである(図\ref{fig:stateDB})。
 
-メモリパターンは変数の集合である。
-コードセグメントを実行することでいくつかの変数が変化した場合、
-メモリパターンも変化したことになる(図\ref{fig:change_mem_pat})。
+\begin{figure}[htpb]
+    \begin{center}
+	\includegraphics[scale=.8]{figure/stateDB.pdf}
+    \end{center}
+    \caption{状態データベース}
+    \label{fig:stateDB}
+\end{figure}
+
+
+コードセグメントを実行すると、メモリツリーに登録されている
+変数の内容(メモリパターン)が変化する場合がある(図\ref{fig:change_mem_pat})。
 
 \begin{figure}[htpb]
     \begin{center}
@@ -233,55 +271,13 @@
     \label{fig:change_mem_pat}
 \end{figure}
 
-変化したメモリパターンを新しいメモリパターンとしてBinary Tree構造で記録していく。
-このBinary Treeを状態データベースと呼ぶ。
-状態データベースのノード(状態ノード)は、メモリパターンのアドレスと
-そのメモリパターンのハッシュ値を保持する(図\ref{fig:state_db})。
-
-\begin{figure}[htpb]
-    \begin{center}
-	\includegraphics[scale=.9]{figure/state_db.pdf}
-    \end{center}
-    \caption{状態データベースの構成}
-    \label{fig:state_db}
-\end{figure}
-
-新たにメモリパターンを追加する場合、メモリパターンのハッシュ値をもとに
-状態データベースを検索する。もし、同じハッシュ値のメモリパターンが見つかった場合は
-そのメモリパターンは状態データベースに追加されない。
-見つからなかった場合、新たな状態ノードとして状態データベースに追加される。
-
-メモリパターンの追加方法は、変化したメモリパターンのコピーを生成して
-コピーの方を状態データベースに登録する。
-これは、もとのメモリパターンは次のコードセグメントを実行すると変化してしまうからである
-(図\ref{fig:mem_pat_entry})。
-
-\begin{figure}[htpb]
-    \begin{center}
-	\includegraphics[scale=.9]{figure/mem_pat_entry.pdf}
-    \end{center}
-    \caption{メモリパターンの状態データベースへの追加方法}
-    \label{fig:mem_pat_entry}
-\end{figure}
-
-
-しかし、コードセグメントを実行してもメモリパターンに登録されているすべての変数が
-変化するわけではない。変化するのは一部の変数のみである。
-したがって、メモリパターン全体をコピーし、
-状態データベースに登録するのはメモリ使用に関して無駄がある。
-
-そこで、変化があった変数のみをコピーし、残りの変化のなかった部分は前回の状態を
-そのまま使用するようにする。つまり、同じ状態を共有するようにする(図\ref{fig:mem_share})。
-これにより、メモリ使用量を減らすことができる。
-
-\begin{figure}[htpb]
-    \begin{center}
-	\includegraphics[scale=.9]{figure/mem_share.pdf}
-    \end{center}
-    \caption{同じ状態の共有}
-    \label{fig:mem_share}
-\end{figure}
-
+メモリパターンが変化したメモリツリーから新たにメモリパターンツリーを生成する。
+生成されたメモリパターンツリーを状態データベースに追加する場合、
+メモリパターンツリーのハッシュ値をもとに状態データベースを検索する。
+もし、同じハッシュ値のメモリパターンツリーが見つかった場合は
+そのメモリパターンツリーは状態データベースに追加されない。
+見つからなかった場合、状態データベースに追加される。
+\\
 
 
 次にDepth First Search(DFS)による状態の探索の実装について述べる。
@@ -313,7 +309,8 @@
 
 タスクリストからタスクを取り出す機構としてタスクイテレータを実装した。
 タスクイテレータはその時点のタスクリストと状態データベースおよび
-ひとつ前の時点のタスクイテレータを保持している(図\ref{fig:task_iterator})。
+ひとつ前の時点のタスクイテレータを保持している。
+また、タスクリストから次のタスクを取り出す機能を持っている(図\ref{fig:task_iterator})。
 
 \begin{figure}[htpb]
     \begin{center}
@@ -323,10 +320,11 @@
     \label{fig:task_iterator}
 \end{figure}
 
-まず、最初のメモリパターンを状態データベースに登録後、
+まず、最初のメモリパターンツリーをメモリツリーより生成し、状態データベースに登録する。
 タスクイテレータの処理によりタスクを取りだしコードセグメントを実行する。
-その実行によって、変化したメモリパターンを状態データベースからハッシュ値をもとに検索する。
-同じメモリパターンがなかった場合、状態データベースに追加する。
+その実行によって変化したメモリツリーよりメモリパターンツリーを生成し、
+それを状態データベースから検索する。
+同じメモリパターンツリーがなかった場合、状態データベースに追加する。
 その後、１段深く探索するために新たにタスクイテレータを生成し、
 その時点の状態データベースを登録する(図\ref{fig:dfs1})。
 
@@ -338,7 +336,7 @@
     \label{fig:dfs1}
 \end{figure}
 
-同じメモリパターンがあった場合は、その経路の探索を終了し、
+同じメモリパターンツリーがあった場合は、その経路の探索を終了し、
 タスクイテレータにより次のタスクを取りだしコードセグメントを実行する。
 
 タスクイテレータのタスクリストをすべて実行した場合、
@@ -392,7 +390,8 @@
 生成されたコードセグメントを実行することで検証を行う。
 
 \subsection{検証の実装}
-検証対象のプログラムからスケジューラに遷移した後、タブローコードセグメントに遷移する前に
+検証対象のプログラムからスケジューラに遷移した後、
+タブローコードセグメントに遷移する前に
 LTL式より生成された検証用コードセグメントを実行する。
 これにより、すべての状態において特定の性質を満たすことを調べることが可能である。
 
@@ -423,8 +422,8 @@
 \lstinputlisting[caption=検証用コードセグメント,label=src:check]
 {src/ltl.cbc}
 
-\verb|p()|関数は命題pに相当するものですべての哲学者(プロセス)が
-左手にフォークを持っているかを判定するものである。
+\verb|p()|関数は命題pに相当するもので、すべての哲学者(プロセス)が
+左手にフォークを持っているかどうかを判定するものである。
 checkコードセグメントがタブロー展開の際に実行されることで、
 すべての状態において命題pが決して起こらないかどうかを検査することができる。
 
--- a/paper/figure/change_mem_pat.bb	Fri Feb 15 17:17:15 2008 +0900
+++ b/paper/figure/change_mem_pat.bb	Fri Feb 15 17:17:15 2008 +0900
@@ -1,5 +1,5 @@
 %%Title: ./change_mem_pat.pdf
 %%Creator: ebb Version 0.5.2
-%%BoundingBox: 0 0 490 703
-%%CreationDate: Fri Feb  8 01:17:47 2008
+%%BoundingBox: 0 0 479 382
+%%CreationDate: Fri Feb 15 15:43:22 2008
 
Binary file paper/figure/change_mem_pat.pdf has changed
--- a/paper/figure/dfs1.bb	Fri Feb 15 17:17:15 2008 +0900
+++ b/paper/figure/dfs1.bb	Fri Feb 15 17:17:15 2008 +0900
@@ -1,5 +1,5 @@
 %%Title: ./dfs1.pdf
 %%Creator: ebb Version 0.5.2
-%%BoundingBox: 0 0 495 376
-%%CreationDate: Tue Feb 12 01:17:32 2008
+%%BoundingBox: 0 0 526 332
+%%CreationDate: Fri Feb 15 17:35:26 2008
 
Binary file paper/figure/dfs1.pdf has changed
--- a/paper/figure/mem_pat_entry.bb	Fri Feb 15 17:17:15 2008 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-%%Title: ./mem_pat_entry.pdf
-%%Creator: ebb Version 0.5.2
-%%BoundingBox: 0 0 537 320
-%%CreationDate: Fri Feb  8 04:17:33 2008
-
Binary file paper/figure/mem_pat_entry.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/figure/mem_pat_tree.bb	Fri Feb 15 17:17:15 2008 +0900
@@ -0,0 +1,5 @@
+%%Title: ./mem_pat_tree.pdf
+%%Creator: ebb Version 0.5.2
+%%BoundingBox: 0 0 466 429
+%%CreationDate: Fri Feb 15 14:05:10 2008
+
Binary file paper/figure/mem_pat_tree.pdf has changed
--- a/paper/figure/mem_share.bb	Fri Feb 15 17:17:15 2008 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-%%Title: ./mem_share.pdf
-%%Creator: ebb Version 0.5.2
-%%BoundingBox: 0 0 484 507
-%%CreationDate: Fri Feb  8 04:17:33 2008
-
Binary file paper/figure/mem_share.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/figure/memoryBtree.bb	Fri Feb 15 17:17:15 2008 +0900
@@ -0,0 +1,5 @@
+%%Title: ./memoryBtree.pdf
+%%Creator: ebb Version 0.5.2
+%%BoundingBox: 0 0 522 283
+%%CreationDate: Fri Feb 15 10:04:40 2008
+
Binary file paper/figure/memoryBtree.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/figure/memory_pattern.bb	Fri Feb 15 17:17:15 2008 +0900
@@ -0,0 +1,5 @@
+%%Title: ./memory_pattern.pdf
+%%Creator: ebb Version 0.5.2
+%%BoundingBox: 0 0 494 233
+%%CreationDate: Fri Feb 15 17:48:32 2008
+
Binary file paper/figure/memory_pattern.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/figure/stateDB.bb	Fri Feb 15 17:17:15 2008 +0900
@@ -0,0 +1,5 @@
+%%Title: ./stateDB.pdf
+%%Creator: ebb Version 0.5.2
+%%BoundingBox: 0 0 526 343
+%%CreationDate: Fri Feb 15 15:01:46 2008
+
Binary file paper/figure/stateDB.pdf has changed
--- a/paper/figure/state_db.bb	Fri Feb 15 17:17:15 2008 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-%%Title: ./state_db.pdf
-%%Creator: ebb Version 0.5.2
-%%BoundingBox: 0 0 436 304
-%%CreationDate: Fri Feb  8 01:59:03 2008
-
Binary file paper/figure/state_db.pdf has changed
--- a/paper/figure/task_iterator.bb	Fri Feb 15 17:17:15 2008 +0900
+++ b/paper/figure/task_iterator.bb	Fri Feb 15 17:17:15 2008 +0900
@@ -1,5 +1,5 @@
 %%Title: ./task_iterator.pdf
 %%Creator: ebb Version 0.5.2
-%%BoundingBox: 0 0 502 187
-%%CreationDate: Fri Feb  8 09:28:29 2008
+%%BoundingBox: 0 0 508 369
+%%CreationDate: Fri Feb 15 16:41:12 2008
 
Binary file paper/figure/task_iterator.pdf has changed