# HG changeset patch # User soto # Date 1613143844 -32400 # Node ID e5248199c73d2937e18c48d2bcbfff83aa27885c # Parent bb7e9eaf9df86c37981d7487c705424f826921ab FIX readd references diff -r bb7e9eaf9df8 -r e5248199c73d paper/final_thesis.pdf Binary file paper/final_thesis.pdf has changed diff -r bb7e9eaf9df8 -r e5248199c73d paper/final_thesis.tex --- a/paper/final_thesis.tex Fri Feb 12 18:02:24 2021 +0900 +++ b/paper/final_thesis.tex Sat Feb 13 00:30:44 2021 +0900 @@ -11,7 +11,7 @@ \usepackage{picins} \usepackage{mythesis} -%\pagestyle{empty} +\pagestyle{empty} \usepackage{multirow} % 特殊文字の表示 @@ -75,7 +75,7 @@ \icon{\includegraphics[width=50mm]{pic/ryukyu.pdf}} \year{令和2年度 卒業論文} \belongto{琉球大学工学部工学科知能情報コース} -\author{175707H 氏名 {上地 悠斗}\\ 指導教員 : {河野 真治} } +\author{175707H {上地 悠斗}\\ 指導教員 : {河野 真治} } % 目次 \makeatletter @@ -108,9 +108,9 @@ \input{tex/cbc_agda.tex}% continuation 形式で書くagda \input{tex/hoare.tex} % Hoare Logic の説明 \input{tex/rbt_intro.tex} % 赤黒木の説明 -\input{tex/rbt_imple.tex}% 手法 -\input{tex/rbt_verif.tex}% 検証 -\input{tex/future.tex}% 今後の課題 +\input{tex/rbt_imple.tex} % 手法 +\input{tex/rbt_verif.tex} % 検証 +\input{tex/future.tex} % 今後の課題 \input{tex/thanks.tex} % 謝辞 \printbibliography[title={参考文献}] diff -r bb7e9eaf9df8 -r e5248199c73d paper/src/agda/list-any.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda/list-any.agda Sat Feb 13 00:30:44 2021 +0900 @@ -0,0 +1,73 @@ +module list-any where + +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; refl; sym; trans; cong) +open Eq.≡-Reasoning +open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not) +open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n) +open import Data.Nat.Properties using + (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩) +open import Function using (_∘_) +open import Level using (Level) +--open import plfa.part1.Isomorphism using (_≃_; _⇔_) + +open import Data.List +open import Data.Nat.Properties as NatProp -- <-cmp +open import Relation.Binary + +open import rbt_t + +-- infix 4 _∈_ _∉_ + +test-l : List ℕ +test-l = 1 ∷ 2 ∷ [] + +data Any-test {A : Set} (P : A → Set) : List A → Set where + here : ∀ {x : A} {xs : List A} → P x → Any-test P (x ∷ xs) + there : ∀ {x : A} {xs : List A} → Any-test P xs → Any-test P (x ∷ xs) + +{- +_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set +x ∈ xs = Any (x ≡_) xs +-} + +_∈1_ : ∀ (n : ℕ) (xs : List ℕ) → Set +n ∈1 [] = Any-test (n ≡_) [] +n ∈1 l@(x ∷ xs) with <-cmp n x +... | tri< a ¬b ¬c = Any-test (n ≡_) xs +... | tri≈ ¬a b ¬c = Any-test (n ≡_) l +... | tri> ¬a ¬b c = Any-test (n ≡_) xs + +test : 1 ∈1 test-l +test = here refl + +data Any (P : ℕ → Set) : rbt → Set where + here : ∀ {x : ℕ} {xs : rbt} → P x → Any P xs + there : ∀ {x : ℕ} {xs : rbt} → Any P (get-rbt xs) → Any P xs + +_∈_ : ∀ (n : ℕ) (xs : rbt) → Bool +n ∈ bt-empty = false +n ∈ bt-node node with <-cmp n (node.number (tree.key node)) +... | tri< a ¬b ¬c = n ∈ (tree.ltree node) +... | tri≈ ¬a b ¬c = true +... | tri> ¬a ¬b c = n ∈ (tree.rtree node) + + + +testany1 : rbt → Set +testany1 bt-empty = {!!} +testany1 (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) = {!!} + +testrbt1 = whileTestPCall' bt-empty 0 +testrbt2 = whileTestPCall' (Env.vart testrbt1) 1 +testrbt3 = whileTestPCall' (Env.vart testrbt2) 2 +testrbt4 = whileTestPCall' (Env.vart testrbt3) 3 +testrbt5 = whileTestPCall' (Env.vart testrbt4) 4 +testrbt6 = whileTestPCall' (Env.vart testrbt5) 5 +testrbt7 = whileTestPCall' (Env.vart testrbt6) 6 + + +test1kk = 100 ∈ (Env.vart testrbt6) + diff -r bb7e9eaf9df8 -r e5248199c73d paper/src/agda/rbt_t.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda/rbt_t.agda Sat Feb 13 00:30:44 2021 +0900 @@ -0,0 +1,276 @@ +module rbt_t where + +open import Data.Nat hiding (compare) +open import Data.Nat.Properties as NatProp -- <-cmp +open import Relation.Binary +open import Data.List + +-- → t を適用するために必要だった +open import Level renaming ( suc to succ ; zero to Zero ) +open import Level + + +data col : Set where + black : col + red : col + +record node (A B : Set) : Set where + field + coler : A + number : B +open node + +record tree (A B C : Set) : Set where + field + key : A + ltree : B + rtree : C +open tree + +data rbt : Set where + bt-empty : rbt + bt-node : (node : tree (node col ℕ) rbt rbt ) → rbt + +record Env : Set (succ Zero) where + field + vart : rbt + varn : ℕ + varl : List rbt +open Env + +whileTest-next : {l : Level} {t : Set l} → (c10 : rbt) → (n : ℕ) → (list : List rbt) → (next : Env → t) → (exit : Env → t) → t +whileTest-next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} ) + +merge-tree : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t + +-- 全てmerge-treeへ +split : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +split node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +split node@record { vart = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit node +split node@record { vart = (bt-node record { key = key ; ltree = (bt-node node₁) ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node +split record { vart = (bt-node record { key = record { coler = coler₁ ; number = number₁ } + ; ltree = (bt-node record { key = record { coler = ly ; number = ln } ; ltree = ll ; rtree = lr }) + ; rtree = (bt-node record { key = record { coler = ry ; number = rn } ; ltree = rl ; rtree = rr }) }) + ; varn = varn ; varl = varl } next exit + = next record { vart = (bt-node record { key = record { coler = red ; number = number₁ } + ; ltree = (bt-node record { key = record { coler = black ; number = ln } ; ltree = ll ; rtree = lr }) + ; rtree = (bt-node record { key = record { coler = black ; number = rn } ; ltree = rl ; rtree = rr }) }) + ; varn = varn ; varl = varl } + + +-- 右回転 +-- 実行時splitへ、それ以外はmerge-treeへ +merge-rotate-right : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-right record { vart = bt-node record { key = record { coler = y ; number = x } + ; ltree = (bt-node record { key = record { coler = ly ; number = lx } ; ltree = ll ; rtree = lr }) + ; rtree = r } + ; varn = varn ; varl = varl } next exit + = next record { vart = bt-node record { key = record { coler = y ; number = lx } + ; ltree = ll + ; rtree = (bt-node record { key = record { coler = red ; number = x } ; ltree = lr; rtree = r }) } + ; varn = varn ; varl = varl } + + +-- split +split-branch : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +split-branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node₁) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = red ; number = number₁ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree₁ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key₁ + ; ltree = (bt-node record { key = record { coler = red ; number = number₁ } + ; ltree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree₁ }) + ; rtree = lr }) + ; rtree = rtree } + ; varn = varn ; varl = varl } next exit + = next node + + +-- 左回転、exitはsplit_branchへ　nextもsplit_branchへ +merge-rotate-left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit + = next record { vart = bt-node record { key = record { coler = y ; number = rx } + 　　; ltree = (bt-node record { key = record { coler = red ; number = x } ; ltree = l ; rtree = rl }) + 　　; rtree = rr} + 　　; varn = varn ; varl = varl } + + +-- skew exitがsplitへ　nextが左回転 +skew-bt : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +skew-bt node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +skew-bt node@record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node +skew-bt node@record { vart = (bt-node record { key = key₁ + ; ltree = ltree₁ + ; rtree = (bt-node record { key = record { coler = black ; number = number } + ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit + = exit node +skew-bt node@record { vart = (bt-node record { key = key₁ + ; ltree = ltree₁ + ; rtree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree }) }) + ; varn = varn ; varl = varl } next exit + = next node + + +set-node-coler : Env → Env +set-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node +set-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } + = record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } + +init-node-coler : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +init-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit + = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } + +--修正前 +merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node +merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty ∷ varl₁) } next exit = exit node + +merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit with <-cmp varn number + +merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri≈ ¬a b ¬c + = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl₁ } + +merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri> ¬a ¬b c + = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = vart }) ; varn = number ; varl = varl₁ } + +merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c + = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ } + +--修正後 +merge-tree1 : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +merge-tree1 env next exit with varl env +... | [] = exit env +... | bt-empty ∷ nl = exit env +... | bt-node node₁ ∷ nl with <-cmp (varn env) (number ( key node₁ )) +... | tri≈ ¬a b ¬c = next (record env { varn = number (key node₁) ; varl = nl }) +-- next (record{ vart = vart env ; varn = number (key node₁) ; varl = nl }) +... | tri> ¬a ¬b c = next (record env { vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl }) +-- next (record{ vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl }) +... | tri< a ¬b ¬c = next (record{ vart = (bt-node record { key = key node₁ ; ltree = vart env ; rtree = rtree node₁ }) ; varn = number (key node₁) ; varl = nl }) + +-- insert +bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +-- mergeへ遷移する +bt-insert (record { vart = bt-empty ; varn = varn ; varl = varl }) next exit + = exit (record { vart = (bt-node (record { key = record { coler = red ; number = varn }; ltree = bt-empty; rtree = bt-empty })) ; varn = varn ; varl = varl }) + +-- 場合分けを行う +bt-insert record {vart = (bt-node record { key = record { coler = y; number = x } ; ltree = ltree ; rtree = rtree }) ; varn = n ; varl = varl } next exit with <-cmp x n +bt-insert node@(record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } ) next exit | tri≈ ¬a b ¬c + = exit node + +bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri> ¬a ¬b c + = next (record {vart = ltree ; varn = varn ; varl = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ∷ varl }) + +bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c + = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl }) + + + +-- normal loop without termination +{-# TERMINATING #-} +insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +insert env exit = bt-insert env (λ env → insert env exit ) exit + + + +init-col : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +init-col env exit = init-node-coler env exit exit + +{- +{-# TERMINATING #-} +merge : {l : Level} {t : Set l} → Env → (exit : Env → t) → t + +{-# TERMINATING #-} +split-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +split-p env exit = split env (λ env → merge env (λ env → merge env exit ) ) exit + +{-# TERMINATING #-} +rotate_right : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +rotate_right env exit = merge-rotate-right env (λ env → split-p env (λ env → merge env exit ) ) exit + +{-# TERMINATING #-} +split-b : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +split-b env exit = split-branch env (λ env → rotate_right env exit ) λ env → merge env exit + +{-# TERMINATING #-} +rotate_left : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +rotate_left env exit = merge-rotate-left env (λ env → split-b env exit ) exit + +{-# TERMINATING #-} +skew : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +skew env exit = skew-bt env (λ env → rotate_left env (λ env → split-b env exit ) ) exit + +merge env exit = merge-tree env (λ env → skew env exit ) exit +-} +-- skewはnextがrotate-right。exitはsplitとなる +-- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する +-- それはskewのexitと等しいので同時に記述してやる。 +skew' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +skew' env exit = skew-bt env (λ env → merge-rotate-left env exit exit ) exit + +split' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +split' env exit = split-branch env (λ env → merge-rotate-right env (λ env → split env exit exit ) (λ env → split env exit exit ) ) exit + + +{- +merge' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node +merge' node@record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = merge' (merge-tree node (λ env → skew' env (λ env → split' env (λ env → env) ) ) (λ env → env) ) exit +-} + +whileTestP : {l : Level} {t : Set l} → (tree : rbt) → (n : ℕ) → (Code : Env → t) → t +whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } ) + + + +{-# TERMINATING #-} +mergeP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit + +{- +mergeP1 : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!} +mergeP1 record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = {!!} +-} + +{- +merge-tree env + (λ env → skew-bt env + (λ env → merge-rotate-left env + (λ env → split-branch env + (λ env → merge-rotate-right env + (λ env → split env (λ env → mergeP env exit ) (λ env → mergeP env exit ) ) exit) + (λ env → mergeP env exit ) ) + exit ) + exit ) exit +-} + +--whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (c11 : ℕ) → (Code : Envc → t) → t +--whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } ) + +--whileTestPCall : (tree : rbt) → (n : ℕ) → Env +--whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env → init-col env (λ env → env ) ) ) ) + +whileTestPCall' : (tree : rbt) → (n : ℕ) → Env +whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) ) + + +-- 以下test部分 +test1 = whileTestPCall' bt-empty 8 +test2 = whileTestPCall' (vart test1) 10 +test3 = whileTestPCall' (vart test2) 24 +test4 = whileTestPCall' (vart test3) 31 +test5 = whileTestPCall' (vart test4) 41 +test6 = whileTestPCall' (vart test5) 45 +test7 = whileTestPCall' (vart test6) 50 +test8 = whileTestPCall' (vart test7) 59 +test9 = whileTestPCall' (vart test8) 73 +test10 = whileTestPCall' (vart test9) 74 +test11 = whileTestPCall' (vart test10) 79 + diff -r bb7e9eaf9df8 -r e5248199c73d paper/tex/cbc_agda.tex --- a/paper/tex/cbc_agda.tex Fri Feb 12 18:02:24 2021 +0900 +++ b/paper/tex/cbc_agda.tex Sat Feb 13 00:30:44 2021 +0900 @@ -6,7 +6,7 @@ その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。 これらを用いて Hoare Logic によりプログラムの検証を行いたい。 -\subsection{CbC記法で書くagda} +\subsection{GearsAgda 形式で書く agda} Agdaでは関数の再帰呼び出しが可能であるが、CbCでは値が 帰って来ない。そのためAgda で実装を行う際には再帰呼び出しを行わないようにする。 \coderef{agda-cg}が例となるコードである。 diff -r bb7e9eaf9df8 -r e5248199c73d paper/tex/intro.tex --- a/paper/tex/intro.tex Fri Feb 12 18:02:24 2021 +0900 +++ b/paper/tex/intro.tex Sat Feb 13 00:30:44 2021 +0900 @@ -1,4 +1,4 @@ -\chapter{はじめに} +\chapter{プログラミング言語の検証} \pagenumbering{arabic} OSやアプリケーションの信頼性を高めることは重要な課題である。 @@ -10,7 +10,7 @@ 継続を導入した C言語の下位言語である。 その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。 -\section{研究目的} +%\section{研究目的} 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。 Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、 事後条件が成り立つことでコマンドの検証を行う。 diff -r bb7e9eaf9df8 -r e5248199c73d slide/slide.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/slide.html Sat Feb 13 00:30:44 2021 +0900 @@ -0,0 +1,1290 @@ +コンテナ技術を用いた教育情報システムの構築
+

