-title: Gears OSのモデル検査の実装

--abstract:

Gears OSは継続を基本とするKernelとUser Programの記述を採用している。メタプログラミングにより、元のプログラムを変更することなくモデル検査を行うことができる。ここではcodeGear単位での可能な並列実行の列挙を登録したdataGearに対して行うことによりCTLで記述された仕様を検証することができた。検証のメモリとCPUの使用量、技術手法についての考察を行う。

-- OS の信頼性

 OS とは一般的にハードウェアへのアクセス、資源管理を行っているソフトウェアである。つまりコンピュータに接続されている全てのメモリやハードディスクといった記憶装置、また CPU や GPU といった計算処理装置には通常 OS の機能を利用する事でしかアクセスすることは出来なくなっている。

これはコンピュータ上で同時に複数のアプリケーションを利用することが可能なため、それぞれのアプリケーションの動作によって別々に資源要求をする場合がある事になる。この時アプリケーションから直接資源へのアクセスを許してしまうと、ハードウェアで競合が起きてしまい正常な処理が行えなくなってしまう可能性がある。
このためハードウェアのアクセスを OS を通して行うことによって、ハードウェアでの競合が発生しないようになっている。
複数のアプリケーションからのタスクを受け取るが、これらの実行する順番やアクセスする時間を管理することで CPU もしくは GPU の利用を複数スレッドに割当ることによって処理効率の向上を図っている。

 またハードウェアへのアクセスや資源管理は複雑で容易ではなく、異なるハードウェアを扱う際にはそれぞれに対応したプログラミングが必要である。しかし OS がこれらのデバイスのアクセスや資源管理を行う機能を持つ事によって、アプリケーション側はハードウェアの違いを気にすることなく、プログラミングする事が出来る。

このように OS はハードウェアのアクセス、資源管理を行う事によって、ハードウェア上での競合を防ぎ、アプリケーションの効率化と複雑な処理を受け持つ重要なソフトウェアである。
そのため OS の不具合はコンピュータの全ての動作に影響するため、その信頼性はも重要なものであり、また時代とともにユーザーインターフェースや、ネットワークサービス、セキュリティといった進歩するハードウェア、サービスに対応して、OS 自体が拡張される必要がある。
しかし、OS は非決定的な実行を持つため、その信頼性を保証するには従来のテストとデバックでは不十分と考えられる。

 テストとはソフトウェアやアプリケーションの検証は用いられる手法で、ソフトウェアあるいはアプリケーションに対して、任意の入力を与えた場合に設計で予想された出力が返ってくる事を確かめる事によって信頼性を保証する手法である。
このテストによる手法は、検証側が定めた範囲での入力による検証であるため全ての入力を抑えられてない場合があり、テストしきれない部分が残ってしまう可能性がある。
このため、実装が必ずしも設計に沿っているとは保証しきれないという問題点がある。

 テスト以外の信頼性を保証する検証としては形式検証があり、形式検証には定理証明とモデル検査\cite{EdmundM}の２つの手法がある。

定理証明は数学的な証明を用いて信頼性を保証する手法である。証明を用いるため、入力や、状態数に比較的影響をうけずに検証を行う事が出来るが、場合分けの複雑化や、場合分け自体が多くなる事がある。agda\cite{agda} といった定理証明支援器と言われるものがある。しかし証明には数学的な知識が不可欠となる

モデル検査は抽象化されたソフトウェアの実装である。プログラムの仕様である logic を満たすかどうかをモデル検査器を用いて調べる事で信頼性を保証する。
モデル検査の場合、自動で全ての状態を網羅的に出力し調べるため検証時間を工夫して短くすることが出来る。

 本研究室で開発している Gears OS\cite{gears} は アプリケーションやソフトウェアの信頼性を OS の機能として保証することを目指しており、信頼性を保証する手法としてモデル検査やhoare logic を用いた定理証明\cite{agda-ryokka}を用いて信頼性へのアプローチを行っている。
 本論文では、このGears OS におけるモデル検査を実現する手法について考察する。

--モデル検査とは

モデル検査は、検証したい内容の時相論理式 p をつくり、対象のシステムの初期状態 s のモデル M  があるとき、M,s が p を満たすか (M,s $\models$ p と表記される)モデル検査器を用いて調べることによって信頼性を保証する手法である。

