|
22
|
1 ---
|
|
|
2 marp: true
|
|
|
3 title: Gears Agda での形式手法を用いたプログラムの検証
|
|
|
4 paginate: true
|
|
|
5
|
|
|
6 theme: default
|
|
|
7 size: 16:9
|
|
|
8 style: |
|
|
|
9 section {
|
|
|
10 background-color: #FFFFFF;
|
|
|
11 font-size: 28px;
|
|
|
12 color: #4b4b4b;
|
|
|
13 font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN";
|
|
|
14 background-image: url("logo.svg");
|
|
|
15 background-position: right 3% bottom 2%;
|
|
|
16 background-repeat: no-repeat;
|
|
|
17 background-attachment: 5%;
|
|
|
18 background-size: 20% auto;
|
|
|
19 }
|
|
|
20
|
|
|
21 section.title h1 {
|
|
|
22 color: #808db5;
|
|
|
23 text-align: center;
|
|
|
24 }
|
|
|
25
|
|
|
26 section.title p {
|
|
|
27 bottom: 25%;
|
|
|
28 width: 100%;
|
|
|
29 position: absolute;
|
|
|
30 font-size: 25px;
|
|
|
31 color: #4b4b4b;
|
|
|
32 background: linear-gradient(transparent 90%, #ffcc00 0%);
|
|
|
33 }
|
|
|
34
|
|
|
35 section.slide h1 {
|
|
|
36 width: 95%;
|
|
|
37 color: white;
|
|
|
38 background-color: #808db5;
|
|
|
39 position: absolute;
|
|
|
40 left: 50px;
|
|
|
41 top: 35px;
|
|
|
42 }
|
|
|
43
|
|
|
44 section.fig_cg p {
|
|
|
45 top: 300px;
|
|
|
46 text-align: center;
|
|
|
47 }
|
|
|
48
|
|
23
|
49 math: mathjax
|
|
22
|
50 ---
|
|
|
51 <!-- headingDivider: 1 -->
|
|
|
52
|
|
|
53 # Gears Agda での形式手法を用いたプログラムの検証
|
|
|
54 <!-- class: title -->
|
|
|
55
|
|
|
56 Uechi Yuto, 琉球大学
|
|
|
57
|
|
|
58 # 証明を用いてプログラムの信頼性の向上を目指す
|
|
|
59 <!-- class: slide -->
|
|
|
60
|
|
|
61 <!-- 研究目的 -->
|
|
|
62 - プログラムの信頼性を高めることは重要な課題である
|
|
|
63 - 信頼性を高める手法として「モデル検査」や「定理証明」など
|
|
|
64 - 欠点として、実装コストが高い点が挙げられる
|
|
|
65 - プログラムの検証に適した Gears Agda を用いる
|
|
|
66 - これは Agda に CbC の継続の概念を取り入れたもの
|
|
|
67 <!-- Agda は Curru-Howard 対応に基づく関数型言語 -->
|
|
|
68 - Continuation based C (CbC)という言語を当研究室で開発している
|
|
|
69 - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
|
|
|
70 - 本研究では Gears Agda にて定理証明を用いた検証と、モデル検査による検証をする
|
|
|
71
|
|
|
72 # Agda の基本
|
|
|
73 - Agdaとは定理証明支援器であり、関数型言語
|
|
|
74 - Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
|
|
|
75 - 型の定義部分で、入力と出力の型を定義できる
|
|
|
76 - input → output のようになる
|
|
|
77 - 関数の定義は = を用いて行う
|
|
|
78 - 関数名を定義した行よりも後ろの行で実装する
|
|
|
79 - = の前で受け取る引数を記述、= の後ろで実装を記述する
|
|
|
80
|
|
23
|
81 <!--
|
|
22
|
82 ```
|
|
|
83 sample : (A : Set ) → (B : Set ) → Set
|
|
|
84 sample a b = b
|
|
|
85 ```
|
|
|
86
|
|
|
87
|
|
|
88 # Agda の基本 record
|
|
|
89 オブジェクトあるいは構造体
|
|
|
90 ```
|
|
|
91 record Env : Set where
|
|
|
92 field
|
|
|
93 varn : N
|
|
|
94 vari : N
|
|
|
95 open Env
|
|
|
96 ```
|
|
|
97
|
|
|
98 型に対応する値の導入(intro)
|
|
|
99 ```
|
|
|
100 record {varn = zero ; vari = suc zero}
|
|
|
101 ```
|
|
|
102 record の値のアクセス(elim)
|
|
|
103 ```
|
|
|
104 (env : Env) → varn env
|
|
|
105 ```
|
|
23
|
106 -->
|
|
|
107
|
|
|
108 # Agda の基本 record
|
|
|
109 オブジェクトあるいは構造体
|
|
|
110 2つのものが同時に存在すること
|
|
|
111 ```
|
|
|
112 record _∧_ (A B : Set) : Set where
|
|
|
113 field
|
|
|
114 p1 : A
|
|
|
115 p2 : B
|
|
|
116 ```
|
|
|
117 ３段論法を示すこともできる
|
|
|
118 ```
|
|
|
119 syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
|
|
|
120 syllogism x a = _∧_.p2 x (_∧_.p1 x a)
|
|
|
121 ```
|
|
|
122
|
|
|
123 # CbC について
|
|
|
124 - CbCとは当研究室で開発しているC言語の下位言語
|
|
|
125 - 関数呼び出し時にスタックの操作を行わずjmp命令で次の処理に移動する
|
|
|
126 - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
|
|
|
127 - CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う
|
|
|
128
|
|
|
129 # Normal level と Meta Level を用いた信頼性の向上
|
|
|
130 プログラムを記述する際に、メモリ管理、スレッド管理、資源管理などのプログラムの本筋とは別に実装が必要な場合がある。これらの計算をメタ計算と呼ぶ。
|
|
|
131 CbC では メタ計算を分離して考える。メタ計算以外を Normal levelとしている。
|
|
|
132 - Normal Level の計算
|
|
|
133 - 軽量継続
|
|
|
134 - Code Gear 単位で関数型プログラミングとなる
|
|
|
135 - atomic(Code Gear 自体の実行は割り込まれない)
|
|
|
136 - Meta Level の計算
|
|
|
137 - メモリやCPUなどの資源管理、ポインタ操作
|
|
|
138 - Contextによる並列実行。monadに相当するData構造
|
|
|
139 - Hoare Condition と証明
|
|
22
|
140
|
|
|
141
|
|
23
|
142 # Normal level と Meta Level の対応
|
|
|
143 
|
|
|
144 Gears Agdaでは 検証を Meta計算として取り扱う
|
|
22
|
145
|
|
|
146 # Gears Agda の記法
|
|
|
147 <!-- Gears Agdaの説明が必要かも -->
|
|
|
148 Gears Agda では CbC と対応させるためにすべてLoopで記述する
|
|
|
149 loopは`→ t`の形式で表現する
|
|
|
150 末尾再帰以外の再帰呼び出しは使わない(構文的には禁止していないので注意が必要)
|
|
|
151 ```
|
|
|
152 {-# TERMINATING #-}
|
|
|
153 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
|
|
|
154 whileLoop env next with lt 0 (varn env)
|
|
|
155 whileLoop env next | false = next env
|
|
23
|
156 whileLoop env next | true = whileLoop
|
|
|
157 (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
22
|
158 ```
|
|
|
159 - tを返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
|
|
|
160 - tail call により light weight continuation を定義している
|
|
|
161
|
|
|
162
|
|
|
163 # Gears Agda と Gears CbC の対応
|
|
|
164 Gears Agda
|
|
|
165 - 証明向きの記述
|
|
|
166 - Hoare Condition を含む
|
|
|
167
|
|
|
168 Gears CbC
|
|
|
169 - 実行向きの記述
|
|
|
170 - メモリ管理, 並列実行を含む
|
|
|
171
|
|
|
172 Context
|
|
|
173 - processに相当する
|
|
|
174 - Code Gear 単位で並列実行
|
|
|
175
|
|
|
176
|
|
|
177
|
|
|
178 # Gears Agda と Hoare Logic
|
|
|
179 <!-- class: slide -->
|
|
23
|
180 - C.A.R Hoare, R.W Floyd が考案
|
|
|
181 - 「プログラムの事前条件(P)が成立しているとき、コマンド(C)を実行して停止すると事後条件(Q)が成り立つ」というもの
|
|
|
182 $$ \{P\} C \{Q\} $$
|
|
|
183 - 事前条件を Code Gear に入れる前の Meta Gear で検証する。これを Pre Condition とする
|
|
|
184 - Command は Code Gear そのもの
|
|
|
185 - 事後条件を Code Gear のあとの Meta Gear で検証する。これを Post Condition とした
|
|
|
186 - 今回は、例として While loop の Hoare Logic を用いた検証を行う
|
|
22
|
187
|
|
23
|
188 <!--
|
|
22
|
189 Gears Agda による Command の例
|
|
23
|
190
|
|
22
|
191 ```
|
|
|
192 {-# TERMINATING #-}
|
|
|
193 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
|
|
|
194 whileLoop env next with lt 0 (varn env)
|
|
|
195 whileLoop env next | false = next env
|
|
|
196 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
|
197 ```
|
|
23
|
198 -->
|
|
|
199
|
|
|
200 # Gears Agda での while loopの実装
|
|
|
201 While Loopの実装は主に以下のDataGearとCodeGearで行った
|
|
|
202 ```
|
|
|
203 record Env : Set where
|
|
|
204 field
|
|
|
205 varn : ℕ -- これからループする回数
|
|
|
206 vari : ℕ -- 今までループした回数
|
|
|
207 open Env
|
|
|
208 ```
|
|
|
209
|
|
|
210 ```
|
|
|
211 {-# TERMINATING #-}
|
|
|
212 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
|
|
|
213 whileLoop env next with lt 0 (varn env)
|
|
|
214 whileLoop env next | false = next env
|
|
|
215 whileLoop env next | true =
|
|
|
216 whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
|
217 ```
|
|
|
218
|
|
|
219 # While loopでのInvariantの定義
|
|
|
220
|
|
|
221 不変条件としてInvariantを定義した。これを実行しながら証明することでHoare Logic での検証ができる
|
|
|
222 ```
|
|
|
223 -- 初期値として、ループする前はループした回数は0であり
|
|
|
224 -- かつループする回数とループする回数は等しい
|
|
|
225 ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
|
|
|
226 ```
|
|
|
227 ```
|
|
|
228 -- ループする回数とループした回数を足すと入力したループして欲しい回数と等しい
|
|
|
229 (varn env) + (vari env) ≡ c10)
|
|
|
230 ```
|
|
|
231 ```
|
|
|
232 vari e1 ≡ c10 -- ループした回数は入力したループして欲しい回数と等しい
|
|
|
233 ```
|
|
22
|
234
|
|
|
235 # Gears Agda の Pre Condition / Post Condition
|
|
23
|
236 ループ実行中の命題は以下のようになる。
|
|
22
|
237 ```
|
|
|
238 whileLoopSeg : {l : Level} {t : Set l} → {c10 : N } → (env : Env) → (varn env + vari env ≡ c10)
|
|
|
239 → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)
|
|
|
240 → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
|
|
|
241 ```
|
|
|
242 - `{-# TERMINATING #-}`を避けるためにloopを分割
|
|
|
243 - `varn env + vari env ≡ c10` が Pre Condition
|
|
|
244 - `varn e1 + vari e1 ≡ c10` が Post Condition
|
|
|
245 - `varn e1 < varn env` が停止を保証する減少列
|
|
|
246
|
|
|
247 これは命題なので証明を与えて Pre Condition から Post Condition を導出する必要がある。証明は値として次の CodeGear に渡される
|
|
|
248
|
|
|
249 # Loop の接続
|
|
23
|
250 loop中のMeta Gearを作成する
|
|
22
|
251 ```
|
|
|
252 TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set )
|
|
|
253 → {Invraiant : Index → Set } → ( reduce : Index → N)
|
|
|
254 → (loop : (r : Index) → Invraiant r
|
|
|
255 → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t)
|
|
|
256 → (r : Index) → (p : Invraiant r) → t
|
|
|
257 ```
|
|
|
258 - IndexはLoop変数
|
|
|
259 - Invariantはloop変数の不変条件
|
|
|
260 - loopに接続するCode Gearを与える
|
|
23
|
261 - つまりloopを抜ける際の Code Gear。ここでは next がそれにあたる
|
|
22
|
262 - reduceは停止性を保証する減少列
|
|
23
|
263 - この減少列のおかげで`{-# TERMINATING #-}`が外せる
|
|
22
|
264
|
|
|
265 これを証明することで検証ができる
|
|
|
266
|
|
|
267 # 実際のloopの接続
|
|
|
268 証明したい性質を以下のように記述する
|
|
|
269 ```
|
|
|
270 whileTestSpec1 : (c10 : N) → (e1 : Env ) → vari e1 ≡ c10 → ⊤
|
|
|
271 whileTestSpec1 _ _ x = tt
|
|
|
272 ```
|
|
|
273 loopをTerminatingLoopSで接続して仕様記述に繋げる
|
|
|
274 ```
|
|
|
275 proofGearsTermS : {c10 : N} → ⊤
|
|
|
276 proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 →
|
|
|
277 TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop
|
|
|
278 (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 ))
|
|
|
279 ```
|
|
|
280 - conversion1はPre Condition をPost Conditionに変換する
|
|
23
|
281 - ⊤は正しいことを示す論理記号
|
|
|
282
|
|
22
|
283
|
|
23
|
284 # 定理証明とtest との違い
|
|
|
285 - test では実値を与えた際の出力が仕様に沿ったものであるかを検証する
|
|
|
286 - コーナーケースを人力で完全に考慮するのは難しい
|
|
|
287 - 今回の定理証明を用いた証明では実値を必要としない
|
|
22
|
288 - そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる
|
|
|
289
|
|
|
290 # モデル検査と定理証明の違い
|
|
|
291 - モデル検査では全ての状態を網羅し、それが仕様を満たしているか検証する
|
|
|
292 - 無限にある状態を検証することはできないため、定理証明と比べると完全な検証にならないこともある
|
|
23
|
293 - 定理証明に比べてモデル検査の実装コストは低い
|
|
|
294 - 定理証明の証明は難しい
|
|
|
295 - その代わりモデル検査は計算コストは高い
|
|
|
296 - 定理証明では並列実行の検証をするには、状態を全探索しそれらを定理証明することになる
|
|
|
297
|
|
|
298 # Gears Agda による モデル検査
|
|
|
299 - 定理証明で並列実行の検証をするのは難しいので、モデル検査で検証を行う。
|
|
|
300 - 今回は Gears Agda にてモデル検査をすることで、並列実行の検証を行う
|
|
|
301 - 題材として、 Dining Philosophers Problem のモデル検査にてdead lockを検知する
|
|
22
|
302
|
|
|
303 # Dining Philosophers Problem
|
|
|
304 ||哲学者の遷移|
|
|
|
305 |---|---|
|
|
23
|
306 ||制約 <br> - 哲学者と同じ数のフォークが存在する <br> - 両手にフォークを持つと食事できる <br> 哲学者のフロー <br> 1. 哲学者は思考をしている <br> 2. 食事をするために右のフォークを取る <br> 3. 次に左のフォークを取る <br> 4. 両方のフォークが取れたら食事をする <br> 5. 思考に戻るために左のフォークを置く <br> 6. 次に右のフォークを置く |
|
|
22
|
307
|
|
|
308 # Dining Philosophers Problem の実装
|
|
|
309 - DPPはマルチプロセスの同期問題である
|
|
|
310 - しかし、Agdaでは並列実行をサポートしていないため、step実行毎に一つずつ処理することで並列実行を表現している
|
|
|
311 - 加えて、哲学者が思考を止めて食事をしようとするのか、食事中に思考に戻ろうとするのかで分岐が発生する
|
|
|
312 - 今回はその状態に対して網羅することでモデル検査を行っている
|
|
|
313
|
|
|
314 # Dining Philosophers Problem の実装
|
|
|
315 Gears Agdaで使用する Data Gear を以下のように定義した
|
|
|
316 ```
|
|
|
317 record Phi : Set where
|
|
|
318 field
|
|
|
319 pid : ℕ
|
|
|
320 right-hand : Bool
|
|
|
321 left-hand : Bool
|
|
|
322 next-code : Code
|
|
|
323 open Phi
|
|
|
324 ```
|
|
|
325 ```
|
|
|
326 record Env : Set where
|
|
|
327 field
|
|
|
328 table : List ℕ
|
|
|
329 ph : List Phi
|
|
|
330 open Env
|
|
|
331 ```
|
|
|
332
|
|
|
333 # Dining Philosophers Problem の実装
|
|
|
334 ```
|
|
|
335 data Code : Set where
|
|
|
336 C_putdown_rfork : Code
|
|
|
337 C_putdown_lfork : Code
|
|
|
338 C_thinking : Code
|
|
|
339 C_pickup_rfork : Code
|
|
|
340 C_pickup_lfork : Code
|
|
|
341 C_eating : Code
|
|
|
342 ```
|
|
|
343
|
|
23
|
344 ```
|
|
22
|
345 code_table : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t
|
|
|
346 code_table C_putdown_rfork = putdown-rfork-c
|
|
|
347 code_table C_putdown_lfork = putdown-lfork-c
|
|
|
348 code_table C_thinking = thinking-c
|
|
|
349 code_table C_pickup_rfork = pickup-rfork-c
|
|
|
350 code_table C_pickup_lfork = pickup-lfork-c
|
|
|
351 code_table C_eating = eating-c
|
|
|
352 ```
|
|
|
353
|
|
|
354 # Dining Philosophers Problem の実装
|
|
|
355 以下が哲学者の動作の実装の一つ
|
|
|
356 ```
|
|
|
357 pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
|
|
|
358 pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where
|
|
|
359 pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
|
|
|
360 pickup-lfork-p zero f [] p env exit with table env
|
|
|
361 ... | [] = exit env
|
|
|
362 ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ;
|
|
|
363 next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)}
|
|
|
364 ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])}
|
|
|
365 pickup-lfork-p zero f (0 ∷ ts) p env exit = exit record env{
|
|
|
366 ph = ((ph env) ++ (record p{left-hand = true ;
|
|
|
367 next-code = C_eating} ∷ [])); table = (f ++ ((pid p) ∷ ts))}
|
|
|
368 ```
|
|
|
369
|
|
|
370 # モデル検査でのデッドロック検知
|
|
|
371 - 今回Gears Agdaでのデッドロックの定義として、以下2つを設定した
|
|
|
372 - その状態から分岐が作れない
|
|
23
|
373 - ThinkingやEathingのときに乱数が出るので、その際に分岐するようにしている。それがないということ
|
|
|
374 - step実行時に状態が一切変化しない
|
|
|
375 - Gears Agda にて出現する状態を全て網羅する
|
|
|
376 - step 実行を無限に続ける
|
|
|
377 - 一度分岐を確認した状態に対しては flag を立てる
|
|
|
378 - 全ての状態の分岐を確認したら停止し、これを State List とした
|
|
|
379 - これで全ての状態に対して dead Lock しているのか検証する
|
|
|
380
|
|
|
381 # モデル検査での Meta Data Gear
|
|
|
382 以下の Meta Data Gear を定義した
|
|
|
383 ```
|
|
|
384 record metadata : Set where
|
|
|
385 field
|
|
|
386 num-branch : ℕ -- その状態から発生する分岐の数
|
|
|
387 wait-list : List ℕ -- step実行で変化がなかったプロセス
|
|
|
388 open metadata
|
|
|
389 ```
|
|
|
390 ```
|
|
|
391 record MetaEnv : Set where
|
|
|
392 field
|
|
|
393 DG : List Env -- historyを持つためListにしている
|
|
|
394 meta : metadata
|
|
|
395 deadlock : Bool
|
|
|
396 is-done : Bool
|
|
|
397 is-step : Bool
|
|
|
398 open MetaEnv
|
|
|
399 ```
|
|
|
400
|
|
|
401 # モデル検査での Meta Data Gear
|
|
|
402 ```
|
|
|
403 record MetaEnv2 : Set where
|
|
|
404 field
|
|
|
405 DG : List (List Env) -- HistoryをもったEnv(状態)を配列として複数持っている。
|
|
|
406 metal : List MetaEnv
|
|
|
407 open MetaEnv2
|
|
|
408 ```
|
|
22
|
409
|
|
|
410 # モデル検査でのデッドロック検知
|
|
23
|
411 網羅には以下の Meta CodeGear を実装した
|
|
|
412 ```
|
|
|
413 check-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
|
|
|
414 check-deadlock-metaenv meta2 exit = search-brute-force-envll-p [] (metal meta2)
|
|
|
415 (λ e → exit record meta2{metal = e}) where
|
|
|
416 search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv))
|
|
|
417 → (exit : List (MetaEnv) → t) → t
|
|
|
418 search-brute-force-envll-p f [] exit = exit f
|
|
|
419 search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv
|
|
|
420 ... | [] = search-brute-force-envll-p f bs exit
|
|
|
421 ... | (env ∷ envs) = brute-force-search env (λ e0 → search-brute-force-envll-p
|
|
|
422 (f ++ ( record metaenv{meta = record (meta metaenv)
|
|
|
423 {num-branch = (length e0)} } ∷ [])) bs exit )
|
|
|
424 ```
|
|
|
425 step実行しても状態が変更しない Meta Code Gear も同じように実装している。
|
|
|
426 これで meta データ を定義できるようになった。
|
|
|
427
|
|
|
428
|
|
|
429 # モデル検査でのデッドロックの検知
|
|
|
430 metaデータから deadlock を検出する Meta Code Gear にて 、モデル検査を Gears Agda にて行えるようになった。
|
|
|
431
|
|
22
|
432 ```
|
|
23
|
433 judge-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
|
|
|
434 judge-deadlock-metaenv meta2 exit = judge-deadlock-p [] (metal meta2)
|
|
|
435 (λ e → exit record meta2{metal = e} ) where
|
|
|
436 judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv))
|
|
|
437 → (exit : List (MetaEnv) → t) → t
|
|
|
438 judge-deadlock-p f [] exit = exit f
|
|
|
439 judge-deadlock-p f (metaenv ∷ bs) exit with num-branch (meta metaenv)
|
|
|
440 ... | suc (suc branchnum) = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
|
|
|
441 ... | zero = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
|
|
|
442 ... | suc zero with (DG metaenv )
|
|
|
443 ... | [] = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
|
|
|
444 ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p))
|
|
|
445 ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
|
|
|
446 ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
|
|
|
447 ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit
|
|
22
|
448 ```
|
|
|
449
|
|
23
|
450 # Gears Agda でのモデル検査の実行
|
|
|
451 以下の関数にてモデル検査を行うことができる
|
|
|
452 ```
|
|
|
453 {-# TERMINATING #-}
|
|
|
454 test-dead-lock-loop2 : MetaEnv2 → MetaEnv2
|
|
|
455 test-dead-lock-loop2 metaenv2 = branch-search-meta2 metaenv2
|
|
|
456 (λ me2 → step-meta2 me2
|
|
24
|
457 (λ me3 → exclude-same-env me3 metaenv2
|
|
23
|
458 (λ me4 → test-dead-lock-loop2 me4) ) )
|
|
|
459 (λ e → check-and-judge-deadlock e (λ e1 → e1) )
|
|
|
460 ```
|
|
|
461 <!-- initから投げるまでにした方がいいかもしれないな -->
|
|
|
462
|
|
|
463 - Code Gear を繋げたものでは、Agdaは停止性を理解できないので、`{-# TERMINATING #-}`を使用してちゃんと止まることを記述している。
|
|
|
464 - 今回の DPP の状態は有限であることが予めわかっていたから可能だった
|
|
|
465 - 状態爆発が起こったり無限にある場合は、範囲を制限してモデル検査する方法が用いられる (bounded model checking)
|
|
|
466
|
|
22
|
467 # 今後の研究方針
|
|
|
468 - モデル検査
|
|
|
469 - 有向グラフからなる有限オートマトンの遷移を全自動探索する
|
|
|
470 - live lock の検出や LTTL も用いたアサーションなどの検証
|
|
24
|
471 - State List のデータ構造を balanced tree にする
|
|
22
|
472 - モデル検査に定理証明を組み込む
|
|
|
473 - 定理証明
|
|
|
474 - Red Black Tree の検証を行う
|
|
|
475 - Gears Agda
|
|
|
476 - Gears Agda を CbC に自動変換できるようにする
|
|
|
477
|
|
|
478
|
|
|
479 # まとめ
|
|
|
480 - 定理証明について、Invariant によるプログラムの検証を行うことができるようになった
|
|
|
481
|
|
|
482 - Gears Agda によるモデル検査により、並列動作の検証を行えるようになった
|
|
|
483
|
|
|
484 <!-- 英語版も欲しい--> |
