\chapter{Continuation based C と検証}
\label{chapter2}
ここでは、CbCの概要を解説し、CbCプログラムの検証に必要となるタブロー法および、
線形時相論理について述べる。
また、検証に関連して他の検証ツールの概要を説明する。

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

\subsection{CbC の要求仕様}
オブジェクト指向技術と、それに基づくJava、C++などの言語が注目されている。
これらの言語は、動的な適合性を中心に設計されたものである。
そのため、C言語などの低レベルな言語による記述に比べて、
余分な条件判断(メソッドサーチ、メタレベルでの実行)を増やしてしまい、
コンパクトで高速な応答を要求されるリアルタイム処理や組み込み用途には適さない。

ハードウェアに一番近い言語はアセンブラである。
マクロアセンブラなどの記述はあまりにも低レベルであり、長年進歩していない。
また、使用可能なゲート数が増えるにつれ、RISC的な対称性の高い少数の命令よりも、
複雑な命令を持つCISC的なCPUが増えてきている。
そのために既存の言語に対するコンパイラを一々設計し直すことが必要になっている。

また、VHDL、Verilogなどのハードウェア記述言語は有限状態遷移の中に閉じており、
オブジェクト指向などの抽象化とは全く別なものとなっている。

コンパイラの自動生成などが重要な研究テーマとなると考えられるが、
ハードウェア記述言語、アセンブラ、プログラミング言語の３つの言語は、
全く異なる方向を向いており、独立しているため、
その研究は困難なものとなると考えられている。

そこで、CbCはこの３つのギャップを埋めるべく次にあげる要求仕様に従って設計された。
\begin{itemize}
    \item ハードウェアとスタックマシンの中間言語

	インタプリタ記述やコンパイラターゲットとして優れていること。
	アーキテクチャ依存性が少ないこと。また、アーキテクチャ依存性をモデル化できること。

    \item C言語よりも下位の言語

	アセンブラよりも汎用性と記述性に優れ、C言語と互換性があること。
	CをCbCにコンパイルでき、ハンドコンパイルの結果を同値なコードに変換できる。

    \item 明確な実行モデル

	C++やPrologのような複雑な実行モデルは好ましくなく、
	ハードウェアに実行順序の変更を許す範囲を広くする。

    \item 状態遷移を直接記述できる

	Yaccのような表駆動やCのような巨大なSwitch文ではなく、
	直接に状態遷移が実行できる。

    \item スレッドを実行モデルに内臓できる

	並列処理記述法ではなく、状態遷移として実現できる。

    \item クリティカルパスの最適化

	全体を散漫に最適化するコンパイルではなく、クリティカルパスを見つけ出して最適化できる。
\end{itemize}
これらの仕様は、ハードウェア記述とソフトウェア記述の両方を同時に行いつつ、
C言語よりも精密な実行記述を可能にするためのものである。また、CbCはプログラム変換や
コンパイラターゲットとして使うことを意識している。
CbCでは、状態遷移記述に適した言語を作ることを考え、スタックマシンを避けて
Continuation(継続)が導入されている。

\subsection{軽量継続(light-weight continuation)}
SchemeやC++、Java、Cは、大域脱出という形で継続を導入している。
これらの言語では、継続は必ず環境(入れ子になった局所変数を格納するスタック)のセーブを伴う。
CbCは関数呼び出しがないため、この環境は存在しない。
コード内部での局所変数は存在するが、それのネストは起こらない。
そのため、環境抜きの継続を使用することができる。これは、具体的には
引数付きの(直接/間接)goto命令である。これを軽量継続(light-weight continuation)と呼んでいる。

CbCはコードセグメントを引数付きgotoで接続することで継続を実現している。
コードセグメントとは、codeという型で定義される、関数に似たプログラム単位である。
原則として、このコードセグメントへの遷移は引数付きgotoによってのみ行われる。
また、コードセグメントからの脱出も引数付きgotoによってのみ行われる。
つまり、CbCのプログラムは、複数のコードセグメントが引数付きgotoで接続されたものになる
(図\ref{fig:code-goto})。

\begin{figure}[htbp]
    \begin{center}
	\includegraphics{figure/code-goto.pdf}
    \end{center}
    \caption{CbCプログラムの構成}
    \label{fig:code-goto}
\end{figure}

図\ref{fig:code-goto}のようにCbCプログラムの構成は、オートマトンと似た構造になることがわかる。
CbCのコードセグメントと引数付きgoto、ifはそれぞれオートマトンの状態と状態遷移および
遷移条件に対応しており、CbCは状態遷移記述に適しているといえる。

また、CbCのconcurrencyはコードセグメント単位であるため、
実装の方法により任意に細分化することができる。
concurrencyとはプログラムの並列実行性のことである。

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