様相論理式にはCTL(Computational Tree Logic)やLTTL(Linear Time Temporal Logic)といったものがあり、それぞれ計算木論理、線形時相論理と言われるものである。またこの2つを合わせたCTL*というものがある。

今回の研究ではLTTLを用いて検証を行う。LTTLは時間を可能性や必然性として様相として持つ線形時相様相論理であるため、状態の遷移や時間の経過を基準に証明を行う場合に利用され、特にシステムのハードウェアやソフトウェアの仕様を記述する手法として用いられる。

モデル検査は様相演算子によって表され、状態が複雑なほど様相演算子で表す状態が増えるため論理式も複雑になってしまう。
そのためモデルによってCTL、LTTL、CTL*の3つの論理式から適切なものを選び検証を行う事で、論理式の複雑度を抑える必要がある。
CTLとLTTLの違いは、LTTLは枝の指定がなく、全ての枝でその状態が存在するか否かを見るので、経路ごとの表現ができない。しかしCTLは時相演算子の使い方に制約があるため、全てのLTTLをCTLで表現することはできない。


--様相演算子

モデル検査を記述するのに使われる論理式の様相演算子は、枝を表すパス量化子と、いつ成り立つかを表す時相演算子がある。
CTLとLTTLでは使われる様相演算子に違いはあるがCTL*ではどの様相演算子も使うことが出来る。


パス量化子
\begin{itemize}
\item ある枝で存在する E
\item 全ての枝で存在する A
\end{itemize}

時相演算子
\begin{itemize}
\item 枝の次の状態で成り立つ X
\item この先いつか成り立つ F
\item このあとずっと成り立つ G
\item この先いつか状態aになる、そのときまでは状態bが成り立つ U
\item 状態bがなりたつまで状態a成り立つ R
\end{itemize}

この様相演算子を用いて表した CTL の導出木が図2.1 から 2.4のようになる。

\begin{figure}[htbp]
  \begin{center}
    \begin{tabular}{c}

      \begin{minipage}{0.50\hsize}
\begin{center}
      \includegraphics[width=70mm]{images/graphEF.pdf}
      \caption{ある枝でいつか真になる EF}
    \label{fig:EF}
\end{center}
\end{minipage}

    \begin{minipage}{0.50\hsize}
   \begin{center}
  \includegraphics[width=70mm]{images/graphAF.pdf}
\caption{すべての枝でいつか真になる AF}
    \label{fig:AF}
\end{center}
\end{minipage}
   \end{tabular}
\end{center}
\end{figure}

\begin{figure}[htbp]
  \begin{center}
    \begin{tabular}{c}
  
 \begin{minipage}{0.50\hsize}
  \begin{center}
    \includegraphics[width=70mm]{images/graphEG.pdf}
  \caption{ある枝でいつも真になる EG}
    \label{fig:EG}
  \end{center}
  \end{minipage}

 \begin{minipage}{0.50\hsize}
    \begin{center}
      \includegraphics[width=70mm]{images/graphAG.pdf}
    \caption{すべての枝でいつも真になる AG}
    \label{fig:AG}
    \end{center}
    \end{minipage}
    \end{tabular}
\end{center}
\end{figure}

参考:蓮尾 一郎,モデル検査入門(2009年)p12\cite{graph}


--モデル検査の実装例

モデル検査の方法としてよく利用される物として、SPIN と java path finder(以下JVM)というツールがある。

SPIN は Promela という仕様記述言語で記述する事でC言語の検証器を生成する事で、コンパイルまたは実行時に検証する事ができる。

チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。
SPINではオートマトンの並列実行処理の検証が可能であるが、これは厳密には実行するステートをランダムに選択し、実行することで実現している。
SPIN では以下の性質を検査する事ができる。
\begin{itemize}
\item アサーション
\item デッドロック
\item 到達性
\item 進行性
\item 線形時相論理で記述された仕様
\end{itemize}

Java Path Finder(JPF) は java プログラムに対するモデル検査ツールで、javaバーチャルマシン(JVM)を直接シミュレーションして実行している。そのため、javaのバイトコードを直接実行可能である。

バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査する。しかしバイトコードの実行パターンを網羅的に調べるために、膨大なCPU時間を必要とする。