コンテナ技術を用いた教育情報システムの構築

+
    +
  • 宮平 賢 +
      +
    • 琉球大学工学部工学科知能情報コース
      • +
    +
    • +
  • 河野 真治 +
      +
    • 琉球大学工学部
      • +
    +
    • +
+
+
+

研究目的

+
    +
  • 情報通信技術の普及に伴い学ぶことが増えている
    • +
  • その学習環境として、Virtual MachineやContainerがある +
      +
    • 高性能なPC
      • +
    • クラウドサービス +
        +
      • 無料だと制限がある
        • +
      +
      • +
    +
    • +
+
+
+

これまでの学生向け学習環境

+
    +
  • +

    VM貸出サービス

    +
      +
    • Akatsuki +
        +
      • 申請を行い、Webコントロールパネルから作成
        • +
      +
      • +
    • ie-virsh +
        +
      • 手元のPCで作成したVMイメージのデプロイ
        • +
      +
      • +
    +
    • +
  • +

    VM貸出サービスのデフォルトスペック

    +
      +
    • CPU 1コア
      • +
    • メモリ 1GB
      • +
    • ディスク容量 10GB
      • +
    +
    • +
+
+
+

これまでの学習環境の問題点

+
    +
  • VM貸出サービスの一部学生は申請の方法が分からなかったり、貸出サービスがあることが周知されていなかったため、旧システムのリソースが余っていた
    • +
