|
7
|
1 \section{Gears Agda によるDPPの実装}
|
|
1
|
2
|
|
|
3 DPP の記述の主要部分を示し，説明する．
|
|
|
4
|
|
|
5 \lstinputlisting[caption= Gears Agdaでの DPP の 哲学者の状態 , label=agda-dpp-state, lastline=7]{src/agda-dpp-impl.agda.replaced}
|
|
|
6
|
|
|
7 \lstinputlisting[caption= Gears Agdaでの DPP の プロセス , label=agda-dpp-process, firstline=9, lastline=16]{src/agda-dpp-impl.agda.replaced}
|
|
|
8
|
|
|
9 \lstinputlisting[caption= Gears Agdaでの DPP の Data Gear , label=agda-dpp-dg, firstline=17, lastline=21]{src/agda-dpp-impl.agda.replaced}
|
|
|
10
|
|
|
11 Code \ref{agda-dpp-state}は
|
|
|
12 前述した哲学者の状態を書き記して，哲学者が今行おうとしている動作を網羅している．
|
|
|
13
|
|
|
14 Code \ref{agda-dpp-process}は
|
|
|
15 哲学者一人ずつの環境を持っている．
|
|
|
16 pid はその哲学者がどこに座っているかの識別子で，
|
|
|
17 right / left hand はフォークを手に持っているかを格納している．
|
|
|
18 next-code は次に行う動作を格納している．
|
|
|
19
|
|
|
20 Code \ref{agda-dpp-dg} が Data Gear になる．
|
|
|
21 phは前もって定義した一人の哲学者のプロセスの List になる．
|
|
|
22 List になっている理由は，哲学者が複数人いるためである．
|
|
|
23 そのため実行時にListから一人ずつ取り出して実行をしていく．
|
|
|
24
|
|
|
25 tableはテーブルに置いてあるフォークの状態のことで，
|
|
|
26 pid が1の人の右側にあるフォークが List の最初にあり，
|
|
|
27 pid が1の人の左側にあるフォーク，すなわち pid が2の人の右側にあるフォークが
|
|
|
28 その次の List に格納されていくようになっている．
|
|
|
29 また，自然数の List になっているが，
|
|
|
30 その場所のフォークがテーブルの上にある場合は自然数の0が，
|
|
|
31 誰かが所持している場合はその人の pid が格納されるようになっている．
|
|
|
32
|
|
|
33 \lstinputlisting[caption= Gears Agdaでの DPP の Data Gear のinit, label=agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced}
|
|
|
34
|
|
|
35 Code \ref{agda-dpp-init}が入力から Data Gear を作成する Code Gear になる．
|
|
|
36 ここでは哲学者の人数を自然数で受け取り，人数分の List Phi と table を一つづつ作成し env を作成している．
|
|
|
37 また，最初の哲学者の状態は思考することであるため，next-code には C\_thinking を格納している．
|
|
|
38
|
|
|
39 \lstinputlisting[caption= Gears Agdaでの DPP の step 実行, label=agda-dpp-step, firstline=31, lastline=37]{src/agda-dpp-impl.agda.replaced}
|
|
|
40
|
|
|
41 Agda では並列実行を行うことができない．そのため step 単位の実行を一つづつ行うことで
|
|
|
42 並列実行をしていることとする．
|
|
|
43
|
|
|
44 この際に Env にある List Phi の中身を展開しながら一つづつ行動を処理していく．
|
|
|
45
|
|
|
46 \lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced}
|
|
|
47
|
|
|
48 Code \ref{agda-dpp-lfork}が step 実行をした際に哲学者が左側のフォークを取る記述になる．
|
|
|
49
|
|
|
50 左側のフォークを取る際には table の index は pid の次の値になっている．
|
|
|
51 図 \ref{fig:DPP} を見ると直感的に理解ができる．
|
|
|
52
|
|
|
53 最後の哲学者は一番最初のフォークを参照する必要がある．
|
|
|
54 フォークの状態を確認し，値が0である場合はフォークがテーブルの上にあるので
|
|
|
55 それを自分の pid に書き換え left-hand を true に書き換えてフォークを手に持つ
|
|
|
56 フォークの状態が0以外，すなわち他の哲学者がその場所のフォークを取得している場合は
|
|
|
57 状態を変化させずに処理を続ける．
|
|
|
58 このように左のフォークを取る記述をした．
|
|
|
59
|
|
|
60 右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る．
|
|
|
61 比較するべき table の List と哲学者のListは一致しているため，put\_lfork のように最後の哲学者が
|
|
|
62 最初のフォークを参照することもない．
|
|
|
63
|
|
|
64 似たような形で哲学者がフォークを置く putdown-l/rfork を実装した．
|
|
|
65
|
|
|
66 思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている．
|
|
|
67
|
|
7
|
68 \section{Gears Agda によるDPPの検証}
|
|
4
|
69
|
|
|
70 これまでの実装は一般的なDPPの実装であったため、
|
|
|
71 Code / Data Gear の実装であった。
|
|
|
72 ここからは、モデル検査を行うため、Meta Data Gear の定義をし、
|
|
|
73 それの操作を行う Meta Code Gear の実装を行っていく。
|
|
|
74
|
|
5
|
75 以下\coderef{dpp-mdg}がMeta Code Gear の定義になる
|
|
4
|
76
|
|
|
77 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
|
|
5
|
78 \lstinputlisting[caption=Gears Agdaでの DPP モデル検査を行うための Meta Data Gear の定義, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}
|
|
4
|
79
|
|
|
80 この Meta Data Gear の説明をすると、
|
|
|
81 metadataは状態の分岐数を持っておくnum-brunchがある。
|
|
|
82 MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)
|
|
|
83 meta に 前述したmetadataを持っており、
|
|
|
84 他には、deadlockしているかのフラグである deadlock 、
|
|
|
85 最後の2つは後述する際に必要になる。
|
|
|
86 そのstate が step 実行済みなのかのフラグであるis-step、
|
|
|
87 そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている。
|
|
|
88
|
|
|
89 MetaEnv2 は1つのstate である MetaEnv の Listを meta で持てる。
|
|
|
90 加えて今まで実行していた Data Gear を DG で持てる。
|
|
|
91
|
|
|
92 deadlockの検出方法として、状態の分岐数を保存するnum-brunchをmetadataに持つようにした。
|
|
|
93
|
|
|
94 そしてnum-brunchの値が1であるということは、それ以上の状態に移動することができないとして、この状態をdead lockであると定義した。
|
|
|
95
|
|
5
|
96 以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる
|
|
4
|
97
|
|
|
98 複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て
|
|
|
99 deadlockのフラグを立ち上げている。
|
|
|
100
|
|
|
101 % judge-dead-lock-pのソースコードを貼り付ける
|
|
5
|
102 \lstinputlisting[caption=DPP での dead lock を検知する Meta Code Gear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced}
|
|
|
103 % こいつはmetaEnv2を受け取れるように変えないと行けない
|
|
4
|
104
|
|
|
105 ここから前述した通り、State Listを作成する。
|
|
|
106
|
|
|
107 そのまま実行するだけでは無限に実行されるのみで停止しないと思われる。
|
|
|
108 しかし、分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。
|
|
|
109 存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。
|
|
|
110
|
|
|
111 Agdaには2つの record が等しい場合の分岐など存在しないため、
|
|
5
|
112 \coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つづつ一致しているか確認する。
|
|
|
113 こちらはそのまま掲載すると長いので、実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。
|
|
|
114
|
|
|
115 \lstinputlisting[caption=重複しているstateを除外する Meta Code Gear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced}
|
|
|
116 % 手を加えているので詳細は付録を参照するように促す
|
|
|
117
|
|
|
118 MetaEnv2 を受け取ってその中身の state を比較するが、そこまで展開する必要がある。
|
|
|
119 loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている。
|
|
4
|
120
|
|
5
|
121 更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し、次のstateの一致を探索するように記述されている。
|
|
|
122
|
|
|
123 実際にstateの一致を見ているのは22行目のeq-env関数で、一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている
|
|
|
124
|
|
|
125 State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている。
|
|
|
126 その値が一致している場合には別の値を見て、一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。
|
|
|
127 他の値である、lhandやrhandなども同じように記述している。
|
|
|
128
|
|
6
|
129
|
|
5
|
130 これらにて、まだ分岐を見ていない1つのStateの分岐を確かめる。
|
|
4
|
131 発生した分岐を step 実行させる。
|
|
|
132 step実行して作成された state が State Listに存在していないかを確かめる。
|
|
|
133 これを繰り返すことで State Listを作る。
|
|
|
134 State List に存在している全ての state の分岐を見たということは、
|
|
|
135 出現するStateを全て網羅することができたと言える。
|
|
|
136
|
|
|
137 あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる
|
|
|
138
|
|
7
|
139 \section{Gears Agda による live lockの検証方法について}
|
|
4
|
140 live lockとは、状態が変動しているが、その状態はループしており、実行が進んでいないことを指す。
|
|
|
141
|
|
|
142 DPPにて例を上げると、(上の哲学者のフローだと) dead lock が発生するため、フローを変更したとする。それは以下のような動作を追加する。
|
|
|
143 「右手にフォークを持っているが、左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」
|
|
|
144 とする。これで解決すると思われるが、全員が同時に食事をしようとした場合、右手のフォークを取ったり置いたりを永遠に繰り返すことになる。
|
|
|
145 これを live lock という
|
|
|
146
|
|
|
147 つまり、この状態を検知するなら、そのstateが持っているhistoryまで考慮する必要がある。つまり、今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い。
|
|
|
148
|
|
|
149 history がloopしていた際に、誰もeathingしていない場合を live lock していると定義する。
|
|
|
150
|
|
|
151 今回のはDPPであるためEatingが挙げられているが、他の実装であれば、どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在いしているかを見れば live lock を検知できる。
|
|
|
152
|
|
|
153
|
|
7
|
154 \section{Gears Agda でのモデル検査の評価}
|
|
4
|
155
|
|
|
156 SPINで行ったDPPのモデル検査に比べると、Gears Agdaの方が制約が多いため難解に思える。しかし、Gears Agda ではプログラムの実装も含んでいる。
|
|
|
157
|
|
|
158 さらに、Gears Agda での実装をしたあとのモデル検査を行う際の Meta Code Gear の流れは変化しないため、比較的容易であると言える。
|
|
|
159
|
|
|
160 加えて、Gears Agda は CbC へコンパイルされ、高速に実行されることを踏まえると、いかに Gears Agda が検証に向いたプログラムであるか理解できる。
|
|
|
161
|
|
|
162 % この評価の話はまとめでしたほうがいいかもね？
|
