\chapter{線形時相論理によるCbCプログラムの検証手法}
\label{chapter3}

\section{CbCによる並列プログラミング}
ここでは、例題に用いるサンプルプログラムの概要と、
そのプログラムの状態の分割およびCbCプログラムとの対応について説明する。
また、並列プログラムのシミュレーション方法についても述べる。

\subsection{Dining Philosophers Problemの概要}
検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
これは資源共有問題の一つで、次のような内容である。

5人の哲学者が円卓についている。各々の哲学者にはスパゲッティーを持った皿が出されている。
スパゲッティーはとても絡まっているので、2本のフォークを使わないと食べられない。
お皿の間には1本のフォークが置いてあるので、
5人の哲学者に対して5本のフォークが用意されていることになる(図\ref{fig:dpp_image})。
哲学者は思索と食事を交互に繰り返している。
空腹を覚えると、左右のフォークを手に取ろうと試み、
2本のフォークを取ることに成功するとしばし食事をし、
しばらくするとフォークを置いて思索に戻る。
隣の哲学者が食事中でフォークが手に取れない場合は、
そのままフォークが空くのを待つ。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.5]{figure/dpp_image.pdf}
    \end{center}
    \caption{Dining Philosophers Problemのイメージ}
    \label{fig:dpp_image}
\end{figure}

各哲学者を一つのプロセスとすると、この問題では5個のプロセスが並列に動くことになる。
プロセスの並列実行はスケジューラによって制御することで実現する。

\subsection{状態の定義とコードセグメントとの対応}
Dining Philosophers ProblemをCbCで実装するにあたり、
プロセスを次のような8個の状態に分割した。
\begin{itemize}
    \item 思索
    \item フォークを持っていない場合の飢餓
    \item 左手にフォークを持つ
    \item 左手にフォークを持っている場合の飢餓
    \item 右手にフォークを持つ
    \item 食事
    \item 右手のフォークを置く
    \item 左手のフォークを置く
\end{itemize}

CbCではconcurrencyがコードセグメント単位であるため、
実装の方法により任意に細分化することができる。
今回は、状態数を8個とし、各状態に対応したコードセグメントを実装した。
以下にコードセグメントの例を示す。

\lstinputlisting[caption=「左手でフォークを持つ」コードセグメント,label=src:pickupL]
{src/pickupL.cbc}

ソースコード\ref{src:pickupL}はDining Philosophers Problemの
プログラムの一部である。
このコードセグメントは、「左手にフォークを持つ」状態に対応したものである。

処理の具体的な内容は、左手側のフォークがあればそのフォークを取り、
フォークを取ったプロセス(哲学者)のIDとフォークのIDを表示する。
その後、次の遷移先として「右手にフォークを持つ」状態である
pickup\_rforkコードセグメントをセットする。
もし、フォークがなければ次の遷移先として「フォークを持っていない場合の飢餓」状態である
hungry1コードセグメントをセットする。

各コードセグメントは、スケジューラに遷移するようにしている。
これは、複数のプロセスをスケジューラを用いて制御するためである。
状態遷移に必ずスケジューラを介すことで、
任意のプロセスのコードセグメントを実行することができる(図\ref{fig:scheduler})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.7]{figure/scheduler.pdf}
    \end{center}
    \caption{スケジューラによる複数プロセスの制御}
    \label{fig:scheduler}
\end{figure}

CbCプログラムはオートマトンと似た構造になっており、
コードセグメントと状態、引数付きgotoと状態遷移、
if制御文と遷移条件がそれぞれ対応している(表\ref{tab:automaton-cbc})。

\begin{table}
    \centering
    \begin{tabular}{|c|c|} \hline
	オートマトン & CbC \\ \hline
	状態 & コードセグメント \\
	状態遷移 & 引数付きgoto \\
	遷移条件 & if制御文 \\ \hline
    \end{tabular}
    \caption{オートマトンとCbCの対応}
    \label{tab:automaton-cbc}
\end{table}

コードセグメントと状態の対応に関しては、実際にはコードセグメントを抜けるときに状態が
確定する。

並列実行をシミュレーションするために必要なスケジューラについて説明する。
スケジューラは、最初にプロセスの生成と初期化を行い、それをタスクリストに登録する。
その後、各プロセスに対してラウンドロビンやランダムといった任意の方式で実行する。
ラウンドロビンとは、各プロセスを一定時間ずつ順番に実行することである。

並列実行のシミュレーションに関しては、SPINを参考に各プロセスをランダムに
実行することで実現する。

\section{CbCプログラムのタブロー展開}
CbCプログラムのタブロー展開の特徴を以下に示す。
\begin{itemize}
    \item プログラムの可能な実行の組み合わせすべてを調べる。
    \item 状態の探索はDepth First Searchで行う。
    \item プログラムの実行によって生成される状態は木構造で記録する。
    \item 同じ状態はすべて共有される。
