Mercurial > hg > Papers > 2023 > soto-master

changeset 26:abde7ffd6011

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add lt slide
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sat, 11 Feb 2023 22:51:00 +0900
parents 83e28d9da152
children 7ce3db013350
files Paper/master_paper.dvi Paper/master_paper.fdb_latexmk Paper/master_paper.log Paper/master_paper.pdf Paper/master_paper.sty Paper/master_paper.synctex.gz slide/lt.md
diffstat 7 files changed, 503 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
Binary file Paper/master_paper.dvi has changed
--- a/Paper/master_paper.fdb_latexmk	Sat Feb 11 22:49:20 2023 +0900
+++ b/Paper/master_paper.fdb_latexmk	Sat Feb 11 22:51:00 2023 +0900
@@ -1,17 +1,17 @@
 # Fdb version 3
-["bibtex master_paper"] 1675432991 "master_paper.aux" "master_paper.bbl" "master_paper" 1675432993
+["bibtex master_paper"] 1675432991 "master_paper.aux" "master_paper.bbl" "master_paper" 1676115609
   "junsrt.bst" 0 -1 0 ""
-  "master_paper.aux" 1675432993 19572 0389835a9786a06fbd1766a61cfb8e10 "latex"
+  "master_paper.aux" 1676115608 19572 0389835a9786a06fbd1766a61cfb8e10 "latex"
   "reference.bib" 1675336779 4441 cbcfa8f3c6c78deaf589b09a84f57dc9 ""
   (generated)
   "master_paper.bbl"
   "master_paper.blg"
-["dvipdf"] 1675432993 "master_paper.dvi" "master_paper.pdf" "master_paper" 1675432993
-  "master_paper.dvi" 1675432993 322416 abfb2d9adc3484e7ae5336c2db6915f3 "latex"
+["dvipdf"] 1676115608 "master_paper.dvi" "master_paper.pdf" "master_paper" 1676115609
+  "master_paper.dvi" 1676115608 322892 d5e1d20746c038537134b70cd2d318bb "latex"
   (generated)
   "master_paper.pdf"
-["latex"] 1675432991 "/home/soto/lab/soto-master/Paper/master_paper.tex" "master_paper.dvi" "master_paper" 1675432993
-  "/home/soto/lab/soto-master/Paper/master_paper.tex" 1675417607 3097 65f21be5c4f1e0234a8f6ffd26dbeafa ""
+["latex"] 1676115607 "/home/soto/lab/soto-master/Paper/master_paper.tex" "master_paper.dvi" "master_paper" 1676115609
+  "/home/soto/lab/soto-master/Paper/master_paper.tex" 1676115607 3097 65f21be5c4f1e0234a8f6ffd26dbeafa ""
   "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1650183167 3524 cb3e574dea2d1052e39280babc910dc8 ""
   "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/tcrm1200.tfm" 1650183167 1536 74b7293ec3713bb7fdca8dd1bd1f469c ""
   "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/tctt1000.tfm" 1650183167 1536 c5729d01ab121276cf99b309129349a0 ""
@@ -128,22 +128,22 @@
   "fig/dpp-model.pdf" 1674369845 54353 01b0af963c00cb0c2721ab5a1d2bc781 ""
   "fig/rbt-stack.pdf" 1674125175 35233 d7920c7c7df9157f95299a7f4e75eab1 ""
   "fig/u-ryukyu-Mark.eps" 1674125175 177171 82fa7968c81a6b7289de9d1085964fe1 ""
-  "master_paper.aux" 1675432993 19572 0389835a9786a06fbd1766a61cfb8e10 "latex"
+  "master_paper.aux" 1676115608 19572 0389835a9786a06fbd1766a61cfb8e10 "latex"
   "master_paper.bbl" 1675432991 3042 1f8e88c721c88589fe6b356911ae236d "bibtex master_paper"
