--- a/resume/master_resume.tex	Wed Feb 20 03:18:06 2008 +0900
+++ b/resume/master_resume.tex	Wed Feb 20 05:53:14 2008 +0900
@@ -25,7 +25,6 @@
 そこで、本研究では、Continuation based C(CbC)言語による実装と
 その実装に対する検証手法を提案している。
 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
-そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
 また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。
 
 本研究は、CbCプログラムが状態遷移記述になることに着目し、
@@ -34,6 +33,130 @@
 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用さ
 れる。
 
+\section{Continuation based Cの概要}
+CbC は、C言語を制限したもので、機械依存性の無いアセンブラのような構成になっており、
+C言語からループ制御構造と、サブルーチン・コールを取り除き、継続を導入した言語である。
+この言語は、C言語に継続専用のプログラム単位であるコード(code)と、
+継続(goto)を導入した構成となっている。
+継続とは、次に実行すべきコードを直接または間接的に指定する手法である。
+CbC は、サブルーチンよりも小さいプログラム単位であるコードを導入しているため、
+C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
+
+CbCはコードセグメントを引数付きgoto文で接続することで継続を実現している。
+コードセグメントとは、codeという型で定義されるプログラム単位である。
+原則として、このコードセグメントへの遷移は引数付きgoto文によってのみ行われる。
+また、コードセグメントからの脱出も引数付きgoto文によってのみ行われる。
+つまり、CbCプログラムは、複数のコードセグメントが引数付きgoto文で接続された構造になる。
+
+CbCのコードセグメントと引数付きgoto文、ifはそれぞれオートマトンの状態と状態遷移および
+遷移条件に対応しており、CbCプログラムは状態遷移記述であると言える。
+また、CbCにおける並列動作はコードセグメント単位となる。
+
+CbCはC言語の下位言語であるが、C言語のサブルーチンへ戻るための環境付き継続を
+導入することでC言語の上位言語となる。この言語をCwC(C with Continuation)と呼ぶ。
+CwCでは、CbCから通常のC言語の関数を呼び出すことができる。
+
+\section{他の検証ツール}
+有限状態遷移系に対する形式的検査手法としてモデル検査手法がある。
+その代表的なツールとしてSPINとJava PathFinder(JPF)があげられる。
+
+SPINは、プログラム変換的な手法で検証するツールで、
+検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、
+それを基にC言語で記述された検証器を生成するものである。
+チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。
+SPINでは、アサーション、デッドロック、到達性、進行制、LTL式の
+性質について検査することができる。
+また、SPINの並列動作はステートメント単位となる。
+
+JPFは、実行可能なJavaのバイトコードを検証するためのシステムである。
+バイトコードを状態遷移モデルとして扱い、
+実行時に遷移し得る状態を網羅的に検査することにより、デッドロックを検知したり、
+キャッチされていない例外(NullPointerExceptionやAssertionErrorなど)を
+検出することができる。
+JPFで検査できる性質として、アサーション、デッドロック、キャッチされていない例外
+があげられる。
+
+また、JPFはJVMベースであるため、複数のプロセスの取扱いができない。
+他にも、実用規模のプログラムは一般的に状態空間が巨大であるため、
+直接実行することはできない。
+そのため、プログラムの一部を抜き出して、
+それに対してデバッグをするのに使用される。
+他にも、Javaを仕様記述言語としてプロトコルの検証などに用いられる。
+JPFの並列動作はスレッド単位となる。
+\section{実装}
+検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
+これは資源共有問題の一つで、次のような内容である。
+5人の哲学者が円卓についており、それぞれ思索と食事を交互に繰り返す。
+円卓には5本のフォークが置かれており、哲学者は左右のフォーク2本を使って食事をする。
+フォークが取れない場合はフォークが空くのを待つ。
+この問題では、すべての哲学者が一斉に左手でフォークを取るとデッドロックが起きる。
+例として、左手でフォークを取るコードセグメントを示す。
+{\footnotesize
+\begin{verbatim}
+code pickup_lfork(PhilsPtr self)
+{
+  if (self->left_fork->owner ==  NULL) {
+    self->left_fork->owner = self;
+    goto pickup_rfork(self);
+  } else {
+    goto pickup_lfork(self);
+  }
+}
+\end{verbatim}
+}
+codeがコードセグメントの定義であり、
+コードセグメントの引数部分をインターフェースと呼ぶ。
+このコードセグメントは左手でフォークが取れた場合は、
+右手でフォークを取るコードセグメントへ遷移する。
+取れなかった場合は、またこのコードセグメントへ遷移する。
+
+次に、タブロー法による状態の展開の実装について説明する。
+タブロー法による状態の展開をタブロー展開と呼ぶ。
+
+CbCプログラムのタブロー展開の特徴として、
+プログラムの可能な実行の組み合わせすべてを調べる、
+プログラムの状態を展開するために状態の探索をDepth First Search(DFS)で行う、
+プログラムの実行によって生成される状態は木構造で記録する、
+同じ状態はすべて共有することでメモリ消費を減らす、
+があげられる。
+
+まず、最初に状態として扱うすべての変数をBinary Tree構造で記録する。
+そして、検証対象のプログラムのコードセグメントを実行して、
+実行に伴う状態の変化をBinary Tree構造で記録していく。
+このBinary Treeを状態データベースと呼ぶ。
+すべての可能な実行の組み合わせを実行しながらそのときの状態を
+状態データベースに登録していくことで状態を展開する。
+
+以下にタブロー展開を行うためのタブローコードセグメントを示す。
+{\footnotesize
+\begin{verbatim}
+code tableau(TaskPtr list)
+{
+  StateDB out;
+  if (lookup_StateDB(&st, &state_db, &out)) {
+    while(!(list=next_task_iterator(task_iter))) {
+      TaskIteratorPtr prev_iter=task_iter->prev;
+      if (!prev_iter) {
+        memory_usage();
+        goto ret(0),env;
+      }
+      free_task_iterator(task_iter);
+      task_iter=prev_iter;
+    }
+    restore_memory(task_iter->state->memory);
+  } else {
+    task_iter=create_task_iterator(list,out,task_iter);
+  }
+  goto list->phils->next(list->phils,list);
+}
+\end{verbatim}
+}
+検証対象プログラムのコードセグメントはこのtableauコードセグメントに遷移するようにする。
+\verb|lookup_StateDB()|関数で状態データベースからコードセグメントの実行によって
+得られた状態を検索・登録していく。登録する際にそのまま登録するのではなく、
+変数を記録したBinary Treeをコピーして登録していく。この際、同じ内容の変数が
+あった場合は、同じ領域を指すことで状態を共有するようにする。
+
 {\small
 \begin{thebibliography}{9}
     \bibitem{bib:jssst2000kono}