\end{itemize}

\subsection{状態の展開}
提案する手法では、プログラムの可能な実行の組み合わせをすべて調べることができる。
CbCプログラムにおける可能な実行の組み合わせとは、
CbCプログラムをオートマトンとみなすと、オートマトンの遷移経路にあたる。

例としてDining Philosophers Problemのプロセス(哲学者)を
状態遷移図で示す(図\ref{fig:dpp_automaton})。
本研究では、CbCで実装するにあたり状態を8個に分割している。
ここで、それぞれの状態をABCDEFGHと定義する。

\begin{description}
    \item[A] 思索
    \item[B] 飢餓
    \item[C] 左手にフォークを持っている
    \item[D] 左手にフォークを持つ場合の飢餓
    \item[E] 両手にフォークを持っている
    \item[F] 食事
    \item[G] 右手のフォークを置いた
    \item[H] 左手のフォークを置いた
\end{description}

このオートマトンは「プロセスを終了する」という入力がないと、
例えば、$A\to B\to B\to B\to\cdots$というように探索が無限に続いてしまう場合がある。
そうなると、一つの遷移経路が無限に続くことになり、
このオートマトンが取り得るすべての遷移経路を調べることができない。
そこで、「ひとつの遷移経路で同じ状態が表れた場合はその経路の探索を終了する」
という条件を付加する。
これにより、先ほどの経路の探索は$A\to B$で終了することができる。

このようにして、遷移経路を図\ref{fig:dpp_automaton}から求めると、
\begin{itemize}
    \item $A\to B$
    \item $A\to B\to C\to D$
    \item $A\to B\to C\to D\to E\to F\to G\to H$
    \item $A\to B\to C\to E\to F\to G\to H$
\end{itemize}
という結果が得られる。
これが、Dining Philosophers Problemのプロセスの可能な実行の組み合わせとなる。


\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.75]{figure/dpp_automaton.pdf}
    \end{center}
    \caption{Dining Philosophers Problemの状態遷移図}
    \label{fig:dpp_automaton}
\end{figure}

例では単一のプロセスの場合を述べたが、実際には5個のプロセスを並列に実行することになる。
その場合、状態数は指数オーダーで増加する。
状態数が多い場合、特に並列プログラムに対する状態の展開を手作業で行うのは不可能に近い。

\newpage
\subsection{タブロー展開器の実装}
CbCプログラムの状態を自動的に展開するためのツールを作成した。
これをタブロー展開器と呼ぶ。
\\

タブロー展開器は、スケジューラと同様にCbCプログラムに組み込み、
複数プロセスを制御することで並列実行をシミュレーションすることができる。
また、タブロー展開器は、コードセグメントを一つずつ実行しながら状態を探索していく。
状態の探索はDFS(Depth First Search)で行う。
例えば、Dining Philosophers Problemの単一プロセスの状態探索木は
図\ref{fig:dpp_dfs}のようになる。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.8]{figure/dpp_dfs.pdf}
    \end{center}
    \caption{Dining Philosophers Problemの状態遷移図}
    \label{fig:dpp_dfs}
\end{figure}

探索が終了すると、すべての状態が展開されたことになる。
\\

タブロー展開器の具体的な実装について説明する。

まず、始めに状態として扱う変数をすべて登録する。
変数はBinary Tree構造で記録する(図\ref{fig:memory_pattern})。
このBinary Treeをメモリパターンと呼ぶ。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.8]{figure/memory_pattern.pdf}
    \end{center}
    \caption{メモリパターンの例}
    \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}

新たに追加される変数がメモリパターンに既に登録されている場合、
その変数は登録されない。
\\

メモリパターンは変数の集合である。
コードセグメントを実行することでいくつかの変数が変化した場合、
メモリパターンも変化したことになる(図\ref{fig:change_mem_pat})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.9]{figure/change_mem_pat.pdf}
    \end{center}
    \caption{コードセグメントの実行にともなうメモリパターンの変化}
    \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)による状態の探索の実装について述べる。

本研究では、イテレータを用いてDFSを実装した。
イテレータとは、配列やリストなどのデータ構造の各要素に対する
繰り返し処理を抽象化する手法のことである。

タブロー展開器はスケジューラとしての機能を備えている。
そのため、プロセスを実行する順番をリストとして持ち、制御する。
これをタスクリストと呼ぶ(図\ref{fig:task_list})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.9]{figure/task_list.pdf}
    \end{center}
    \caption{タスクリストの例}
    \label{fig:task_list}
\end{figure}

状態を展開する際に、このタスクリストに登録された順番にプロセスを実行していく。
したがって、プログラムの状態を一つ進めるためにタスクリストからタスクを取りだし、
実行するという処理が繰り返し必要になる。
その繰り返し処理を抽象化することで、データ構造の要素に対して行いたい処理を
簡潔に記述することができる。