+
+
    +
  • VMのスペックの変更にはシステム管理チームへの申請が必要であり、利用者と管理者とのやり取りなどの手間があった
    • +
+
+
    +
  • 旧システムにはGPUが搭載されていないため、貸出サービスではなく研究室ごとの機器、クラウドサービスが多く利用された
    • +
+
+
+

教育情報システムの構築

+
+
+

オンプレミス環境

+
    +
  • 汎用サーバ x 4
    • +
  • ディスクサーバ x 2
    • +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
CPUIntel Xeon Gold 6238 (2.10GHz/22Core)
GPUNvidia Tesla V100S
メモリ512GB
SAS SSD5TB
NVMe SSD1.5TB
+
+
+

VM貸出サービスの移行

+
    +
  • VM貸出サービスを継続するため、KVMを導入する
    • +
  • VMからGPUの利用にはPCIパススルーの設定が必要となる
    • +
  • しかし、VM1つに対し、1つのGPUが必要になる +
      +
    • 希望する学生全員に割り当てができない
      • +
    +
    • +
+
+
    +
  • そこで、コンテナ環境を導入する +
      +
    • 1つのGPUを複数のコンテナから利用できる
      • +
    +
    • +
+
+
+

コンテナ環境の導入

+
    +
  • 要件としてマルチユーザであり、GPUが利用できるなどがある
    • +
  • そこで、Podman、Singularityを導入する
    • +
  • Podman +
      +
    • rootlessで利用できる
      • +
    • nvidia-dockerの設定を行えばGPUを利用できる
      • +
    +
    • +
  • Singularity +
      +
    • rootlessで利用できる
      • +
    • GPUの利用が容易 +
        +
      • GPUドライバーのインストールのみ
        • +
      +
      • +
    +
    • +
