Mercurial > hg > Papers > 2023 > soto-master
changeset 12:3aa9d35e93bf
add conclusion
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 29 Jan 2023 15:21:21 +0900 |
| parents | 1a8a9fa534a2 |
| children | 62d87fdd7775 |
| files | Paper/master_paper.out Paper/master_paper.pdf Paper/master_paper.tex Paper/src/dpp-verif/ModelChecking.agda Paper/tex/dpp_impl.tex Paper/tex/spin_dpp.tex Paper/tex/thanks.tex |
| diffstat | 7 files changed, 141 insertions(+), 59 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/master_paper.out Sat Jan 28 23:34:46 2023 +0900 +++ b/Paper/master_paper.out Sun Jan 29 15:21:21 2023 +0900 @@ -30,8 +30,9 @@ \BOOKMARK [1][]{section.6.7}{\376\377\0006\000.\0007\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000\040\000l\000i\000v\000e\000\040\000l\000o\000c\000k\060\156\151\034\212\074\145\271\154\325\060\153\060\144\060\104\060\146}{chapter.6}% 29 \BOOKMARK [1][]{section.6.8}{\376\377\0006\000.\0008\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\060\342\060\307\060\353\151\034\147\373\060\156\212\125\117\241}{chapter.6}% 30 \BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\060\176\060\150\060\201\060\150\116\312\137\214\060\156\134\125\147\033}{}% 31 -\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 32 -\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 33 -\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 34 -\BOOKMARK [0][]{appendix.A}{\376\377\116\330\000\040\223\062\000A\000\040\000\040\170\024\172\166\117\032\151\155\176\076}{}% 35 -\BOOKMARK [1][]{section.A.1}{\376\377\000A\000-\0001\000\040\170\024\172\166\117\032\166\172\210\150\214\307\145\231}{appendix.A}% 36 +\BOOKMARK [1][]{section.7.1}{\376\377\0007\000.\0001\000\040\116\312\137\214\060\156\212\262\230\114}{chapter.7}% 32 +\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 33 +\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 34 +\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 35 +\BOOKMARK [0][]{appendix.A}{\376\377\116\330\000\040\223\062\000A\000\040\000\040\170\024\172\166\117\032\151\155\176\076}{}% 36 +\BOOKMARK [1][]{section.A.1}{\376\377\000A\000-\0001\000\040\170\024\172\166\117\032\166\172\210\150\214\307\145\231}{appendix.A}% 37
--- a/Paper/master_paper.tex Sat Jan 28 23:34:46 2023 +0900 +++ b/Paper/master_paper.tex Sun Jan 29 15:21:21 2023 +0900 @@ -117,42 +117,41 @@ \input{tex/intro.tex} \input{tex/cbc.tex} \input{tex/agda.tex} - \input{tex/cbc_agda.tex} +\chapter{Gears Agda による定理証明} +先行研究では、Hoare Logic を 使用して while loop の検証を行っていた。 +本研究では、invariant というプログラムの不変条件を定義し、それを検証することで、比較的容易に検証を行うことができるようになった(本章2節) +本章では Gears Agda による定理証明の方法について説明する。 -\chapter{Gears Agda による定理証明} \input{tex/hoare.tex} \input{tex/while_loop.tex} % while loop の実装と検証(簡単に) \input{tex/tree_desc.tex}% Gears Agda における木構造の設計 -\chapter{Gears Agda によるモデル検査} -定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが -できるが，専門的な知識が多く難易度が高いという欠点がある． -加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、 -並列処理を定理証明するには検証する状態が膨大になり困難である。 -そのため、並列処理はモデル検査にて検証する方が良い。 - -\section{モデル検査とは} -モデル検査 (Model Cheking) とは、検証手法のひとつである。 -モデル検査はプログラムが入力に対して仕様を満たした動作を -行うことを網羅的に検証することを指す． -しかし、モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる -状態爆発が起こり得るという問題がある． -実際にモデル検査で行うことは、検証したい内容の時相理論式 $\varphi$ を作り、対象のシステムの初期状態 s のモデル M があるとき、M, s が $\varphi$ を満たすかを調べる。 - \input{tex/spin_dpp.tex}% Gears Agda の記法 loopのやつやる - -% Gears Agdaの場合はListの方が停止することがわかりやすいので、今回はState Listを作成した。本来はburanceされたtree structureが最も良い - \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる \chapter{まとめと今後の展望} -ここまでで Gears Agda により定理証明を用いた検証と -モデル検査による検証方法を確立した． -これからは Red Black Tree の定理証明を用いた検証と， -モデル検査部分では現在boundedな検知を行っているので -unboundedな検知を行えるようにしたい． +本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで、定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。 + +実際に Invariant を用いることで、プログラムに与える入力とその出力に対して条件を与え、Hoare Logic による検証を行えるようになった。 +これにより、いままでより容易に Gears Agda にて検証が進められるようになった。 + +また、先行研究での課題にて、CbCで開発、検証を行いたいと考えている Gears OSの並列並列動作の検証があった。これもモデル検査により、Gears Agda 内で並列動作に対する検証も行えるようになった。 + + +\section{今後の課題} +今後の課題としてモデル検査による検証、定理証明による検証、Gears Agda の今後の展望について述べる。 +モデル検査においては、有効オートマトンによるプログラムの遷移を全自動探索することと、live lockやアサーションの検証を行いたい。 +加えて、State List のデータ構造を brunced tree にすることで、並列にモデル検査が行えるようになると考えられる。 +これにより、状態が膨大になるモデル検査に対応できる。 + +定理証明においては、Red Black Tree の検証を行いたいと思っている。 +これで検証を行ったものをモデル検査や Gears OS のファイルシステムなどに転用できると考えている。 + +Gears Agda の展望について、CbC に変換することが挙げられる。 +CbC はアセンブラに近いため記述が複雑かつ困難であるが、Gears Agda で記述したものを CbC に変換できるようになれば、その点を解決できる。更に、Gears Agda で検証を行ったプログラムであるため、プログラムの信頼性もある。 +加えて、モデル検査の実行には速度が求められるが、CbCで高速に実行できるようになることが期待される。 % %謝辞 \input{tex/thanks.tex}
--- a/Paper/src/dpp-verif/ModelChecking.agda Sat Jan 28 23:34:46 2023 +0900 +++ b/Paper/src/dpp-verif/ModelChecking.agda Sun Jan 29 15:21:21 2023 +0900 @@ -136,8 +136,22 @@ set-state redu origin (false ∷ ss) f b env envl exit | p ∷ ps | C_eating = set-state redu origin ss (f ++ (p ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む set-state redu origin (true ∷ ss) f b env envl exit | p ∷ ps | C_thinking = set-state redu origin ss (f ++ (record p{next-code = C_pickup_rfork} ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む set-state redu origin (false ∷ ss) f b env envl exit | p ∷ ps | C_thinking = set-state redu origin ss (f ++ (p ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む - set-state redu origin (s ∷ ss) f b env envl exit | p ∷ ps | _ = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする + set-state redu origin st@(s ∷ ss) f b env envl exit | p ∷ ps | _ = set-state redu origin st (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする +-- eatingも探索範囲に含める +brute-force-search-1 : {n : Level} {t : Set n} → Env → (exit : List Bool → t) → t +brute-force-search-1 env exit = make-state-list 1 [] (ph env) env (env ∷ []) exit where + make-state-list : {n : Level} {t : Set n} → ℕ → List Bool → List Phi → Env → (List Env) → (exit : List Bool → t) → t + make-state-list redu state (x ∷ pl) env envl exit with next-code x + ... | C_thinking = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit + ... | C_eating = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit + ... | _ = make-state-list redu state pl env envl exit + make-state-list redu state [] env envl exit = bit-force-search redu [] state env envl exit where + bit-force-search : {n : Level} {t : Set n} → ℕ → (f b : List Bool )→ Env → (List Env) → (exit : List Bool → t) → t + bit-force-search zero f l env envl exit = exit [] + bit-force-search (suc redu) f [] env envl exit = exit [] + bit-force-search (suc redu) f (true ∷ bs) env envl exit = bit-force-search (suc redu) (f ++ (false ∷ [])) bs env envl exit + bit-force-search (suc redu) f (false ∷ bs) env envl exit = exit (f ++ (true ∷ bs)) test-search : List Env test-search = init-table 3 (λ e0 → brute-force-search e0 (λ e1 → e1)) @@ -281,6 +295,7 @@ metal : List MetaEnv -- 結局探索して1ステップ実行(インターリーディング)するからMetaEnvのList Envがちょうどよい open MetaEnv2 +-- this one need 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 search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t @@ -290,7 +305,8 @@ ... | (env ∷ envs) = brute-force-search env (λ e0 → make-brute-force-envl (length e0) [] metaenv e0 (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit)) where make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t make-brute-force-envl len res xs [] exit = exit res - make-brute-force-envl len res xs (x ∷ state) exit = make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit + make-brute-force-envl len res xs (x ∷ state) exit = brute-force-search env (λ e0 → search-brute-force-envll-p (f ++ ( record metaenv{meta = record (meta metaenv){num-branch = (length e0)} } ∷ [])) bs exit ) + -- make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit data _===_ {n} {A : Set n} : List A -> List A -> Set n where reflection : {x : List A} -> x === x @@ -305,6 +321,7 @@ testhoge _ _ = {!!} -} +-- this need step-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t step-deadlock-check metaenvl exit = deadlock-check-p [] metaenvl exit where deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t @@ -356,6 +373,45 @@ ... | 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 +waitlist-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t +waitlist-deadlock-metaenv meta2 exit = deadlock-check-p [] (metal meta2) (λ e → exit record meta2{metal = e}) where + deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + deadlock-check-p f [] exit = exit f + deadlock-check-p f b@(metaenv ∷ bs) exit with DG metaenv + ... | [] = deadlock-check-p f bs exit + ... | p0 ∷ envs = step-c p0 (λ e0 → check-wait-process [] (ph p0) e0 ( λ e → deadlock-check-p (f ++ (record metaenv{meta = record (meta metaenv){wait-list = e } } ∷ [])) bs exit) ) where + check-wait-process : {n : Level} {t : Set n} → List ℕ → List Phi → (p1 : Env) → (exit : List ℕ → t) → t + check-wait-process waitl [] p1 exit = exit waitl + check-wait-process waitl (p ∷ ps) p1 exit = hoge11 p (ph p1) (λ e → check-wait-process (waitl ++ e) ps p1 exit) where + hoge11 : {n : Level} {t : Set n} → Phi → List Phi → (exit : List ℕ → t) → t + hoge11 p [] exit = exit [] + hoge11 p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp) + hoge11 p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 p p1s exit + hoge11 p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 p p1s exit + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit [] + +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 ) + {- + -- brute-force-search env (λ e0 → make-brute-force-envl (length e0) [] metaenv e0 (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit)) where + make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t + make-brute-force-envl len res xs [] exit = exit res + make-brute-force-envl len res xs (x ∷ state) exit = make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit +-} + 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 @@ -368,7 +424,7 @@ ... | 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 + ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = false} ∷ []) ) bs exit {- test-env-deadlock : {n : Level} {t : Set n} → (a b : Env)→ (exit : List MetaEnv → t) → t @@ -412,14 +468,14 @@ make-brute-force-envl res (addenv ∷ statel) meta exit = make-brute-force-envl (res ++ ( record meta{DG = addenv ∷ (DG meta); is-done = false; is-step = false} ∷ [])) statel meta exit -step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (next exit : MetaEnv2 → t) → t -step-meta2 meta2 next1 exit = step-brute-force-p1 [] (metal meta2) (λ envll → next1 record meta2{metal = envll}) (λ e → exit meta2) where +step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t +step-meta2 meta2 exit = step-brute-force-p1 [] (metal meta2) (λ envll → exit record meta2{metal = envll}) where step-brute-force-p-p : {n : Level} {t : Set n} → (envl : (List Env)) → (exit : (List Env) → t) → t - step-brute-force-p1 : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (next exit : List (MetaEnv) → t) → t - step-brute-force-p1 f [] next1 exit = next1 f - step-brute-force-p1 f (metaenv ∷ metaenvl) next1 exit with is-step metaenv - ... | true = step-brute-force-p1 (f ++ (metaenv ∷ [])) metaenvl next1 exit - ... | false = step-brute-force-p-p (DG metaenv) (λ e0 → step-brute-force-p1 (f ++ (record metaenv{DG = e0; is-step = true} ∷ [])) metaenvl next1 exit) + step-brute-force-p1 : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + step-brute-force-p1 f [] exit = exit f + step-brute-force-p1 f (metaenv ∷ metaenvl) exit with is-step metaenv + ... | true = step-brute-force-p1 (f ++ (metaenv ∷ [])) metaenvl exit + ... | false = step-brute-force-p-p (DG metaenv) (λ e0 → step-brute-force-p1 (f ++ (record metaenv{DG = e0; is-step = true} ∷ [])) metaenvl exit) step-brute-force-p-p [] exit = exit [] step-brute-force-p-p (x ∷ bs) exit = step-c x (λ e0 → exit (e0 ∷ bs)) @@ -457,7 +513,7 @@ ... | 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) exit ) exit + 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) 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) @@ -544,19 +600,20 @@ ; next-code = C_thinking } ∷ [] }) + test-env1 : Env test-env1 = (record { - table = 1 ∷ 2 ∷ 0 ∷ [] + table = 1 ∷ 0 ∷ 0 ∷ [] ; ph = record { pid = 1 ; left-hand = false - ; right-hand = false - ; next-code = C_pickup_rfork + ; right-hand = true + ; next-code = C_pickup_lfork } ∷ record { pid = 2 ; left-hand = false ; right-hand = false - ; next-code = C_pickup_rfork + ; next-code = C_thinking } ∷ record { pid = 3 ; left-hand = false @@ -614,7 +671,7 @@ ... | [] = exit origin ... | env1 ∷ envl with DG x ... | [] = loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit - ... | env2 ∷ history = eq-env origin (ph env1) (ph env2) (λ exit-e → exit record origin{metal = f ++ (record x{is-done = boolor (is-done me) (is-done x); is-step = boolor (is-step me) (is-step x) } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit ) + ... | env2 ∷ history = eq-env origin (ph env1) (ph env2) (λ exit-e → exit record origin{metal = f ++ (record x{is-done = boolor (is-done me) (is-done x) } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit ) eq-env origin [] [] exit loop = exit origin -- true eq-env origin [] (x ∷ pl2) exit loop = loop false @@ -624,7 +681,7 @@ eq-pid origin pl1 pl2 p1 p2 next1 exit1 with <-cmp (pid p1) (pid p2) ... | tri< a ¬b ¬c = exit1 false ... | tri> ¬a ¬b c = exit1 false - ... | tri≈ ¬a b ¬c = eq-lhand origin pl1 pl2 p1 p2 next1 exit1 + ... | tri≈ ¬a b ¬c = eq-lhand origin pl1 pl2 p1 p2 next1 exit1 eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 with (left-hand phi1) ... | sss with (left-hand phi2) @@ -632,7 +689,7 @@ eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | false = exit1 false eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | true = exit1 false eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | false = eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 - + eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 with (right-hand phi1) ... | sss with (right-hand phi2) eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | true = eq-next-code origin pl1 pl2 phi1 phi2 next1 exit1 @@ -714,7 +771,7 @@ ; 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 → testhoge me3 me2 (λ me4 → check-same-env-test me4 (λ me5 → me5))) (λ e → e) ) (λ e → e) )) (λ e → e) + } ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 ( λ me3 → testhoge me3 me2 (λ me4 → check-same-env-test me4 (λ me5 → me5))) (λ e → e) ) )) (λ e → e) test-dead-lock-meta21 : MetaEnv2 @@ -733,18 +790,22 @@ ; 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 → testhoge me3 me2 (λ me4 → check-same-env-test me4 (λ me5 → me5))) (λ e → e) ) (λ e → e) )) (λ e → e) + } ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 ( λ me3 → testhoge me3 me2 (λ me4 → check-same-env-test me4 (λ me5 → me5))) (λ e → e) ) )) (λ e → e) +check-and-judge-deadlock : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t +check-and-judge-deadlock meta2 exit = check-deadlock-metaenv meta2 (λ e0 → waitlist-deadlock-metaenv e0 (λ e → judge-deadlock-metaenv e exit ) ) + test-dead-lock-meta22 : ℕ → MetaEnv2 → MetaEnv2 -test-dead-lock-meta22 zero metaenv2 = metaenv2 -test-dead-lock-meta22 (suc n) metaenv2 = branch-search-meta2 metaenv2 (λ me1 → testhoge me1 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 me2 (λ me4 → test-dead-lock-meta22 n me4) ) (λ e → e)) ) (λ e → e) +test-dead-lock-meta22 zero metaenv2 = check-and-judge-deadlock metaenv2 (λ e → e) +test-dead-lock-meta22 (suc n) metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-meta22 n me4) ) ) (λ e5 → e5) {-# TERMINATING #-} test-dead-lock-loop : MetaEnv2 → MetaEnv2 -test-dead-lock-loop metaenv2 = branch-search-meta2 metaenv2 (λ me1 → testhoge me1 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 me2 (λ me4 → test-dead-lock-loop me4) ) (λ e → e)) ) (λ e → e) +test-dead-lock-loop metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-loop me4) ) ) (λ e → e) --- test-dead-lock-loop test-metaenv2 +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-loop me4) ) ) (λ e → check-and-judge-deadlock e (λ e1 → e1) ) test-step-c2 : List (List Env) test-step-c2 = init-brute-force (record {
--- a/Paper/tex/dpp_impl.tex Sat Jan 28 23:34:46 2023 +0900 +++ b/Paper/tex/dpp_impl.tex Sun Jan 29 15:21:21 2023 +0900 @@ -112,12 +112,16 @@ 加えて今まで実行していた Data Gear を DG で持てる。 次に Meta Data Gear を作成する Meta Code Gear の説明をすると + - その状態から分岐できる状態数をカウントする Meta Code Gear + - Wait List を作成する Meta Code Gear -以下が分岐できる状態数をカウントする Meta Code Gear のcodeとなる +以下の \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 データとしている。 @@ -125,7 +129,7 @@ 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 に入るようになっている。 @@ -136,7 +140,7 @@ 以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる -複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て +複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て、wait-listの数がプロセス数と一致していた場合に deadlockのフラグを立ち上げている。これが、Gears Agda におけるアサーションになっている。 % judge-dead-lock-pのソースコードを貼り付ける
--- a/Paper/tex/spin_dpp.tex Sat Jan 28 23:34:46 2023 +0900 +++ b/Paper/tex/spin_dpp.tex Sun Jan 29 15:21:21 2023 +0900 @@ -1,3 +1,18 @@ +\chapter{Gears Agda によるモデル検査} +定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが +できるが，専門的な知識が多く難易度が高いという欠点がある． +加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、 +並列処理を定理証明するには検証する状態が膨大になり困難である。 +そのため、並列処理はモデル検査にて検証する方が良い。 + +\section{モデル検査とは} +モデル検査 (Model Cheking) とは、検証手法のひとつである。 +モデル検査はプログラムが入力に対して仕様を満たした動作を +行うことを網羅的に検証することを指す． +しかし、モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる +状態爆発が起こり得るという問題がある． +実際にモデル検査で行うことは、検証したい内容の時相理論式 $\varphi$ を作り、対象のシステムの初期状態 s のモデル M があるとき、M, s が $\varphi$ を満たすかを調べる。 + \section{Dining Philosophers Problem} 今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP) を用いることとした．
--- a/Paper/tex/thanks.tex Sat Jan 28 23:34:46 2023 +0900 +++ b/Paper/tex/thanks.tex Sun Jan 29 15:21:21 2023 +0900 @@ -3,8 +3,10 @@ 本研究の遂行、本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に心より感謝致します。 共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します。 -最後に、 有意義な時間を共に過ごした理工学研究科情報工学専攻の学友、並びに物心両面で支えてくれた家族に深く感謝致します。 +私の研究において苦楽を共にした Manjaro Linux とその開発者には頭が上がりません。 +さらに、ゼミの前においしいご飯で元気づけてくれた Hally's Cafe に感謝しております。 +最後に、 有意義な時間を共に過ごした理工学研究科工学専攻の学友、並びに物心両面で支えてくれた家族に深く感謝致します。 \begin{flushright} - 2022年 3月 \\ 安田亮 + 2023年 3月 \\ 上地悠斗 \end{flushright} \ No newline at end of file