またJVMベースであるため、複数のプロセスの取り扱いが出来ず、状態空間が巨大になる場合は直接実行は出来ず、一部を抜き出してデバックをするのに使用される。
JPF では以下の事ができる。
\begin{itemize}
\item スレッドの可能な実行全てを調べる
\item デッドロックの検出
\item アサーション
\item Partial Order Reduction
\end{itemize}
\chapter{Gears OS とCbC}
%信頼性を保証する一つの方法は、プログラムの可能な実行を数え上げて要求仕様を満たしているかどうかを調べるモデル検査である。
%本論文では、Gears OS 上のアプリケーション、さらに Gears OS そのものをGears OS 上でモデル検査することに関して考察する。

--Continuation based C

Gears OS は軽量継続を基本とする言語  Continuation based C (以下 CbC )\cite{CbC}を用いた OS の実装である。

CbC は Code Gear という単位を用いて記述する C の機能を持つプログラミング言語である。コンパイルには llvmcbc\cite{llvmcbc} を用いて行う。Code Gear は一般的な処理記述にあたり関数に比べて細かく分割されている。Code Gear 間の遷移は軽量継続である goto 文によって行われる。

軽量継続である goto は継続前の Code Gear に戻ることはないため、プログラムの記述をそのまま状態遷移に落とし込むことが出来る。
Cの関数の型が\verb+__code+ であるような構文で定義することができる。
つまり、codeGearはdataGearを通して、次のcodeGearに goto で接続される(図\ref{fig:code-datagear})。

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=140mm]{fig/input-outputDataSegment.pdf}
    \end{center}
    \caption{codeGear と DataGear}
    \label{fig:code-datagear}
\end{figure}


例えば、ソースコード3.1は DiningPhilosohersPloblem(以下DPP) の例題で右のforkを取るという処理を行っているは以下のように書ける。
ここでは \verb+cas+ (check and set)と busy wait で書いてある。
通常の関数呼び出しと異なり、stackや環境を
隠して持つことがなく、計算の状態は codeGear の入力ですべて決まる。

\lstinputlisting[caption=pickUrforkp, label=pickUprfork]{src/PhilsImpl.cbc}

メタ計算 と stub
codeGear の入力は dataGear と呼ばれる構造体だが、これにはノーマルレベルの dataGear とメタレベルの dataGear の階層がある。メタレベルには計算を実行する CPU やメモリ、計算に関与するすべてのノーマルレベルの dataGear を格納する context などがある。context は通常の OS のプロセスに相当する。

遷移は次の図(\ref{fig:meta_Gear})の上のように codeGear から Code Gear に移動するだけだが、その前に出力する dataGear を context に書き出す必要がある。
これは通常の関数呼び出しのreturnの処理に相当する。

図3.2の下はメタレベルから見た codeGear である。
goto 先は meta という meta codeGaer であり、そこで必要なメタ計算が行われる。ここに任意のメタ計算を置くことができる。
この場合の引数は context と行き先を表す番号だけである。
ソースコード3.2は DPP における 右のフォークを持ち上げる例題の stub\cite{gearsOS2} である pickup\_rfork\_stub と、その stub meta に goto する ノーマルレベルのものになる。
このようにノーマルレベルの CodeGear からメタレベルに遷移する際には goto meta で引数を渡すだけで、メタレベルの計算は隠されている。

\lstinputlisting[caption=pickuprfork, label=pickuprfork]{src/pickup_rfork.cbc}

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=150mm]{fig/meta_gear.pdf}
    \end{center}
    \caption{Gears OS のメタ計算}
    \label{fig:meta_Gear}
\end{figure}

メタレベルから見ると、codeGearの入力は context ただ一つであり、そこから必要なノーマルレベルのdataGearを取り出して、ノーマルレベルのcodeGaerを呼び出す。この取り出しは stub と呼ばれる meta codeGear によって行われる。(図\ref{fig:Context_ref})
これは通常の関数呼び出しのABI(引数とレジスタやスタック上の関係を決めたバイナリインターフェース)に相当する。
\newpage
 stub codeGear は codeGear の接続の間に挟まれる Meta Code Gear である。ノーマルレベルのcodeGear から MetadataGear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。stub Code Gear はこの問題を防ぐため、Context から必要なdataGaerのみをノーマルレベルに和刺す処理を行なっている。

 このようにノーマルレベルの Code Gear からは context を見ることはできず、メタ計算レベルではノーマルレベルの引数の詳細を気にしないで