-  "master_paper.lof" 1675432993 629 bb98eadca704b5d48a03911c72cf03e2 "latex"
-  "master_paper.lol" 1675432993 4682 ee5355881ee488a771f0e7774cbca43d "latex"
-  "master_paper.out" 1675432993 8014 752f2940cbc6f3216306fde56a77d4ef "latex"
-  "master_paper.sty" 1675417772 13216 984eba3376324a0ce8eefb51796ff866 ""
-  "master_paper.tex" 1675417607 3097 65f21be5c4f1e0234a8f6ffd26dbeafa ""
-  "master_paper.toc" 1675432993 3910 500a0fc084c1fda6fc35b24ae13c676a "latex"
+  "master_paper.lof" 1676115608 629 bb98eadca704b5d48a03911c72cf03e2 "latex"
+  "master_paper.lol" 1676115608 4682 ee5355881ee488a771f0e7774cbca43d "latex"
+  "master_paper.out" 1676115608 8014 752f2940cbc6f3216306fde56a77d4ef "latex"
+  "master_paper.sty" 1676115605 13232 506750f1706ac71feedc33ce08dea99b ""
+  "master_paper.tex" 1676115607 3097 65f21be5c4f1e0234a8f6ffd26dbeafa ""
+  "master_paper.toc" 1676115608 3910 500a0fc084c1fda6fc35b24ae13c676a "latex"
   "src/agda-dpp-impl.agda.replaced" 1675358521 2824 60454fbbf20d18849d1886385e94384b ""
   "src/agda-term3.agda.replaced" 1675358515 545 44ab43e2fe263959526d8b27411b6b81 ""
   "src/agda/And.agda.replaced" 1675358518 74 04fb41b7bb7a82a71ad4722821fb7177 ""
-  "src/agda/Nat.agda.replaced" 1675432437 116 07a41429bdde1dc47d3c66af9f69f91e ""
+  "src/agda/Nat.agda.replaced" 1675582383 117 9f9ba563076ef0d3edd10e2c2dd037cb ""
   "src/agda/abridgement.agda.replaced" 1675358518 545 2c7399d5b35681da89289c89fd9d172f ""
   "src/agda/cbc-agda.agda.replaced" 1675358518 1143 ab39102eb0f69d3b9f8e4e985a7c1e37 ""
   "src/agda/plus.agda.replaced" 1675358518 131 02cc3ce23c67c850a18782de80b72708 ""
-  "src/agda/plus2.agda.replaced" 1675432523 151 8208961eb70fd6fee1108760f1208768 ""
+  "src/agda/plus2.agda.replaced" 1675582383 170 98245cb6f75325de135bf175f2b2f356 ""
   "src/agda/syllogism.agda.replaced" 1675358518 193 37bc8bff0ac10305e5bdf929856897e5 ""
   "src/bt_impl/bt_env.agda.replaced" 1675358515 353 1c4e0e30a709998b56db02c2f5d79780 ""
   "src/bt_impl/find.agda.replaced" 1675358515 1009 ee258753faf846ae2bf560ebad44102a ""
--- a/Paper/master_paper.log	Sat Feb 11 22:49:20 2023 +0900
+++ b/Paper/master_paper.log	Sat Feb 11 22:51:00 2023 +0900
@@ -1,4 +1,4 @@
-This is e-upTeX, Version 3.141592653-p4.0.0-u1.28-220214-2.6 (utf8.uptex) (TeX Live 2022/Arch Linux) (preloaded format=uplatex 2022.11.28)  3 FEB 2023 23:03
+This is e-upTeX, Version 3.141592653-p4.0.0-u1.28-220214-2.6 (utf8.uptex) (TeX Live 2022/Arch Linux) (preloaded format=uplatex 2022.11.28)  11 FEB 2023 20:40
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -647,10 +647,10 @@
 Here is how much of TeX's memory you used:
  16732 strings out of 478689
  253685 string characters out of 5861063
- 1442008 words of memory out of 5000000
+ 1442015 words of memory out of 5000000
  34816 multiletter control sequences out of 15000+600000
  520406 words of font info for 134 fonts, out of 8000000 for 9000
  929 hyphenation exceptions out of 8191
  60i,12n,64p,954b,2407s stack positions out of 5000i,500n,10000p,200000b,80000s
 
-Output written on master_paper.dvi (49 pages, 322416 bytes).
+Output written on master_paper.dvi (49 pages, 322892 bytes).
Binary file Paper/master_paper.pdf has changed
--- a/Paper/master_paper.sty	Sat Feb 11 22:49:20 2023 +0900
+++ b/Paper/master_paper.sty	Sat Feb 11 22:51:00 2023 +0900
@@ -107,7 +107,7 @@
 \def\euniversity{University of the Ryukyus}
 
 % 所属