+
+
+

コンテナエンジンの補い

+
    +
  • +

    Podman

    +
      +
    • イメージの作成やコンテナの作成が遅い +
        +
      • Podmanがまだ開発段階
        • +
      +
      • +
    • rootlessでは実行できない機能がある +
        +
      • IPアドレスの割り当て
        • +
      +
      • +
    +
    • +
  • +

    Singularity

    +
      +
    • イメージの作成に時間がかかる +
        +
      • ビルド中にエラーが発生すると、一から再開する必要がある
        • +
      +
      • +
    +
    • +
  • +

    そこでPodmanのwrapperであるie-podmanを作成した

    +
    • +
+
+
+

ie-podmanの作成

+
    +
  • ユーザのUID、GIDを取得し管理を行う +
      +
    • 他のユーザのリソースを操作できない
      • +
    +
    • +
  • SSD上にイメージ等を保存し、高速を図る
    • +
+
+
+

ie-podmanの機能 1/2

+
    +
  • Podmanのすべての機能をwrappするのではなく、一部機能のみを提供する
    • +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
コマンド機能
buildContainerfileの指示に従いイメージを作成する
cpコンテナにファイルを送信する
exec起動中のコンテナでプロセスを実行する
imagesコンテナイメージの一覧を表示する
infoコンテナの情報を表示する
logsコンテナのlogを表示する
ps起動中のコンテナの一覧を表示する
+
+
+