処理を行うことができるようになっている。ノーマルレベルとメタレベルは、必要ならばCPUのsystem mode と user mode の状態を変えても良い。

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=140mm]{fig/Context_ref.pdf}
    \end{center}
    \caption{Contexが持つDataGaerへのアクセス}
    \label{fig:Context_ref}
\end{figure}

\clearpage

--Gears OS における DPP の検証

ここでcodeGearの実行はOSの中での基本単位である必要がある。つまり、codeGearは並行処理などにより割り込まれることなく、codeGearで記述された通りに実行される必要がある。しかしこれは一般的には保証されないものであるため、他のcodeGearによって共有されている dataGearに競合的に書き込んだり、割り込みにより処理が中断したりする可能性が存在する。

しかし、Gears OS は codeGear が正しく実行さることを保証される。つまり、Gears OS は CodeGear　の処理によって競合が起きないように実装されているとする。

プログラムの非決定的な実行は入力あるいは並列実行の非決定性から発生する。後者は並列実行される codeGear の順列並び替えとなる。よってこれらの並び替えを生成し、その時に生じる context の状態をすべて数え上げれれば\cite{tauble}モデル検査を実装できることになる。

ただし、context の状態は有限状態になるとは限らず、また有限になるとしても巨大になる場合が考えられる。この場合は OS やアプリケーションのテストとして動作する十分な状態にまで、 context の状態を抽象化することができればモデル検査を行えると考えられる。


メモリ領域の集合で一つの状態が定義され、この状態をさらに格納するデータベースを用意する。codeGearのシャッフルの深さ優先探索を行ない、新しく生成された状態をデータベースで参照し、既にあれば、深さを一つ戻り、別な探索枝に移ると言った動作を行うことで新しい状態が生成されてない、もしくは、バグを見つければモデル検査は終了と言うことになる。

ここでは例題として Dining Phisopher 問題のdead lockの検出を行う。

(1)  Dining Phisopherを Gears OS上のアプリケーションとして実装する(DPP)。

(2) DPPをcodeGearのシャッフルの一つして実行する meta codeGear を作成する。

(3) 可能な実行を生成する iterator を作成する。

(4) 状態を記録する memory 木と状態DBを作成する。

この段階でDPPのモデル検査が可能になるはずである。

一方で Gears OSそのものも codeGear で記述されている。CPU毎のC.context、そして、それが共有するKernelのK.context、それからユーザプログラムのU.context などの context からなると考えれ、これら全体は meta dataGear である K.context に含まれていると考える。

また、U.context がDPPのように単純なものであれば OS 全体の context も複雑にはならないため、モデル検査を Gears OS 全体に対して実行可能であると考えられる。

(5) Gears OSを含む codeGear のシャッフル実行を行ない、モデル検査を行う。

これにより、Gears OSの自分自身によるモデル検査が可能になる。この時に、検査するcodeGearと検査されるcodeGearは同じ物であるが、
実行する meta codeGarが異なっている。現状では、これは異なるmeta codeGearを指定してコンパイルしなおすことにより実現する。

Gears OSの実装は Unix 上のアプリケーションとしての実装と、x.v6\cite{xv6}の書き換えによる実装の二種類があるが、前者ではアプリケーションはOSに直接リンクされる。後者では x.v6 のexec機構により実行される。実際にOSのモデル検査を実行するためには、必要なmeta dataGear/meta codeGear　の emulatorを書く必要がある。しかし、検査する必要がない部分は無視できるようにしたいと考えている。

Gears OSは並列実行機構を持っているので、

(6) モデル検査を並行実行\cite{tauble2}することができる

と考えられる。

--Gears OS におけるモデル検査

Gears OS 上で DPP を動かし、導出木を作成。これをLTTLに落とし込むことによってdead lock とlive lock の2つを探索することが可能である。

dead lock とは、スレッドが待機状態に入ったままになってしまう状態を指し、今回扱う DPP の例題だと、全てのスレッドが1つずつfork を持ってしまった場合に発生する。