CwCは現在までにIA32用、PowerPC用、MIPS用、ARM用のコンパイラが実装されている。

\section{タブロー法によるプログラムの状態の展開}
タブロー法は、様相論理式の恒真性を検証する定理証明アルゴリズムで、
木構造に基づく反駁手法である。タブロー法によって状態を展開することをタブロー展開という。

ここでは、タブロー展開は、仕様とプログラムの大域的な状態をすべて生成する手法である。
反例を探す場合は反例が見つかった場合に生成を停止して良いが、証明を行う場合は
すべての大域的な状態を生成する必要がある。大域的な状態の生成は、初期状態から非決定的に
生成されるすべての次の状態を生成することにより行われる。これを状態の展開という。
証明には、プログラムの状態の数に比例し、また、プログラムが含む変数の数の指数乗の計算量がかかる。


この展開の際に、仕様も同時に展開することでプログラムに対する仕様の検証を行うことが可能である。

\section{ソフトウェアの検証}
現在、様々なものにソフトウェアが組み込まれているが、
これらの中にはバグを含むものが少なくないのが現状である。
バグとは、ソフトウェアが期待された動きと別な動きをすることである。
また、その「期待された動き」を規定したものを仕様と呼び、
自然言語または論理で記述される。

ソフトウェアのバグを減らし信頼性を高めるために、テストや検証を行う必要がある。

テストとは、限定された条件でプログラムを実行し、
正しく動作するかどうかを確認する作業のことである。
通常、すべての条件で動作を確認するのは難しいため、
重要な部分のみテストを行うことが多い。
そのため、テストでは誤りが存在することを示すことはできるが、
誤りが存在しないことは証明できない。

検証とは、ソフトウェアが仕様を満たすことを数学的、論理的に確かめることである。
ソフトウェア検証には、大きく分類してモデル検査と定理証明がある。
モデル検査では、有限状態モデルを網羅的に探索して、デッドロックや飢餓状態などの
望ましくない状態を自動的に検出することができる。
しかし、無限の状態を持つものや有限でも多くの状態を持つものは取り扱うことが困難である。
一方、定理証明では、定理や推論規則を用いて検証を行うため、
そのような状態を持つものでも取り扱うことが可能であるが、対話的な推論が必要になる。

\section{並列プログラムにおける検証}
並列プログラムにおいて、個々のプログラムが正しく動作することが証明されても、
それらを並列に実行したとき、その全体の動作の正しさは証明されない。
これは並列プログラムの非決定性によるものである。

プログラムにおいて非決定性な要素として入力と並列実行があげられる。
単体のプログラム自体は仕様が決まっており、決定性であるといえる。
しかし、複数のプログラムを並列に実行する場合、その全体の動作は非決定性となる
(図\ref{fig:parallel_exec})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics{figure/parallel_exec}
    \end{center}
    \caption{並列実行の非決定性}
    \label{fig:parallel_exec}
\end{figure}

並列プログラムの検証手順として、並列実行するプログラムの可能な実行すべてを
データ構造として構築し、そのデータ構造に対して仕様を検証する。

例えば、C、VHDL、Javaなどで記述された複数のプログラムを並列実行する場合を考える。
まず、それぞれのプログラムをCbCで書き換える。そして、それらのCbCプログラムを
並列実行するためにスケジューラを組み込み、制御する。
それによって作成された並列実行可能なプログラム全体は
一つのCbCプログラムとみなすことができる。
その並列実行を検証するために、プログラムの状態をデータ構造として構築する必要がある。
そこで、CbCプログラムに対してタブロー展開を行う。そして、タブロー展開によって生成されたデータ構造に対して仕様を検証する(図\ref{fig:verification_procedure})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.4]{figure/verification_procedure.pdf}
    \end{center}
    \caption{並列プログラムの検証手順}
    \label{fig:verification_procedure}
\end{figure}


\section{線形時相論理による検証}
本研究では、時相論理の一つである線形時相論理(Linear-time Temporal Logic、LTL)を用いる。
時相論理とは、時間を様相として持つ様相論理である。
時相論理は、システムのハードウェアやソフトウェアの仕様を記述する方法として、
形式的検証で利用される。
様相論理とは、必然性や可能性などの様相概念を取り扱う論理である。

時相論理は、時間との関連で命題を理解し表現するための表記法と規則の体系である。
計算機科学においては、状態の遷移や時間の経過の観点より
システムの性質を記述するのに用いられる。
%線形時相論理とは、時間に関する様相を持つ様相時相論理の一つである。
%様相時相論理とは、時間との関連で命題を理解し表現するための表記法と規則の体系である。
%また、状態の遷移や時間の経過の観点よりシステムの性質を記述する論理体系である。

