\documentclass[twocolumn, a4j, twoside]{jarticle}
\usepackage{master_proc}
\usepackage[dvips]{graphicx}

% dvipdfm を使って PDF ファイルに日本語の栞をつける
% \usepackage[dvipdfm]{color}
% \usepackage[dvipdfm,bookmarks=true,bookmarksnumbered=true,%
% bookmarkstype=toc]{hyperref}

\jtitle{線形時相論理によるContinuation based Cプログラムの検証}		%和文タイトル
\etitle{Verification of Continuation based C Program using Linear-time Temporal Logic}	%英文タイトル
\author{下地 篤樹}	%著者名
\studentid{068507B}	%学籍番号
\teacher{河野 真治}	%指導教官

\begin{document}
\maketitle
\section{はじめに}
リアルタイムプログラムや並列プログラムのような非決定性を含むプログラムは、
逐次型のプログラムに有効な二分法などによるデバッグ手法ではデバッグすることが
困難である。
そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
確立が重要な課題となっている。

そこで、本研究では、Continuation based C(CbC)言語による実装と
その実装に対する検証手法を提案している。
また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。

本研究は、CbCプログラムが状態遷移記述になることに着目し、
状態遷移記述に対して有効であるタブロー法による状態の展開を行い、
状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。

\vspace{-2mm}
\section{Continuation based Cの概要}
CbC は、C言語を制限したもので、
Cからループ制御構造と、サブルーチン・コールを取り除き、継続を導入した言語である。
この言語は、Cに継続専用のプログラム単位であるコード(code)と、
継続(goto)を導入した構成となっている。
継続とは、次に実行すべきコードを直接または間接的に指定する手法である。
CbC は、サブルーチンよりも小さいプログラム単位であるcodeを導入しているため、
C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。

CbCはコードセグメントを引数付きgoto文で接続することで継続を実現している。
コードセグメントとは、codeという型で定義されるプログラム単位である。
このコードセグメントへの遷移は引数付きgoto文によってのみ行われる。
また、コードセグメントからの脱出も引数付きgoto文によってのみ行われる。

また、ここでは、CbCにおける並列度はコードセグメント単位を使用する。

CbCにCのサブルーチンへ戻るための環境付き継続を
導入することでCの上位言語となる。この言語をCwC(C with Continuation)と呼ぶ。
CwCでは、CbCから通常のC言語の関数を呼び出すことができる。

\vspace{-2mm}
\section{線形時相論理の概要}
線形時相論理(Linear-time Temporal Logic、LTL)は、
時間を様相として持つ様相論理の一つで、
状態遷移システムの単一の経路に関する性質を記述することが可能である。
表\ref{tab:LTL}にLTLの単項演算子を示す。
\begin{table}
{\footnotesize
    \begin{center}
    \begin{tabular}{|l|c|l|} \hline
	\multicolumn{1}{|c|}{名称} & 記号表記 & \multicolumn{1}{|c|}{意味} \\ \hline
	Always & □p & pは今後常に真である \\ \hline
	Sometime & ◇p & pは将来のいずれかの時点で真である\\ \hline
	Next & ○p & pは次の時点で真である \\ \hline
    \end{tabular}
\vspace{-2mm}
    \caption{線形時相論理の単項演算}
    \label{tab:LTL}
    \end{center}
}
\vspace{-8mm}
\end{table}
検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用さ
れる。

\vspace{-2mm}
\section{他のモデル検査ツール}
他のモデル検査ツールとしてSPINとJava PathFinder(JPF)がある。

SPIN\cite{bib:spin}は、プログラム変換的な手法で検証するツールで、
検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、
それを基にC言語で記述された検証器を生成するものである。
チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。
SPINでは、アサーション、デッドロック、到達性、進行制、LTL式の
性質について検査することができる。
また、SPINの並列動作はステートメント単位となる。

JPF\cite{bib:jpf}は、実行可能なJavaのバイトコードを検証するためのシステムである。
バイトコードを状態遷移モデルとして扱い、
実行時に遷移し得る状態を網羅的に検査することにより、デッドロックを検知したり、
キャッチされていない例外を検出することができる。
JPFで検査できる性質として、アサーション、デッドロック、キャッチされていない例外
があげられる。
また、JPFの並列動作はスレッド単位となる。
\vspace{-2mm}

\section{実装}
検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
これは資源共有問題の一つで、次のような内容である。
5人の哲学者が円卓についており、それぞれ思索と食事を交互に繰り返す。
円卓には5本のフォークが置かれており、哲学者は左右のフォーク2本を使って食事をする。
フォークが取れない場合はフォークが空くのを待つ。
この問題では、すべての哲学者が一斉に左手でフォークを取るとデッドロックが起きる。
例として、左手でフォークを取るコードセグメントを示す。

\vspace{-3mm}
{\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}
}
\vspace{-4mm}

codeがコードセグメントの定義であり、
コードセグメントの引数部分をインターフェースと呼ぶ。
このコードセグメントは左手でフォークが取れた場合は、
右手でフォークを取るコードセグメントへ遷移する。
取れなかった場合は、またこのコードセグメントへ遷移する。

次に、タブロー法による状態の展開の実装について説明する。