またlive lock とは待機状態ではないが、同じ状態を繰り返してしまい処理が進まない状態をいい、今回の DPP の例題において「待機状態においてフォークを下ろす。」という処理を入れた場合で、さらに各スレッドが順番に動作するとした時、 dead lock の状態に入った場合において、各スレッドは fork を下ろす動作をするが、その後またfork を持ち上げる動作を行うので live lock 状態になる。
このようにdead lock 状態ではないが、状態が膠着状態になるのがlive lock である。

LTTLで検証できる 常に p または　常に$\neg$p と、いつか p またはいつか$\neg$p であるから、dead lock を検証する事が可能である。

--Dining Philosophers Problem の例題

モデル検査の検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。

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

各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。

以下はDPPにおける右側のフォークを取るプログラムである。
最初に右のフォークを持たれているかどうかを確認し、いなければ自分を持ち主に登録する。
その後 next に次に遷移する自分の状態を入れ scheduler に遷移することによって scheduler を通して次の状態に遷移する。このときscheduler からメタ計算を挟むことによって状態をMemoryTree に入れる事ができる。
左のフォークの持ち主がいた場合は飢餓状態を登録し scheduler に遷移する事で待機状態を維持する。

\lstinputlisting[caption=pickuplfork, label=pickuplfork]{src/pickup_lfork.cbc}

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=140mm]{fig/dpp_image.pdf}
    \end{center}
    \caption{Dining Philosohers Ploblem image}
    \label{DPP_image}
\end{figure}


--Gears OS を用いた DPP 

DPP は哲学者5人が同時に行動するので、5つのスレッドで同時に処理することで状態を生成する事ができる。まず Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\verb+__exit+を渡す。par goto で生成された Task は\verb|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能である。
%また Gears OS には Synchronied Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue があり、これを使い5つのフォークの状態を管理する。
%Syncrhonized Queueは CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う命令である。
5つのフォークの状態はCASで管理する。
CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータがないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗し、もう一度 CAS を行う。
5スレッドで行われる処理の状態は以下の6通りで、think のあとPickup Right fork に戻ってくる。
\begin{itemize}
\item Pickup Right fork
\item Pickup Left fork
\item eating
\item Put Right fork
\item Put Left fork
\item Thinking
\end{itemize}


この状態は goto next によって遷移する。状態を遷移する際、MemoryTreeによって状態を保存する。またこの状態遷移は無限ループするのでMemoryTree に保管される。またこのMemoryTreeはスレッドの数だけあり、sutats DB によってまとめられている。

DPPの状態遷移は6つの状態を繰り返すため、同じ状態が出た場合には終了させなければならない。そこでstate DBを用いて同じ状態を検索することで終了判定をだす。

この実行は Single thread に行われるが、iterator を使って並行実行しても良い。

必要な時相論理的な仕様は codeGear にコンパイルすることができるので、それを同時に走らせることによりチェックできる。
これは SPIN の LTL の仕様記述と同じことになる。このようにモデル検査を codeGear と dataGear 上に実現することができる。


メモリ領域の登録には
\verb|add_mamory_area(ContextPtr cbc_contex |
\verb|,void *addrss,long length) | のようなAPIを用いる。
状態の格納は、mera codeGear で行われるので、customize が可能である。この段階で対称性の利用や状態の抽象化を行うこと可能となる。


\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=140mm]{fig/model_checking.pdf}
    \end{center}
    \caption{DPP on Gears OS}
    \label{DPP_chacking}
\end{figure}


--Gears OS でのモデル検査実装

モデル検査を行うのに、次のものを用意した。
\begin{itemize}
\item MCTaskManagerImpl.cbc (導出木を作るために dataGear に process (context) を登録する。)
\item MCWorker.cbc (導出木を作る meta codeGear)
\item TaskIterator.c
  次の実行を選択する interator
\item memory.c ( memory range の扱い (2分木))
\item crc32.c ( memory 状態の hash)
\item state\_db.c (状態の data base (2分木))
\end{itemize}

--Meta の入れ替え

今回のモデル検査では全ての状態を走査する、またこれはランダムに行う必要がある。
CbC で実装された DPP は ソースコード4.2 の　Perl script meta.pm によって正規表現を用いて 遷移先の meta を機械的に置き換える事によってランダム実行を行っている。