LTLは、未来を記述することを可能にする時相論理で、
状態遷移システムの単一の経路に関する性質を記述することが可能である。

LTLの演算には通常の論理演算に加えて、時間に関する単項演算がある(表\ref{tab:LTL})。

\begin{table}
    \centering
    \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}
    \caption{線形時相論理の単項演算}
    \label{tab:LTL}
\end{table}

LTLで表現できる重要な特性には次の２つがある。
\begin{itemize}
    \item □¬p：安全性特性
    \item ◇p：活性特性
\end{itemize}
安全性特性とは、有限な期間での反例を無限の時系列に拡張しても反例であるような状態のことである。
活性特性とは、有限な期間での反例を無限の時系列に拡張したとき、それが反例でなくなる状態である。
つまり、安全性特性はあるシステムにおいて「何か悪いことが決して起こらない」ことを意味する。
また、活性特性は「何か良いことがいずれ起きる」ことを意味する。
これらの表現を用いてシステムの要求仕様を記述することで、
形式的検証を行うことが可能である。

\section{他の検証ツール}
他の検証ツールとしてSPINとJava PathFinderがあげられる。
この２つのツールの概要を説明する。

\subsection{SPINの概要}
有限状態遷移系に対する形式的検査手法としてモデル検査手法がある。
その代表的なツールとしてSPIN\cite{bib:spin}がある。

SPINは、プログラム変換的な手法で検証するツールで、
検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、
それを基にC言語で記述された検証器を生成するものである。
チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。

SPINは、PROMELAによる記述を入力として網羅的に状態を探索し、その性質を検査する。
また、SPINはPROMELAによる記述をシミュレーション実行することもできる。
SPINによるモデル検査は、検査すべき対象のモデルをPROMELAで記述し、
それを基にPAN(Protocol ANnalyzer)という、状態を網羅的に探索する実行形式を
自動生成し、それにより様々な性質の検査を行う。

SPINでは以下の性質を検査することができる。
\begin{itemize}
    \item アサーション
    \item 到達性
    \item 進行性
    \item LTL式で記述された仕様
\end{itemize}

SPINはオートマトンの並列実行が可能であるが、これは厳密には実行するステートメントを
ランダムに選択し、実行することで実現している。以下にPROMELAの記述例を示す。

\begin{lstlisting}[caption=PROMELAの記述例,label=src:PROMELA]
byte state = 1;

proctype A()
{
  byte tmp;
  (state == 1) -> tmp=state; tmp=temp+1; state=tmp
}

proctype B()
{
  byte tmp;
  (state == 1) -> tmp=state; tmp=temp-1; state=tmp
}

init
{
  run A(); run B()
}
\end{lstlisting}

このプログラムではプロセスAとBが定義されている。
PROMELAでは、``;''で区切られたステートメントが並列に実行される。
このプログラムでは、プロセスAとBが並列に実行される。
並列に実行されるとなっているが、全く同時に実行されるわけではなく、
ランダムに各プロセスが選ばれて実行されている。
また、SPINのconcurrencyはステートメント単位となっている。

\subsection{Java PathFinderの概要}
Javaプログラムに対するモデル検査ツールであるJava PathFinder(JPF)\cite{bib:jpf}
について説明する。
JPFはNASAで開発され、現在はsourceforge.net上で開発が続けられている。

最初の実装では、JavaをPromelaに変換していたが、
現在は、Javaバーチャルマシン(JVM)を直接シミュレーションして実行している。
そのため、Javaのバイトコードを直接実行可能である。


JPFは、実行可能なJavaのバイトコードを検証するためのシステムである。
バイトコードを状態遷移モデルとして扱い、
実行時に遷移し得る状態を網羅的に検査することにより、デッドロックを検知したり、
キャッチされていない例外(NullPointerExceptionやAssertionErrorなど)を
検出することができる。

また、JPFはバイトコードの実行パターンを網羅的に調べるため、膨大なCPU時間を必要とする。


JPFでできることを以下に示す。
\begin{itemize}
    \item スレッドの可能な実行すべてを調べる
    \item デッドロックの検出
    \item アサーション
    \item Partial Order Reduction
\end{itemize}

Partial Order Reductionとは、モデル検査アルゴリズムで探索される
状態空間のサイズを減らすための手法である。


また、JPFはJVMベースであるため、複数のプロセスの取扱いができない。
他にも、実用規模のプログラムは一般的に状態空間が巨大であるため、
直接実行することはできない。

JPFは、大きなプログラムには使えないため、一部を抜き出して、
それに対してデバッグをするのに使用される。
他にも、Javaを仕様記述言語としてプロトコルの検証などに用いられる。

JPFのconcurrencyはスレッド単位である。


%%%end%%%