Mercurial > hg > Papers > 2022 > soto-sigos

changeset 11:ae8ea72d5c41

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD スライドを作成
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Wed, 25 May 2022 18:31:17 +0900
parents 07afffd7bf05
children c3f937a26b26
files DPP/ModelChecking.agda slide/slide.md
diffstat 2 files changed, 152 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/DPP/ModelChecking.agda	Tue May 24 19:32:38 2022 +0900
+++ b/DPP/ModelChecking.agda	Wed May 25 18:31:17 2022 +0900
@@ -271,6 +271,12 @@
     deadlock : Bool
 open MetaEnv
 
+record MetaEnv2 : Set where
+  field
+    DG : List (List Env)
+    metal :  List MetaEnv -- 結局探索して1ステップ実行(インターリーディング)するからMetaEnvのList Envがちょうどよい
+open MetaEnv2
+
 
 branch-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t
 branch-deadlock-check metaenv exit = search-brute-force-envll-p [] metaenv exit where
@@ -371,6 +377,121 @@
   test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | _ | _ = test12 stack al b0 bs
 -}
 
+branch-search-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+branch-search-meta2 meta2 exit = search-brute-force-envll (DG meta2) (λ envll → exit record meta2{DG = envll})
+
+step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+step-meta2 meta2 exit = step-brute-force (DG meta2) (λ envll → exit record meta2{DG = envll})
+
+{-# TERMINATING #-}
+check-same-env : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+check-same-env meta2 exit = check-same-env-p [] (metal meta2) meta2 exit where
+  check-wait-process-p : {n : Level} {t : Set n} → ℕ → List Phi → (p1 : Env) → (exit : ℕ → t) → t
+  check-wait-process-p waitl [] p1 exit = exit waitl
+  check-wait-process-p waitl (p ∷ ps) p1 exit = hoge11 waitl p (ph p1) (λ e → check-wait-process-p e ps p1 exit) where
+    hoge11 : {n : Level} {t : Set n} → ℕ → Phi → List Phi → (exit : ℕ → t) → t
+    hoge11 n p [] exit = exit n
+    hoge11 n p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp)
+    hoge11 n p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 n p p1s exit
+    hoge11 n p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 n p p1s exit
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit n
+  check-wait-process : {n : Level} {t : Set n} → ℕ → List Phi → List MetaEnv → MetaEnv → (exit : List MetaEnv → t) → t
+  check-wait-process n pl metal me exit with metal
+  ... | sss with <-cmp (length pl) n
+  ... | tri≈ ¬a b ¬c = exit (me ∷ [])
+  check-wait-process n pl metal me exit | [] | tri< a ¬b ¬c = exit []
+  check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c with DG x
+  check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | [] = exit []
+  check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit)
+  check-wait-process n pl metal me exit | [] | tri> ¬a ¬b c = exit []
+  check-wait-process n pl metal me exit | x ∷ sss | tri> ¬a ¬b c with DG x
+  ... | [] = exit []
+  ... | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit)
+  check-same-env-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → MetaEnv2 → (exit : MetaEnv2 → t) → t
+  check-same-env-p [] [] metae2 exit = exit metae2
+  check-same-env-p f@(x ∷ fs) [] metae2 exit = step-meta2 record metae2{metal = f} (λ me2 → branch-search-meta2 me2 (λ me3 → check-same-env me3 exit))
+  check-same-env-p [] bl@(b ∷ bs) metae2 exit with DG b
+  ... | [] =  check-same-env-p [] bs metae2 exit
+  ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p ([] ++ lme) bl metae2 exit)
+  check-same-env-p f@(x ∷ fs) bl@(b ∷ bs) metae2 exit with DG b
+  ... | [] = check-same-env-p f bs metae2 exit
+  ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p (f ++ lme) bl metae2 exit)
+
+check-same-env-test : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+check-same-env-test meta2 exit = check-same-env-p [] (metal meta2) meta2 exit where
+  check-wait-process-p : {n : Level} {t : Set n} → ℕ → List Phi → (p1 : Env) → (exit : ℕ → t) → t
+  check-wait-process-p waitl [] p1 exit = exit waitl
+  check-wait-process-p waitl (p ∷ ps) p1 exit = hoge11 waitl p (ph p1) (λ e → check-wait-process-p e ps p1 exit) where
+    hoge11 : {n : Level} {t : Set n} → ℕ → Phi → List Phi → (exit : ℕ → t) → t
+    hoge11 n p [] exit = exit n
+    hoge11 n p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp)
+    hoge11 n p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 n p p1s exit
+    hoge11 n p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 n p p1s exit
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (suc n)
+    hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit n
+  check-wait-process : {n : Level} {t : Set n} → ℕ → List Phi → List MetaEnv → MetaEnv → (exit : List MetaEnv → t) → t
+  check-wait-process n pl metal me exit with metal
+  ... | sss with <-cmp (length pl) n
+  ... | tri≈ ¬a b ¬c = exit (me ∷ [])
+  check-wait-process n pl metal me exit | [] | tri< a ¬b ¬c = exit (me ∷ [])
+  check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c with DG x
+  check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | [] = exit []
+  check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit)
+  check-wait-process n pl metal me exit | [] | tri> ¬a ¬b c = exit (me ∷ [])
+  check-wait-process n pl metal me exit | x ∷ sss | tri> ¬a ¬b c with DG x
+  ... | [] = exit []
+  ... | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit)
+  make-metaenvl : {n : Level} {t : Set n} → (f : (List MetaEnv)) → List (List Env) → (exit : List MetaEnv → t) → t
+  make-metaenvl f [] exit = exit f
+  make-metaenvl f ([] ∷ bs) exit = make-metaenvl f bs exit
+  make-metaenvl f ((e ∷ es) ∷ bs) exit = make-metaenvl (f ++ (record{ DG = (e ∷ []); meta = record { num-branch = zero ; wait-list = [] }; deadlock = true} ∷ [])) bs exit
+  check-same-env-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → MetaEnv2 → (exit : MetaEnv2 → t) → t
+  check-same-env-p [] [] metae2 exit = make-metaenvl [] (DG metae2) (λ lme → exit record metae2{metal = lme})
+  check-same-env-p f@(x ∷ fs) [] metae2 exit = exit record metae2{metal = f}
+  check-same-env-p [] bl@(b ∷ bs) metae2 exit with DG b
+  ... | [] =  check-same-env-p [] bs metae2 exit
+  ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p ([] ++ lme) bs metae2 exit)
+  check-same-env-p f@(x ∷ fs) bl@(b ∷ bs) metae2 exit with DG b
+  ... | [] = check-same-env-p f bs metae2 exit
+  ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p (f ++ lme) bs metae2 exit)
+
+record Eq (A : Set) : Set where
+  field
+    == : A → A → Bool
+
+open Eq {{...}}
+
+record testrec : Set where
+  field
+    aaa : ℕ
+
+{-
+search-brute-force-envll : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t
+search-brute-force-envll envll exit = search-brute-force-envll-p [] envll exit where
+  search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t
+  search-brute-force-envll-p f [] exit = exit f
+  search-brute-force-envll-p f ([] ∷ bs) exit = search-brute-force-envll-p f bs exit
+  search-brute-force-envll-p f (b@(x ∷ xs) ∷ bs) exit = brute-force-search x (λ e0 → make-brute-force-envl [] e0 b (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit) ) where
+    make-brute-force-envl : {n : Level} {t : Set n} → List (List Env) → (state p_step : List Env) → (exit : List (List Env) → t) → t
+    make-brute-force-envl res [] xs exit = exit res
+    make-brute-force-envl res (x ∷ state) xs exit = make-brute-force-envl (res ++ (x ∷ xs) ∷ []) state xs exit
+-}
+
 test-env : Env
 test-env = (record {
   table = 0 ∷ 0 ∷ 0 ∷ []
@@ -424,6 +545,23 @@
                    ; deadlock = false
                    } ∷ []) (λ e3 → e3)
 