ie-podmanの機能 2/2

+
    +
  • registryやsifなど独自機能を提供する
    • +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
コマンド機能
registry学科のレジストリの操作を行う
rmコンテナを削除する
runコンテナを作成する
sifイメージをsifファイルに変換する
startコンテナを起動する
stopコンテナを停止する
+
+
+

ジョブスケジューラの導入

+
    +
  • 多くのリソースを必要とするプログラムは管理が必要である
    • +
  • 4台のサーバのリソースを利用できるようにする必要がある
    • +
  • そこで、ジョブスケジューラのSlurmを採用する +
      +
    • フォールトトレラントで拡張性が高い
      • +
    +
    • +
+
+
+

ジョブスケジューラの構築

+

利用方針 「計算リソースの利用効率を上げる」

+
    +
  • Jobの優先順位 +
      +
    • 要求するリソースの少ないJobの優先度を高くする
      • +
    • 実行時間が短いJobの優先度を高くする
      • +
    • これまでのJobの実行履歴で優先度は変化しない
      • +
    +
    • +
+

これでは多くのリソースを要求するJobが実行されない可能性がある。

+
    +
  • Jobの実行時間 +
      +
    • Jobの実行時間の記載がない場合は1日で強制終了させる
      • +
    • 管理者からJobの優先度を上げる
      • +
    +
    • +