mcMeta はモデル検査を行う場合で random は並行実行のシミュレーションを行う場合となっている。
    7行目は多次元リストのPhilsImpls を regular expression に渡している。これはgoto の遷移先である。
    その後11行目で受け取った文字列を goto 先にランダムに、配置しており。
    16行目では文字列を受け取った文字列に遷移する前に mcMeta を挟むようにしている。 
\lstinputlisting[caption=meta.pm, label=meta.pm]{src/meta.pm}
    
--モデル検査のフラグの管理

 ソースコード4.3 の mcDPP.h はモデル検査で使われるフラグの宣言をしている。
 \lstinputlisting[caption=mcDPP.h, label=mcDPP.h]{src/mcDPP.h}
 しかし今回の DPP の例題においては t\_eating と f\_F\_eating のフラグしか使用してしいない。
 

DPPの例題は食事とそれ以外の状態を循環しているため t\_eating フラグの「食事中」と f\_F\_eating フラグの「いつか食事にする」という２つの状態で表すことが可能となる。また今回のモデル検査では DPP でのデッドロックの検出を行う。

デッドロックはプログラムの処理が止まってしまっている状態であるため、上の２つのフラグがついていない状態がデッドロックということになるため、２つのフラグによって表す事が出来る。

フラグは now と next を見比べながら update する。すべての状態は 今のcontext にのっているが、過去は add\_memory\_rangeで記録されたものあるいはフラグしか見れないようになっている。
 
ソースコード4.4 のmcDPP.cbc ではフラグの比較によるモデル検査を行っている。
 \lstinputlisting[caption=mcDPP.cbc, label=mcDPP.cbc]{src/mcDPP.cbc}
 


最初に今のフラグと次のフラグを取得し、次にphils-\>self が 1 である場合はreturn でぬける。
12行目では 次と今のフラグがet\_ating または t\_F\_eatingであればt\_F\_eating;
15行目では直前のフラグと今のフラグ、または直前のフラグと次のフラグが違っているとchangeに1が入り、動き続け、そうでなければ18行目で今のフラグとt\_F\_eatingを比較し、あっている場合にはnot<>eating となり、終了する。


--導出木の作り方
\lstinputlisting[caption=putdown\_lfork, label=putdownlfork]{src/putdown_lfork.cbc}
ソースコード5.5 は DPP の例題のもので、Philospher の Leftfork を置く部分である。フォークは各 Philosher 間で共有されるデータのため、競合が起きないように CAS を行う必要がある。
このソースコードは以下のソースコード5.6に変換される。
Gearef はContext から Data Gaer を参照するマクロになっている。
goto 先がmcMeta になっている。

\lstinputlisting[caption=putdownlforkImpl, label=putdownlforkImpl]{src/putdown_lforkImpl.cbc}

Gears OS のノーマルレベルの code は変換されるが、mcMeta は \_\_ncode と記述されており、これは meta として扱い変換しない意味である。
9行目にある mctiにタスクを渡している。

\lstinputlisting[caption=mcMeta, label=mcMeta]{src/mcMeta.cbc}

--実行結果

次にモデル検査を行った結果を一部抜き出して掲載する。

not<>eating はデッドロックフラグである
次の5つの値はフォークを持っているスレッドを表しており、この場合は各スレッドが一本ずつ持っている状態を表している。
食事をしているスレッドがある場合は5つの値のうち2つは同じ値になっている。
その次の5つの値が各スレッドの状態を示している。
flag 0 の後の部分がstateDBによって同じ状態のものを探しハッシュ値で抽象化している部分となり、最後にこの処理を行っていたスレッド番号となっている。

\begin{itembox}[1]{モデル検査の実行結果を一部抜粋}
\begin{verbatim}
not <> eating
00000000 01000000 02000000 03000000 04000000 
01000000 01000000 01000000 01000000 01000000
flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 5

not <> eating
00000000 01000000 02000000 03000000 04000000 
01000000 01000000 01000000 01000000 01000000
flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 4

not <> eating
00000000 01000000 02000000 03000000 04000000 
01000000 01000000 01000000 01000000 01000000
flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 3

not <> eating
00000000 01000000 02000000 03000000 04000000 
01000000 01000000 01000000 01000000 01000000
flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 2

not <> eating
00000000 01000000 02000000 03000000 04000000 
01000000 01000000 01000000 01000000 01000000
flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 1
\end{verbatim}
\end{itembox}

