\section{Gears Agdaによるモデル検査の流れ}
今回作成した Gears Agda による DPP のモデル検査の流れは以下のようになっている.

\begin{enumerate}
  \item Gears Agda にて DPP の実装を行う
  \item プログラムが実行中に取りうる状態の網羅をする State List を作成する
  \item 上で実装したものを使用しつつ Meta Data Gear を構築する Meta Code Gearを記述する
  \item 上記 Meta Code Gear で作成された meta data を元に,dead lockを判定する Meta Code Gear を記述する
  \item 状態を網羅した State List にある State を一つずつ Meta Code Gear に実行させて,dead lockしている状態がないか確認する
\end{enumerate}

先行研究では網羅した状態データを State DB に格納していた.しかし今回の Gears Agda では State List にて代替とした.これは List で行った方が Agda での実装がしやすい点にある.本来は branced tree をデータ構造に持って State を作成するほう正しい.

dead lock の定義として,全てのプロセスが他のプロセスの実行終了待ちをしている.かつ新たに状態の分岐が作成できないものとした.
そこでstep実行してもプロセスがすべて変動がなく,かつStateの分岐が作成されなかったものを dead lock としている.

最後について,今回は状態の網羅を一度終了してから dead lock の有無を検証している.しかし,これは今回のプログラムが有限オートマトンであることは事前に明らかであるためにできたことである.検証したいプログラムが無限の状態を作成する場合は,Stateを作成するたびにそれに対して dead lock や live lock などのモデル検査をすることもできる.モデル検査中に意図しない動きがあった場合に停止するようにすることで,無限の状態を作成するプログラムであっても,モデル検査ができると考える.他にも,プログラムが取る状態を制限することで有限な状態を作成するようにし,モデル検査をすることもできる. (bounded model checking)

\section{Gears Agda によるDPPの実装}

DPP の記述の主要部分を示し，説明する．

\lstinputlisting[caption= Gears Agdaでの DPP の 哲学者の状態 , label=agda-dpp-state, lastline=7]{src/agda-dpp-impl.agda.replaced}

\lstinputlisting[caption= Gears Agdaでの DPP の プロセス , label=agda-dpp-process, firstline=9, lastline=16]{src/agda-dpp-impl.agda.replaced}

\lstinputlisting[caption= Gears Agdaでの DPP の Data Gear , label=agda-dpp-dg, firstline=17, lastline=21]{src/agda-dpp-impl.agda.replaced}

Code \ref{agda-dpp-state}は
前述した哲学者の状態を書き記して，哲学者が今行おうとしている動作を網羅している．

Code \ref{agda-dpp-process}は
哲学者一人ずつの環境を持っている．
pid はその哲学者がどこに座っているかの識別子で，
right / left hand はフォークを手に持っているかを格納している．
next-code は次に行う動作を格納している．

Code \ref{agda-dpp-dg} が Data Gear になる．
phは前もって定義した一人の哲学者のプロセスの List になる．
List になっている理由は，哲学者が複数人いるためである．
そのため実行時にListから一人ずつ取り出して実行をしていく．

tableはテーブルに置いてあるフォークの状態のことで，
pid が1の人の右側にあるフォークが List の最初にあり，
pid が1の人の左側にあるフォーク，すなわち pid が2の人の右側にあるフォークが
その次の List に格納されていくようになっている．
また，自然数の List になっているが，
その場所のフォークがテーブルの上にある場合は自然数の0が，
誰かが所持している場合はその人の pid が格納されるようになっている．

\lstinputlisting[caption= Gears Agdaでの DPP の Data Gear のinit, label=agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced}

Code \ref{agda-dpp-init}が入力から Data Gear を作成する Code Gear になる．
ここでは哲学者の人数を自然数で受け取り，人数分の List Phi と table を一つずつ作成し env を作成している．
また，最初の哲学者の状態は思考することであるため，next-code には C\_thinking を格納している．

\lstinputlisting[caption= Gears Agdaでの DPP の step 実行, label=agda-dpp-step, firstline=31, lastline=37]{src/agda-dpp-impl.agda.replaced}

Agda では並列実行を行うことができない．そのため step 単位の実行を一つずつ行うことで
並列実行をしていることとする．

この際に Env にある List Phi の中身を展開しながら一つずつ行動を処理していく．

\lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced}

Code \ref{agda-dpp-lfork}が step 実行をした際に哲学者が左側のフォークを取る記述になる．

左側のフォークを取る際には table の index は pid の次の値になっている．
図 \ref{fig:DPP} を見ると直感的に理解ができる．

最後の哲学者は一番最初のフォークを参照する必要がある．
フォークの状態を確認し，値が0である場合はフォークがテーブルの上にあるので
それを自分の pid に書き換える。次に left-hand を true に書き換えて手に持つ
フォークの状態が0以外，すなわち他の哲学者がその場所のフォークを取得している場合は
状態を変化させずに処理を続ける．
このように左のフォークを取る記述をした．

右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る．
比較するべき table の List と哲学者のListは一致しているため，pickup\_lfork のように最後の哲学者が
最初のフォークを参照することもない．

似たような形で哲学者がフォークを置く putdown-lfork/rfork を実装した．
思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている．

\section{Gears Agda によるDPPの検証}

これまでの実装は一般的なDPPの実装であったため,
Code / Data Gear の実装であった.
ここからは,モデル検査を行うため,Meta Data Gear の定義をし,
それの操作を行う Meta Code Gear の実装を行っていく.

以下\coderef{dpp-mdg}がMeta Data Gear の定義になる。

% ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
\lstinputlisting[caption=Gears Agda で DPP のモデル検査を行うための Meta Data Gear, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}