-\def\department{大学院理工学研究科}
+\def\department{大学院理工学研究科 \\ 工学専攻}
 \def\edepartment{Graduate School of Engineering and Science}
 
 % 専攻
Binary file Paper/master_paper.synctex.gz has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide/lt.md	Sat Feb 11 22:51:00 2023 +0900
@@ -0,0 +1,484 @@
+---
+marp: true
+title: Gears Agda での形式手法を用いたプログラムの検証
+paginate: true
+
+theme: default
+size: 16:9
+style: |
+  section {
+    background-color: #FFFFFF;
+    font-size: 28px;
+    color: #4b4b4b;
+    font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN";
+    background-image: url("logo.svg");
+    background-position: right 3% bottom 2%;
+    background-repeat: no-repeat;
+    background-attachment: 5%;
+    background-size: 20% auto;
+  }
+  
+    section.title h1 {
+      color: #808db5;
+      text-align: center;
+      }
+    
+    section.title p {
+        bottom: 25%;
+        width: 100%;
+        position: absolute;
+        font-size: 25px;
+        color: #4b4b4b;
+        background: linear-gradient(transparent 90%, #ffcc00 0%);
+    }
+
+  section.slide h1 {
+      width: 95%;
+      color: white;
+      background-color: #808db5;
+      position: absolute;
+      left: 50px; 
+      top: 35px;
+  }
+
+  section.fig_cg p {
+     top: 300px;
+     text-align: center;
+  }
+
+math: mathjax
+---
+<!-- headingDivider: 1 -->
+
+# Gears Agda での形式手法を用いたプログラムの検証
+<!-- class: title -->
+
+Uechi Yuto, 琉球大学
+
+# 証明を用いてプログラムの信頼性の向上を目指す
+<!-- class: slide -->
+
+<!-- 研究目的 -->
+- プログラムの信頼性を高めることは重要な課題である
+  - 信頼性を高める手法として「モデル検査」や「定理証明」など
+  - 欠点として、実装コストが高い点が挙げられる
+- プログラムの検証に適した Gears Agda を用いる
+    - これは Agda に CbC の継続の概念を取り入れたもの
+    <!-- Agda は Curru-Howard 対応に基づく関数型言語 -->
+- Continuation based C (CbC)という言語を当研究室で開発している
+  - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
+- 本研究では Gears Agda にて定理証明を用いた検証と、モデル検査による検証をする
+
+# Agda の基本 
+- Agdaとは定理証明支援器であり、関数型言語
+- Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
+- 型の定義部分で、入力と出力の型を定義できる
+  -  input → output のようになる
+- 関数の定義は = を用いて行う
+  - 関数名を定義した行よりも後ろの行で実装する
+  - = の前で受け取る引数を記述、= の後ろで実装を記述する
+
+<!--
+```
+sample : (A : Set ) → (B : Set ) → Set
+sample a b = b
+```
+
+
+# Agda の基本 record
+オブジェクトあるいは構造体
+```
+record Env  : Set where
+  field
+    varn : N
+    vari : N
+open Env
+```
+
+型に対応する値の導入(intro)
+```
+record {varn = zero ; vari = suc zero}
+```
+record の値のアクセス(elim)
+```
+(env : Env) → varn env
+```
+-->
+
+# Agda の基本 record
+オブジェクトあるいは構造体
+2つのものが同時に存在すること
+```
+record _∧_ (A B : Set) : Set where
+  field
+    p1 : A
+    p2 : B
+```
+３段論法を示すこともできる
+```
+syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
+syllogism x a = _∧_.p2 x (_∧_.p1 x a)
+```
+
+# CbC について
+- CbCとは当研究室で開発しているC言語の下位言語
+    - 関数呼び出し時にスタックの操作を行わずjmp命令で次の処理に移動する
+    - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
+- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う
+
+# Normal level と Meta Level を用いた信頼性の向上
+プログラムを記述する際に、メモリ管理、スレッド管理、資源管理などのプログラムの本筋とは別に実装が必要な場合がある。これらの計算をメタ計算と呼ぶ。
+CbC では メタ計算を分離して考える。メタ計算以外を Normal levelとしている。
+- Normal Level の計算
+  - 軽量継続
+  - Code Gear 単位で関数型プログラミングとなる
+  - atomic(Code Gear 自体の実行は割り込まれない)
+- Meta Level の計算
+  - メモリやCPUなどの資源管理、ポインタ操作
+  - Contextによる並列実行。monadに相当するData構造
+  - Hoare Condition と証明
+
+
+# Normal level と Meta Level の対応
+![height:400px](meta-cg-dg.jpg)
+Gears Agdaでは 検証を Meta計算として取り扱う
+
+# Gears Agda の記法
+<!-- Gears Agdaの説明が必要かも -->
+Gears Agda では CbC と対応させるためにすべてLoopで記述する
+loopは`→ t`の形式で表現する
+末尾再帰以外の再帰呼び出しは使わない(構文的には禁止していないので注意が必要)
+```
+{-# TERMINATING #-}
+whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true = whileLoop 
+  (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+```
+- tを返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
+- tail call により light weight continuation を定義している
+
+
+# Gears Agda と Gears CbC の対応
+Gears Agda
+- 証明向きの記述
+- Hoare Condition を含む
+
+Gears CbC
+- 実行向きの記述
+- メモリ管理, 並列実行を含む
+
+Context
+- processに相当する
+- Code Gear 単位で並列実行
+
+
+
+# Gears Agda と Hoare Logic
+<!-- class: slide -->
+- C.A.R Hoare, R.W Floyd が考案
+- 「プログラムの事前条件(P)が成立しているとき、コマンド(C)を実行して停止すると事後条件(Q)が成り立つ」というもの
+$$ \{P\} C \{Q\} $$
+- 事前条件を Code Gear に入れる前の Meta Gear で検証する。これを Pre Condition とする 
+- Command は Code Gear そのもの
+- 事後条件を Code Gear のあとの Meta Gear で検証する。これを Post Condition とした
+- 今回は、例として While loop の Hoare Logic を用いた検証を行う
+
+<!--
+Gears Agda による Command の例
+
+```
+{-# TERMINATING #-}
+whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+```
+-->
+
+# Gears Agda での while loopの実装
+While Loopの実装は主に以下のDataGearとCodeGearで行った
+```
+record Env  : Set where
+  field
+    varn : ℕ -- これからループする回数
+    vari : ℕ -- 今までループした回数
+open Env
+```
+
+```
+{-# TERMINATING #-}
+whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true =
+    whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+```
+
+# While loopでのInvariantの定義
+
+不変条件としてInvariantを定義した。これを実行しながら証明することでHoare Logic での検証ができる
+```
+-- 初期値として、ループする前はループした回数は0であり
+-- かつループする回数とループする回数は等しい
+((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+```
+```
+-- ループする回数とループした回数を足すと入力したループして欲しい回数と等しい
+(varn env) + (vari env) ≡ c10)
+```
+```
+vari e1 ≡ c10 -- ループした回数は入力したループして欲しい回数と等しい
+```
+
+# Gears Agda の Pre Condition / Post Condition
+ループ実行中の命題は以下のようになる。
+```
+whileLoopSeg : {l : Level} {t : Set l} → {c10 :  N } → (env : Env) → (varn env + vari env ≡ c10)
+   → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) 
+   → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
+```
+- `{-# TERMINATING #-}`を避けるためにloopを分割
+- `varn env + vari env ≡ c10` が Pre Condition
+- `varn e1 + vari e1 ≡ c10` が Post Condition
+- `varn e1 < varn env` が停止を保証する減少列
+
+これは命題なので証明を与えて Pre Condition から Post Condition を導出する必要がある。証明は値として次の CodeGear に渡される
+
+# Loop の接続
+loop中のMeta Gearを作成する
+```
+TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) 
+  → {Invraiant : Index → Set } → ( reduce : Index → N) 
+  → (loop : (r : Index) → Invraiant r 
+    → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) 
+  → (r : Index) → (p : Invraiant r) → t
+```
+- IndexはLoop変数
+- Invariantはloop変数の不変条件
+- loopに接続するCode Gearを与える
+  - つまりloopを抜ける際の Code Gear。ここでは next がそれにあたる
+- reduceは停止性を保証する減少列
+  - この減少列のおかげで`{-# TERMINATING #-}`が外せる
+
+これを証明することで検証ができる
+
+# 実際のloopの接続
+証明したい性質を以下のように記述する
+```
+whileTestSpec1 : (c10 : N) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
+whileTestSpec1 _ _ x = tt
+```
+loopをTerminatingLoopSで接続して仕様記述に繋げる
+```
+proofGearsTermS : {c10 :  N} → ⊤
+proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
+    TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop 
+    (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 
+```
+- conversion1はPre Condition をPost Conditionに変換する
+- ⊤は正しいことを示す論理記号
+
+
+# 定理証明とtest との違い
+- test では実値を与えた際の出力が仕様に沿ったものであるかを検証する
+    - コーナーケースを人力で完全に考慮するのは難しい
+- 今回の定理証明を用いた証明では実値を必要としない
+    - そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる
+
+# モデル検査と定理証明の違い
+- モデル検査では全ての状態を網羅し、それが仕様を満たしているか検証する
+- 無限にある状態を検証することはできないため、定理証明と比べると完全な検証にならないこともある
+- 定理証明に比べてモデル検査の実装コストは低い
+  - 定理証明の証明は難しい
+  - その代わりモデル検査は計算コストは高い
+- 定理証明では並列実行の検証をするには、状態を全探索しそれらを定理証明することになる
+
+# Gears Agda による モデル検査
+- 定理証明で並列実行の検証をするのは難しいので、モデル検査で検証を行う。
+- 今回は Gears Agda にてモデル検査をすることで、並列実行の検証を行う
+- 題材として、 Dining Philosophers Problem のモデル検査にてdead lockを検知する
+
+# Dining Philosophers Problem
+||哲学者の遷移|
+|---|---|
+|![height:450px](DPP.jpg)|制約 <br> - 哲学者と同じ数のフォークが存在する <br> - 両手にフォークを持つと食事できる <br> 哲学者のフロー <br> 1. 哲学者は思考をしている  <br> 2. 食事をするために右のフォークを取る <br> 3. 次に左のフォークを取る <br> 4. 両方のフォークが取れたら食事をする <br> 5. 思考に戻るために左のフォークを置く <br> 6. 次に右のフォークを置く |
+
+# Dining Philosophers Problem の実装
+- DPPはマルチプロセスの同期問題である
+  - しかし、Agdaでは並列実行をサポートしていないため、step実行毎に一つずつ処理することで並列実行を表現している
+- 加えて、哲学者が思考を止めて食事をしようとするのか、食事中に思考に戻ろうとするのかで分岐が発生する
+  - 今回はその状態に対して網羅することでモデル検査を行っている
+
+# Dining Philosophers Problem の実装
+Gears Agdaで使用する Data Gear を以下のように定義した
+```
+record Phi : Set where
+  field
+    pid : ℕ
+    right-hand : Bool
+    left-hand : Bool
+    next-code : Code
+open Phi
+```
+```
+record Env : Set where
+  field
+    table : List ℕ
+    ph : List Phi
+open Env
+```
+
+# Dining Philosophers Problem の実装
+```
+data Code : Set  where
+   C_putdown_rfork : Code
+   C_putdown_lfork : Code
+   C_thinking : Code
+   C_pickup_rfork : Code
+   C_pickup_lfork : Code
+   C_eating : Code
+```
+
+``` 
+code_table : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t
+code_table C_putdown_rfork = putdown-rfork-c
+code_table C_putdown_lfork = putdown-lfork-c
+code_table C_thinking = thinking-c
+code_table C_pickup_rfork = pickup-rfork-c
+code_table C_pickup_lfork = pickup-lfork-c
+code_table C_eating = eating-c
+```
+
+# Dining Philosophers Problem の実装
+以下が哲学者の動作の実装の一つ
+```
+pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
+pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where
+  pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
+  pickup-lfork-p zero f [] p env exit with table env
+  ... | [] = exit env
+  ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ;
+         next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)}
+  ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])}
+  pickup-lfork-p zero f (0 ∷ ts) p env exit = exit record env{
+    ph = ((ph env) ++ (record p{left-hand = true ;
+         next-code = C_eating} ∷ [])); table = (f ++ ((pid p) ∷ ts))}
+```
+
+# モデル検査でのデッドロック検知
+- 今回Gears Agdaでのデッドロックの定義として、以下2つを設定した
+  - その状態から分岐が作れない
+    - ThinkingやEathingのときに乱数が出るので、その際に分岐するようにしている。それがないということ
+  - step実行時に状態が一切変化しない
+- Gears Agda にて出現する状態を全て網羅する
+  - step 実行を無限に続ける
+  - 一度分岐を確認した状態に対しては flag を立てる
+  - 全ての状態の分岐を確認したら停止し、これを State List とした
+- これで全ての状態に対して dead Lock しているのか検証する
+
+# モデル検査での Meta Data Gear
+以下の Meta Data Gear を定義した
+```
+record metadata : Set where
+  field
+    num-branch : ℕ -- その状態から発生する分岐の数
+    wait-list : List ℕ -- step実行で変化がなかったプロセス
+open metadata
+```
+```
+record MetaEnv : Set where
+  field
+    DG : List Env -- historyを持つためListにしている
+    meta : metadata
+    deadlock : Bool
+    is-done : Bool
+    is-step : Bool
+open MetaEnv
+```
+
+# モデル検査での Meta Data Gear
+```
+record MetaEnv2 : Set where
+  field
+    DG : List (List Env) -- HistoryをもったEnv(状態)を配列として複数持っている。
+    metal :  List MetaEnv
+open MetaEnv2
+```
+
+# モデル検査でのデッドロック検知
+網羅には以下の Meta CodeGear を実装した
+```
+check-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+check-deadlock-metaenv meta2 exit = search-brute-force-envll-p [] (metal meta2) 
+  (λ e → exit record meta2{metal = e}) where
+  search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) 
+    → (exit : List (MetaEnv) → t) → t
+  search-brute-force-envll-p f [] exit = exit f
+  search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv
+  ... | [] = search-brute-force-envll-p f bs exit
+  ... | (env ∷ envs) =  brute-force-search env (λ e0 → search-brute-force-envll-p 
+    (f ++ ( record metaenv{meta = record (meta metaenv)
+    {num-branch = (length e0)} } ∷ [])) bs exit )
+```
+step実行しても状態が変更しない Meta Code Gear も同じように実装している。
+これで meta データ を定義できるようになった。
+
+
+# モデル検査でのデッドロックの検知
+metaデータから deadlock を検出する Meta Code Gear にて 、モデル検査を Gears Agda にて行えるようになった。
+
+```
+judge-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+judge-deadlock-metaenv meta2 exit = judge-deadlock-p [] (metal meta2) 
+  (λ e → exit record meta2{metal = e} ) where
+  judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) 
+    → (exit : List (MetaEnv) → t) → t
+  judge-deadlock-p f [] exit = exit f
+  judge-deadlock-p f (metaenv ∷ bs) exit with num-branch (meta metaenv)
+  ... | suc (suc branchnum) = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
+  ... | zero = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
+  ... | suc zero with (DG metaenv )
+  ... | [] = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
+  ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p))
+  ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
+  ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
+  ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit
+```
+
+# Gears Agda でのモデル検査の実行
+以下の関数にてモデル検査を行うことができる
+```
+{-# TERMINATING #-}
+test-dead-lock-loop2 : MetaEnv2 → MetaEnv2
+test-dead-lock-loop2 metaenv2 = branch-search-meta2 metaenv2 
+  (λ me2 → step-meta2 me2 
+  (λ me3 → testhoge me3 metaenv2 
+  (λ me4 → test-dead-lock-loop2 me4) ) ) 
+(λ e → check-and-judge-deadlock e (λ e1 → e1) )
+```
+<!-- initから投げるまでにした方がいいかもしれないな -->
+
+- Code Gear を繋げたものでは、Agdaは停止性を理解できないので、`{-# TERMINATING #-}`を使用してちゃんと止まることを記述している。
+  - 今回の DPP の状態は有限であることが予めわかっていたから可能だった
+  - 状態爆発が起こったり無限にある場合は、範囲を制限してモデル検査する方法が用いられる (bounded model checking)
+
+# 今後の研究方針
+- モデル検査
+    - 有向グラフからなる有限オートマトンの遷移を全自動探索する
+    - live lock の検出や LTTL も用いたアサーションなどの検証
+    - State List のデータ構造を blanced tree にする
+    - モデル検査に定理証明を組み込む
+- 定理証明
+    - Red Black Tree の検証を行う
+- Gears Agda
+    - Gears Agda を CbC に自動変換できるようにする
+
+
+# まとめ
+- 定理証明について、Invariant によるプログラムの検証を行うことができるようになった
+
+- Gears Agda によるモデル検査により、並列動作の検証を行えるようになった
+
+<!-- 英語版も欲しい-->
\ No newline at end of file