DFSの実装の具体的な内容について述べる。

タスクリストからタスクを取り出す機構としてタスクイテレータを実装した。
タスクイテレータはその時点のタスクリストと状態データベースおよび
ひとつ前の時点のタスクイテレータを保持している(図\ref{fig:task_iterator})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.9]{figure/task_iterator.pdf}
    \end{center}
    \caption{タスクイテレータ}
    \label{fig:task_iterator}
\end{figure}

まず、最初のメモリパターンを状態データベースに登録後、
タスクイテレータの処理によりタスクを取りだしコードセグメントを実行する。
その実行によって、変化したメモリパターンを状態データベースからハッシュ値をもとに検索する。
同じメモリパターンがなかった場合、状態データベースに追加する。
その後、１段深く探索するために新たにタスクイテレータを生成し、
その時点の状態データベースを登録する(図\ref{fig:dfs1})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.9]{figure/dfs1.pdf}
    \end{center}
    \caption{タスクイテレータを用いたDFS 1}
    \label{fig:dfs1}
\end{figure}

同じメモリパターンがあった場合は、その経路の探索を終了し、
タスクイテレータにより次のタスクを取りだしコードセグメントを実行する。

タスクイテレータのタスクリストをすべて実行した場合、
そのタスクイテレータを破棄し、ひとつ前のタスクイテレータに戻る(図\ref{fig:dfs2})。
そこで探索可能な経路があればメモリパターンをレストアし探索を行う。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.8]{figure/dfs2.pdf}
    \end{center}
    \caption{タスクイテレータを用いたDFS 2}
    \label{fig:dfs2}
\end{figure}

これを繰り返していき、タスクイテレータが根に到達した場合、
全状態の探索が完了したことになる(図\ref{fig:dfs3})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.8]{figure/dfs3.pdf}
    \end{center}
    \caption{状態探索の完了}
    \label{fig:dfs3}
\end{figure}


\newpage
ソースコード\ref{src:tableau}に実際にタブロー展開を行っているコードセグメントを示す。

\lstinputlisting[caption=タブローコードセグメント,label=src:tableau]
{src/tableau.cbc}

タブローコードセグメントは、関数呼び出しを使用するためCwCで記述している。

\verb|get_memory_hash()|関数によってメモリパターンのハッシュ値を取得する。
そのハッシュ値をもとに\verb|lookup_StateDB()|関数で状態データベースの検索を行っている。
\verb|next_task_iterator()|関数は次に実行するタスクを取り出すものである。

\verb|restore_memory()|関数は任意の時点の状態に戻すための関数である。

実際にコードセグメントを実行するのは\verb|goto list->phils->next()|である。
引数付きgotoで検証対象のプログラムのコードセグメントに遷移する。

タスクイテレータが根に達した場合、探索を終了するために
\verb|goto ret(0),env|を実行している。

%\section{LZW法を用いた状態の圧縮}

\section{線形時相論理による仕様の検証手法}
タブロー展開を行う際に、線形時相論理(Linear-time Temporal Logic、LTL)式より
生成されたコードセグメントを実行することで検証を行う。

\subsection{検証の実装}
検証対象のプログラムからスケジューラに遷移した後、タブローコードセグメントに遷移する前に
LTL式より生成された検証用コードセグメントを実行する。
これにより、すべての状態において特定の性質を満たすことを調べることが可能である。

実装したDining Philosophers Problemプログラムに対してデッドロックの検出を行う。
デッドロックとは、複数のプロセスが互いに相手の占有している資源の開放を待ってしまい、
結果としてプログラムが停止してしまうことである。排他制御の欠陥で起こる。

Dining Philosophers Problemにおいて、資源とはフォークのことである。
つまり、この場合のデッドロックはすべての哲学者(プロセス)が左手でフォークを持ち、
右手のフォークが空くのを待っている状態である(図\ref{fig:dpp_deadlock})。

\begin{figure}[htpb]
    \begin{center}
	\includegraphics[scale=.5]{figure/dpp_deadlock.pdf}
    \end{center}
    \caption{Dining Philosophers Problemのデッドロック状態}
    \label{fig:dpp_deadlock}
\end{figure}


デッドロックを検知するために、 命題pを「すべての哲学者が左手にフォークを持っている」
として、 命題pが決して起こらないことを検査する。
これをLTL式で表すと□~pである。
これは、LTLで表現できる重要な特性の一つの安全性特性である。

これを検査するための検証用コードセグメントをソースコード\ref{src:check}に示す。

\lstinputlisting[caption=検証用コードセグメント,label=src:check]
{src/ltl.cbc}

\verb|p()|関数は命題pに相当するものですべての哲学者(プロセス)が
左手にフォークを持っているかを判定するものである。
checkコードセグメントがタブロー展開の際に実行されることで、
すべての状態において命題pが決して起こらないかどうかを検査することができる。

%%% end %%%