この Meta Data Gear の説明をすると,
metadataは状態の分岐数を持っておくnum-brunchがある.
MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)となる。
meta には前述したmetadataを持っており,
他には,deadlockしているかのフラグである deadlock ,
最後の2つは後に必要になるフラグである。
そのstate が step 実行済みなのかのフラグであるis-step,
そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている.

MetaEnv2 は1つのstate である MetaEnv の Listを metal で持てる.
加えて今まで実行していた Data Gear  を DG で持てる.

次に Meta Data Gear を作成する Meta Code Gear の説明をする。

\begin{enumerate}
  \item その状態から分岐できる状態数をカウントする Meta Code Gear
  \item Wait List を作成する Meta Code Gear
\end{enumerate}

以下の \coderef{dpp-mcg-branch} が分岐できる状態数をカウントする Meta Code Gear となる。

%ここにコードを載せる%
\lstinputlisting[caption=状態の分岐数をカウントする Meta Data Gear の定義, label=code:dpp-mcg-branch]{src/dpp-verif/dpp-metacode.agda.replaced}


実際にやっていることは,MetaEnv2 から state を取り出し,分岐を見る関数に遷移させている.その結果の List の length を meta データとしている.

つまり,この Meta Code Gear の実装にあたって新しい実装はほとんど行っていない.

Wait List の 作成も同じように取り出した state を step させて,そこで一致するnext-codeを状態が変わっていないとして Wait List に入れている.

%いちおうコード載せようかな？←棄却されました%

Wait List について,Thinking と Eathing の状態に関しては状態が変わる可能性がある.
これを Wait List に入れなければ Wait List のみで dead lock が検知できると考えられる.しかし,DPP以外の他のプログラムをモデル検査する際に,一つ一つ next-code の設定を行うのは煩雑であると考えた.そのため,step した際に状態が変化しないものを Wait List にいれた.これと分岐がない場合という条件にて,dead lock を検知する.これにより Meta Code Gear の作成が簡易化された.そのため,Thinking と Eathing のプロセスも Waithing List に入るようになっている.

deadlockの検出方法として,上記の2つのMeta Code Gear で作成したmeta データを使用する.

そして「num-brunchの値が1であり,wait Listの数がプロセス数と一致する」ということは,「その状態から別の状態に遷移することができない」として,この状態をdead lockであると定義した.

以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる。

複雑なことは何もしておらず,単純にstate毎のnum-brunchの値を見て,wait-listの数がプロセス数と一致していた場合に
deadlockのフラグを立ち上げている.これが,Gears Agda におけるアサーションになっている.

% judge-dead-lock-pのソースコードを貼り付ける
\lstinputlisting[caption=DPP での dead lock を検知する Meta Code Gear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced}
% こいつはmetaEnv2を受け取れるように変えないと行けない

ここから前述した通り,State Listを作成する.

そのまま実行するだけでは無限に実行されるのみで停止しないと思われる.
しかし,分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる.
存在していた場合はそれを追加せず,存在しなかった場合にのみ State を追加する.

Agdaには2つの record が等しいか確かめる関数などは存在せず,
\coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つずつ一致しているか確認する.
こちらはそのまま掲載すると長いので,実際のコードに手を加えて省略している.実際のコードは付録にて参照できる.

\lstinputlisting[caption=重複しているstateを除外する Meta Code Gear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced}
% 手を加えているので詳細は付録を参照するように促す

MetaEnv2 を受け取ってその中身の state を比較するが,そこまで展開する必要がある.
 loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている.

更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し,次のstateの一致を探索するように記述されている.

実際にstateの一致を見ているのは22行目のeq-env関数で,一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている。

State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている.
その値が一致している場合には別の値を見て,一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている.
他の値である,lhandやrhandなども eq-pid と同じように記述している.


これらにて,まだ分岐を見ていない1つのStateの分岐を確かめる.
発生した分岐を step 実行させる.
step実行して作成された state が State Listに存在していないかを確かめる.
これを繰り返すことで State Listを作る.
State List に存在している全ての state の分岐を見たということは,
出現するStateを全て網羅することができたと言える.

あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる。

\section{Gears Agda による live lockの検証方法について}
live lockとは,状態が変動しているが,その状態はループしており,実行が進んでいないことを指す.

DPPにて例を上げると,(上の哲学者のフローだと) dead lock が発生するため,フローを変更したとする.それは以下のような動作を追加する.
「右手にフォークを持っているが,左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」
とする.これで解決すると思われるが,全員が同時に食事をしようとした場合,右手のフォークを取ったり置いたりを永遠に繰り返すことになる.
これを live lock という

つまり,この状態を検知するなら,そのstateが持っているhistoryまで考慮する必要がある.つまり,今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い.

history がloopしていた際に,誰もeathingしていない場合を live lock していると定義する.

今回のはDPPであるためEatingが挙げられているが,他の実装であれば,どのコマンドが実行されるのが正常な動きなのかを決める.それがloop中に存在しているかを確認することで live lock を検知できる.


\section{Gears Agda でのモデル検査の評価}

SPINで行ったDPPのモデル検査に比べると,Gears Agdaの方がコードも長く、制約が多いため難解に思える.しかし,Gears Agda ではプログラムの実装も含んでいる.

さらに,Gears Agda での実装をしたあとのモデル検査を行う際の Meta Code Gear の流れは変化しないため,他のプログラムに適応できることを考えると比較的容易であると言える.

加えて,Gears Agda は CbC へコンパイルされ,高速に実行されることを踏まえると,いかに Gears Agda が検証に向いたプログラムであるか理解できる.

% この評価の話はまとめでしたほうがいいかもね？