--評価

--今後の展開


---OS自体のモデル検査

Gears OS 自体も CodeGear と DataGear で書かれているので、CPU毎の C.context、共有するkernel のK.context、ユーザープログラムの U.context と考えることができ、これらはmeta dataGear であるK.context に含まれている。

U.context がDPPのような単純なものならば、OS全体のcontext も複雑にはならないため、DPP のモデル検査のようにシャッフル実行を行う事が出来れば、この枠組みの中で検証することが可能であると思われる。

しかし、OS のモデル検査にはいくつかの問題がある。

OS の場合はほとんどが meta level の記述なので、それを emulation する必要がある。メモリやCPUは問題ないが Translation Lookaside Buffer (以下TLB) を emulation する必要があるが、TLB は仮想アドレスから物理アドレスへの変換を高速化する際に使われるメモリ管理ユニットのキャッシュであり、またマイクロプロセッサによる物理空間と仮想空間の仮想記憶をサポートする際に利用しているため、emulation の仕方に工夫が必要となる。

また CPUの状態、例えばキャッシュなども emulation する場合には、codeGear の大きさをメモリアクセスレベルまで小さくする必要がある。
つまり、見つけたいバグを知っていれば検証は可能だが、起きる可能性のある未知のメタ計算が出てくる場合の検証方法と、その未知のメタ計算を探す手法が必要となってくる。

モデル検査は膨大な状態空間を探索する必要があり、OS 込みのモデル検査となると厳しいと予想される。
しかし、OS 特定部分だけに絞り調べる場合には巨大なアプリケーションは必要ない思われ、普通のテストの代わりにモデル検査を使うように検証を行う事が出来ると考えられる。

この OS を含むモデル検査は OS の拡張性をデバイスドライバの開発などに向いていると考えられる。この場合は、デバイス自体の仕様が codeGear/dataGear
で書かれている必要がある。

Gears OS は Unix 上のApplicationとして実現されているものと、xv6 の書き換えとして実現するものとの二種類がある。

xv6 は linux を素体としたもので OS としては小さい構造となっている。そのためまずはこのxv6 に対してモデル検査を行えるようになることが OS 自体のモデル検査を行う上での次の目標となる。

---プログラムの展開と状態数の抽象化
 GearsOS におけるモデル検査はプログラムの実行を網羅的に行うことでプログラムの状態を展開しデッドロックを調べる。反例を探す場合はプログラムの状態を展開しつつ反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての状態を生成する必要がある。状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数乗の計算量がかかる。この展開の際に仕様も同時に展開することでプログラムに対する仕様の検証を行う事が可能である。

状態の展開は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。

---dataGear

スレッド数がランダムで決まる、または途中でスレッドが増える例題がある場合について考える。
その例題を走査するためには、スレッド の状態を memoryTree として保管する iterator をスレッドの数だけ用意する必要がある。
しかし現在のData Gear は予め生成しておいたものであり、実行中に生成をする方法がない。
また生成される Data Gear は iterator であるためノーマルレベルからは呼び出せないようにしておく必要がある。このため Data Gear の自動生成 には工夫が必要となる。

---Gears Debugger

モデル検査を行った際に、メモリの状態を iterator で保管している。

このmemoryTree を実行履歴としてtrace し遡ることが出来れば、展開された状態から任意の実行状態を作る事が可能であると考えらる。さらに mcMeta に対して debugger を埋め込む事によって、状態の展開から bug の発生箇所を発見し、debug することが可能であると考えられる。

---Red Black Tree への応用
Red Black Tree は平衡二分木の一種で複雑な構造ではあるが、探索、挿入、削除の最悪計算量O($\log${n})となるものである。この例題のモデル検査したいと考えている。

Red Black Tree をモデル検査するためにはノードを循環構造に事によって状態を有限で表す必要があり。またノードの値を iterator で整合性の検証の仕方について考察する必要がある。

% \chapter{まとめ}
%Gears OS でのモデル検査の実装方法について考察した。DPPの検証自体は前に書かれたことがある\cite{}。
%この時のmemory tree と state DB を使うことも可能だが、これ自体はCで書かれている。
%これもcodeGear で書く方が望ましい。まず、DPPを動かすとこから始めて、OS自体を検証する方向に研究を進めていきたい。