CbCプログラムのタブロー法による状態の展開の特徴として、
プログラムの可能な実行の組み合わせすべてを調べる、
プログラムの状態を展開するために状態の探索をDepth First Searchで行う、
プログラムの実行によって生成される状態は木構造で記録する、
同じ状態はすべて共有することでメモリ消費を減らすということ
があげられる。

まず、最初に状態として扱うすべてのメモリをBinary Tree構造で記録する。
そして、検証対象のプログラムのコードセグメントを実行して、
実行に伴う状態の変化をBinary Tree構造で記録していく。
このBinary Treeを状態データベースと呼ぶ。
すべての可能な実行の組み合わせを実行しながらそのときの状態を
状態データベースに登録していく。

以下にタブロー展開を行うためのtableauコードセグメントを示す。
このコードセグメントはCwCで記述している。

\vspace{-3mm}
{\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}
}
\vspace{-3mm}

検証対象プログラムのコードセグメントはこのtableauコードセグメントに遷移するようにする。
\verb|lookup_StateDB()|関数で状態データベースからコードセグメントの実行によって
得られた状態を検索・登録していく。登録する際にそのまま登録するのではなく、
メモリを記録したBinary Treeをコピーして登録していく。この際、同じメモリ内容が
あった場合は、同じ領域を指すことで状態を共有するようにする。
このtableauコードセグメントによりDFSで状態を探索していく。

また、タブロー展開を行う際に、
LTL式より生成されたコードセグメントを実行することで検証を行う。
検証対象プログラムからtableauコードセグメントに遷移する前に
生成された検証用コードセグメントを実行することで検証する。

ここでは、実装したDining Philosophers Problemに対して、デッドロックの検知を行う。
デッドロックとは、複数のプロセスが互いに相手の占有している資源の開放を待ってしまい、
結果としてプログラムが停止してしまうことである。
Dining Philosophers Problemにおいて、資源とはフォークのことである。
つまり、この場合のデッドロックはすべての哲学者(プロセス)が左手でフォークを持ち、
右手のフォークが空くのを待っている状態である。

デッドロックが起きる条件である、「哲学者が一斉に左手でフォークを取る」を
すべての状態で検査することでプログラムのデッドロックを検知する。

\vspace{-2mm}
\section{評価および考察}
Dining Philosophers Problemの検証をCbC、SPIN、JPFで行った。
それぞれの結果を表\ref{tab:time}に示す。
\begin{table}[htbp]
\vspace{-2mm}
    {\footnotesize
    \begin{center}
    \begin{tabular}{|r|r|r|} \hline
	\multicolumn{3}{|c|}{\textbf{CbCによる検証}} \\ \hline
	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
	5 & 38,984 & 0.68 \\ \hline
	6 & 159,299 & 3.90 \\ \hline
	7 & 845,529 & 28.48 \\ \hline
	8 & 3,915,727 & 201.04 \\ \hline
	\multicolumn{3}{|c|}{\textbf{SPINによる検証}} \\ \hline
	5 & 94 & 0.008 \\ \hline
	6 & 212 & 0.01 \\ \hline
	7 & 494 & 0.03 \\ \hline
	8 & 1,172 & 0.04 \\ \hline
	\multicolumn{3}{|c|}{\textbf{JPFによる検証}} \\ \hline
	5 & 不明 & 3.98 \\ \hline
	6 & 不明 & 7.33 \\ \hline
	7 & 不明 & 26.29 \\ \hline
	8 & 不明 & 123.16 \\ \hline
    \end{tabular}
\vspace{-3mm}
    \caption{検証の計測結果}
    \label{tab:time}
    \end{center}
    }
\vspace{-7mm}
\end{table}
CbCの検証では、実際に実行可能なプログラムであり、プログラムで渡される引数全体と
大域変数全体が状態となるため、プロセス数が増えるにつれて状態数も指数関数的に
多くなっている。

SPINによる結果は、CbCでの検証と比べて状態数が少ない。
生成される状態数が少ないことが探索時間の短さにつながっていると考えられる。

JPFの探索時間が、プロセス数6個まではCbCの探索時間よりも遅く、
7個以上になるとCbCより速いのは、CbCの実装によるものだと推測される。

CbCでの実装では、メモリのBinary Treeをバランスさせていないため、
状態数が増えるにつれて探索時間が長くなっていると考えられる。

\vspace{-2mm}
\section{まとめ}
Dining Philosophers ProblemをCbCで記述し、
LTL式より生成された検証用コードセグメントを同時にタブロー展開することで
検証を行い、他のモデル検査ツールと比較した。
CbCの方が遅いという結果になったが、実用には耐えられるレベルである。
また、メモリのTreeをバランスさせることで探索時間の短縮を行うことが課題である。

\vspace{-2mm}
{\small
\begin{thebibliography}{9}
    \bibitem{bib:jssst2000kono}
	河野真治. ``継続を持つCの下位言語によるシステム記述''.
	日本ソフトウェア科学会第17回大会, 2000.
    \bibitem{bib:sigos2007}
	下地篤樹, 河野真治. ``線形時相論理によるContinuation based Cプログラムの検証''.
	情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), April, 2007.
    \bibitem{bib:spin}
	``Spin - Formal Verification''.
	http://spinroot.com/spin/whatispin.html
    \bibitem{bib:jpf}
	``Java PathFinder''.
	http://javapathfinder.sourceforge.net/
\end{thebibliography}
}
\end{document}