+

また、Jobのスケジュールにはバックフィルを採用する。

+
+
+

+
+
+

ファイルシステムの導入

+
    +
  • Cephを採用 +
      +
    • 自己修復、自己管理機能を搭載するため信頼性が高い
      • +
    • 柔軟なアクセス方法の提供 +
        +
      • Object Gateway
        • +
      • ブロックデバイス
        • +
      • POSIX互換のファイルシステム
        • +
      +
      • +
    +
    • +
+
+
+

教育情報システムの構成

+
    +
  • 汎用サーバ全てにKVM、Podman、Singularityをインストール
    • +
  • Slurm +
      +
    • 汎用サーバ1台をコントローラ/計算ノード
      • +
    • 残りを計算ノード
      • +
    +
    • +
  • Ceph +
      +
    • ディスクサーバをOSD
      • +
    • 汎用サーバ3台をMON, MDS, MGR
      • +
    +
    • +
+
+
+
+

教育情報システムの利用と管理

+
+
+

VM貸出サービスの利用

+
    +
  • VMの作成、スペックの変更で申請が必要なくなった
    • +
  • VMの作成 +
      +
    • ie-virsh define --template Ubuntu-20 VM_NAME
      • +
    +
    • +
  • スペックの変更 +
      +
    • ie-virsh edit VM_NAME
      • +
    +
    • +
+
+
+

ie-podmanの使用方法

+
    +
  • PodmanはDockerと同じCLIを提供している
    • +
  • IPアドレス、GPUをコンテナへ割り当てられる +
      +
    • ie-podman run --ip --gpu [IMAGE_NAME]
      • +
    +
    • +
  • 作成したイメージをsifファイルへの変換に対応 +
      +
    • ie-podman sif [IMAGE_NAME]
      • +
    +
    • +
+
+
+

GPUの利用方法

+
    +
  • Singularityでは容易にGPUを利用できる +
      +
    • singularity run --nv [SIF_NAME]
      • +
    +
    • +
  • ホームディレクトリ、/tmpなどがコンテナにマウントされる +
      +
    • プログラムの実行に便利
      • +
    +
    • +
  • SlurmによるJob管理 +
      +
    • 必要なリソースを記述し投下する
      • +
    • CPU数、GPU数
      • +
    +
    • +
+
+
+

batchファイルの例

+
    +
  • Jobに必要とするリソース +
      +
    • CPU 8コア、GPU 1つ
      • +
    +
    • +
  • Jobの実行時間 +
      +
    • 1分
      • +
    +
    • +
+
#!/bin/bash
+#SBATCH --job-name sample
+#SBATCH --output logs/%x-%j.log
+#SBATCH --error logs/%x-%j.err
+#SBATCH --nodes 1
+#SBATCH --cpus-per-task 8
+#SBATCH --gpus tesla:1
+#SBATCH --time 01:00
+
+singularity exec --nv [SIF_NAME] [COMMANDS]
+
+
+
+

教育情報システムの評価

+
+
+

ファイルシステムの評価 1/2