+test-dead-lock-meta2 : MetaEnv2
+test-dead-lock-meta2 = branch-search-meta2 (record { DG = (record { table =  0 ∷ 0 ∷ 0 ∷ [] ; ph = record
+           { pid = 1
+           ; left-hand = false
+           ; right-hand = false
+           ; next-code = C_thinking
+           } ∷ record
+                 { pid = 2
+                 ; left-hand = false
+                 ; right-hand = false
+                 ; next-code = C_pickup_rfork
+           } ∷ record
+                 { pid = 3
+                 ; left-hand = false
+                 ; right-hand = false
+                 ; next-code = C_pickup_rfork
+                 }  ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 (λ me3 → check-same-env-test me3 (λ me4 → me4))) ))
 
 test-step-c2 : List (List Env)
 test-step-c2 = init-brute-force (record {
--- a/slide/slide.md	Tue May 24 19:32:38 2022 +0900
+++ b/slide/slide.md	Wed May 25 18:31:17 2022 +0900
@@ -67,7 +67,7 @@
 # Gears Agda と CbC
 - Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のこと
 - 通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。この際メインルーチンで使用していた変数などの環境はスタックされ、サブルーチンが終了した際にメインルーチンに戻り、スタックしていた変数をもとに戻す流れとなる。
-- CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ、スタックを持たず環境を保持しない。更に遷移後にメインルーチンに戻ることもない。つまり関数の実行では暗黙な環境が存在せず、関数が受け取った引数のみを使用する。
+- CbCの場合はサブルーチンコールの際にアセンブラでいうjmpで関数遷移を行うことができ、スタックを持たず環境を保持しない。更に遷移後にメインルーチンに戻ることもない。つまり関数の実行では暗黙な環境が存在せず、関数が受け取った引数のみを使用する。
 - これにより限定的な実行条件を作成でき、検証がしやすくなる。
 
 # Gears Agda でのアルゴリズム入れ替え判定
@@ -86,12 +86,12 @@
 
 - アルゴリズムの入れ替え可否をモデル検査で判定し、入れ替えたあとに適応前後で同じ処理をしていることを定理証明で検証することを目標としている
 
-- この Gears Agda でのモデル検査の先駆けとして今回は Dining Philosophers Programのモデル検査を行った
+- この Gears Agda でのモデル検査の先駆けとして今回は Dining Philosophers Program のモデル検査をboundedで行っている
 
 # CbC について
 - CbCとは当研究室で開発しているC言語の下位言語
   - 継続呼び出しは引数付き goto 文で表現される。
-    - 関数呼び出し時のスタックの操作を行わずjmp命令で次の処理に移動する
+    - 関数呼び出し時にスタックの操作を行わずjmp命令で次の処理に移動する
   - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
 - CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。
 
@@ -102,7 +102,7 @@
 - 型の定義部分で、入力と出力の型を定義できる
   -  input → output のようになる
 - 関数の定義は = を用いて行う
-  - 関数名の後、 = の前で受け取る引数を記述します
+  - 関数名の後ろの行で、 = の前で受け取る引数を記述、=の後ろで実装を記述します
 
 <!--
 curry-Houerd対応
@@ -149,32 +149,34 @@
 # Normal level と Meta Level の対応
 ![height:400px](meta-ca-dg.jpg)
 
-# DPPの説明
+# Dining Philosophers Program の説明
 ![height:500px](DPP.jpg)
 
 # モデル検査と定理証明の説明
 モデル検査はコストが安いが完全な検証にはならない
 定理証明はコスト高いが完全な検証になる
 
-# DPPの記述
+# Dining Philosophers Program の記述
 - DPPはマルチプロセスの同期問題である
   - しかし、Agdaでは並列実行をサポートしていないため、step実行毎に一つづつ処理することで並列実行を表現している
 
 - 加えて、哲学者が思考中に食事をし始めるのか、食事中に思考に戻ろうとするのかで分岐が発生する
-  - これを網羅するために今回はその状態に対してビット全探索を行った
+  - これを網羅するために今回はその状態に対して網羅することでモデル検査をboundedに行っている
 
 # モデル検査でのデッドロック検知
+- 現在は探索する深さを指定している(boundedなモデル検査)
 - デッドロックとは全てのプロセスが他のプロセスの実行待ちの状態となり実行が進まなくなること
 - 今回Gears Agda でのデッドロックの定義として、以下2つを満たすものとした
-  - ビット全探索で分岐が作れない
+  - 網羅で分岐が作れない
   - 実行時に状態に変動がない
 - これでプログラムがデッドロックしているのか検知するところまではできるようになった
 
 # まとめと今後の研究方針
-- 今回は Gears Agda にてDPPを記述し、モデル検査にてデッドロックを検知できるようになった
-  - 今回のモデル検査を一般化し、自動でモデル検査を実行できるようにしたい
-  - さらにプログラムの仕様を渡し、これを満たしているかモデル検査で検証したい
-    - 仕様にLTLを使えるようにもしたい
+- 今回は Gears Agda にて Dining Philosophers Program を記述し、モデル検査にてデッドロックをboundedに検知できるようになった
+  - unboundedなデッドロック検知ができるように
+  - 今回のモデル検査を一般化し、自動でモデル検査を実行できるように
+  - さらにプログラムの仕様を渡し、これを満たしているかモデル検査で検証
+    - 仕様にLTLを使えるように
 - アルゴリズムの自動適応にて、モデル検査で仕様を満たしている場合に入れ替えて同じ動作をしているかを定理証明で証明できるようにしたい
 
 <!-- 英語版も欲しい -->