\chapter{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 を検証する事が可能である。


\section{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}

\section{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を用いて同じ状態を検索することで終了判定をだす。

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

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

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


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


\section{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}

\section{Meta の入れ替え}
    Perl script の正規表現を使って meta を機械的に置き換える。mcMeta か random 。random は並行実行のシミュレーションになる。
    7行目は多次元リストのPhilsImpls を regular expression に渡している。これはgoto の遷移先である。
    その後11行目で受け取った文字列を goto 先にランダムに、配置しており。
    16行目では文字列を受け取った文字列に遷移する前に mcMeta を挟むようにしている。 
\lstinputlisting[caption=mcDPP.h, label=mcDPP.h]{src/meta.pm}

    \newpage
    
 \section{モデル検査のフラグの管理}
 mcDPP.h はモデル検査を行うためのフラグの宣言である。
 \lstinputlisting[caption=mcDPP.h, label=mcDPP.h]{src/mcDPP.h}
 しかし今回の DPP の例題においては t\_eating と f\_F\_eating のフラグしか使用してしいない。
 
  t\_eating は食事中で f\_F\_eating がいつか食事になるという意味である。

  now と next を見比べながらフラグを update する。すべて状態は 今のcontext にのっているが、過去は add\_memory\_rangeで記録されたものあるいはフラグしか見れないようになっている。

q\lstinputlisting[caption=mcDPP.cbc, label=mcDPP.cbc]{src/mcDPP.cbc}
これは 検証したいCTL あるいは LTTLによって違うものになる。
mcDPP.cbcではフラグの比較によるモデル検査を行っている。
最初に今のフラグと次のフラグを取得し、次にphils->self が 1 である場合はreturn でぬける。
12行目では 次と今のフラグがet\_ating または t\_F\_eatingであればt\_F\_eating;
15行目では直前のフラグと今のフラグ、または直前のフラグと次のフラグが違っているとchangeに1が入り、動き続け、そうでなければ18行目で今のフラグとt\_F\_eatingを比較し、あっている場合にはnot<>eating となり、終了する。


\section{導出木の作り方}
\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}
\section{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として実現されているものと、x.v6 の書き換えとして実現するものとの二種類がある。
後者の開発にモデル検査が使えると良い。