+
    +
  • +

    実験概要

    +
      +
    • ddコマンドを使用し書き込み速度を比較する
      • +
    +
    • +
  • +

    書き込み速度の比較

    +
      +
    • GFS2
      • +
    • NFS
      • +
    • CephFS
      • +
    • CephRBD
      • +
    +
    • +
+
+
+

ファイルシステムの評価 2/2

+
+
+

ie-podmanの評価 1/3

+
    +
  • +

    実験環境

    +
      +
    • 新システムの汎用サーバで実施
      • +
    +
    • +
  • +

    実験概要

    +
      +
    • イメージのBuild速度を比較する
      • +
    +
    • +
  • +

    Build速度の比較

    +
      +
    • Docker
      • +
    • Podman (rootless)
      • +
    • ie-podman
      • +
    +
    • +
+
+
+

ie-podmanの評価 2/3

+
FROM ubuntu:18.04
+RUN apt-get update && \
+    apt-get upgrade -y && \
+    DEBIAN_FRONTEND=noninteractive \
+    apt-get install -y \
+	qemu-utils qemu-efi-aarch64 \
+	qemu-system-arm qemu-system-x86 \
+	build-essential uuid-dev \
+	git python iasl wget vim nasm && \
+    DEBIAN_FRONTEND=noninteractive \
+    apt-get install -y \
+	crossbuild-essential-armhf
+
+WORKDIR /workdir
+RUN git clone --recursive https://github.com/tianocore/edk2 && \
+    wget https://sourceforge.net/projects/gnu-efi/files/gnu-efi-3.0.12.tar.bz2/download && \
+    tar xf download
+
+
+
+

ie-podmanの評価 3/3

+
+
+

学習環境の評価

+
    +
  • VM +
      +
    • 学生が自由にスペックを変更できる
      • +
    • ディスク容量を抑えれる
      • +
    +
    • +
  • コンテナ +
      +
    • 気軽に利用できる
      • +
    • 高性能な実況環境を利用できる
      • +
    +
    • +
+
+
+

まとめ

+
+
+

今後の課題

+
    +
  • 教育情報システムの周知 +
      +
    • Jobの投下やリソースの要求方法
      • +
    • ie-virsh、ie-podmanの使用方法
      • +
    • 定期的な周知が必要
      • +
    +
    • +
  • ie-podmanのネットワーク構成の見直し +
      +
    • プレフィックス長が24のため、最大254個のIPアドレス
      • +
    • コンテナを停止で使用されない場合は削除する必要がある
      • +
    +
    • +
  • バックアップの運用 +
      +
    • Cephと専用サーバ以外のバックアップ先を用意する必要がある
      • +
    +
    • +
+
+
\ No newline at end of file diff -r bb7e9eaf9df8 -r e5248199c73d slide/slide.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/slide.md Sat Feb 13 00:30:44 2021 +0900 @@ -0,0 +1,74 @@ +--- +marp: false +title: Geas Agda による Left Learning Red Black Tree の検証 +paginate: true + +theme: default +size: 16:9 +style: | + section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Arial", "Hiragino Maru Gothic ProN"; + } + + section.title { + font-size: 40px; + padding: 40px; + } + section.title h1 { + text-align: center; + } + + section.slide h1 { + position: absolute; + left: 50px; top: 35px; + } + +--- + +# Geas Agda による Left Learning Red Black Tree の検証 + +- 上地 悠斗 + - 琉球大学工学部工学科知能情報コース +- 河野 真治 + - 琉球大学工学部 + +--- + +# 証明を用いたプログラムの信頼性の向上を目指す + + + +--- + +# これまでの成果 + +- Gears Agda +- Gears Agda による Hoare Logic を用いた簡単なプログラムの検証 +- Gears Agda で実装したRed Black Tree + +--- +# 今回の成果 + +- Left Lerning Red Black Tree の実装 +- (delete) 誰もやろうとしていなかった +- 証明付き Data 構造を用いた List による性質の記述 + +--- +# Agdaの紹介 + +--- +# gears Agda + +--- +# llrbt + +--- +# delete + +--- +# Left Lerning Red Black Tree の実装 + +---