Mercurial > hg > Papers > 2023 > moririn-sigos

view gearsAgda.html @ 4:854b01e2ce98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 17 Apr 2023 20:31:28 +0900
parents 170b950774a3
children
line wrap: on
line source

<html>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8">
<head>
<STYLE type="text/css">
.main { width:100%; }
.side { top:0px; width:0%; position:fixed; left:80%; display:none}
</STYLE>
<script type="text/javascript">
function showElement(layer){
    var myLayer = document.getElementById(layer);
    var main = document.getElementById('mmm');
    if(myLayer.style.display=="none"){
        myLayer.style.width="20%";
        main.style.width="80%";
        myLayer.style.display="block";
        myLayer.backgroundPosition="top";
    } else { 
        myLayer.style.width="0%";
        main.style.width="100%";
        myLayer.style.display="none";
    }
}
</script>
<script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
<script type="text/javascript" id="MathJax-script" async
  src="https://cdn.jsdelivr.net/npm/mathjax/es5/tex-chtml.js">
</script>
<title>GearsAgda : Meta continuation based Hoare Logic</title>
</head>
<body>
<div class="main" id="mmm">
<h1>GearsAgda : Meta continuation based Hoare Logic</h1>
<a href="#" left="0px" onclick="javascript:showElement('menu')">
<span>Menu</span>
</a>

<p>

<hr/>
<h2><a name="content000">Continuation based C and GearsAgda</a></h2>
goto 文中心に記述する。LLVM/GCC で実装されている。コンパイラの Basic block に相当する
<p>
C form
<pre>
    __code whileLoop(EnvPtr en, __code next(EnvPtr en)) {
        if ( 0 &gt;= en-&gt;varn )  goto next(en);
         else {
           en-&gt;varn = en-&gt;varn - 1;
           en-&gt;vari = en-&gt;vari + 1;
           goto whileLoop(en, next);
        }
    }

</pre>
Agda は pure fuctional な depedent type language。証明を記述できる。goto 文は、以下の形式で記述する。
<p>
Agda form
<p>

<pre>
    whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
    whileTest c10 next = next (record {varn = c10 ; vari = 0} )
    {-# 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
    test1 : Env
    test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))

</pre>
TERMINATING は停止性が確認できないことを示している。
<p>

<hr/>
<h2><a name="content001">Gears OS</a></h2>
CbC と dataGear で構成する OS。
<p>

<pre>
    __code putdown_rfork(struct PhilsImpl* phils, __code next(...)) {
        struct AtomicT_int* right_fork = phils-&gt;Rightfork;
        goto right_fork-&gt;set(-1, putdown_lfork);
    }

</pre>
をメタ計算で表すと、
<p>

<pre>
    __code putdown_rforkPhilsImpl_stub(struct Context* context) {
            PhilsImpl* phils = (PhilsImpl*)GearImpl(context, Phils, phils);
            enum Code next = Gearef(context, Phils)-&gt;next;
            goto putdown_rforkPhilsImpl(context, phils, next);
    }
    __code putdown_lforkPhilsImpl(struct Context *context,struct PhilsImpl* phils, enum Code next) {
        struct AtomicT_int* left_fork = phils-&gt;Leftfork;
        Gearef(context, AtomicT_int)-&gt;atomicT_int = (union Data*) left_fork;
        Gearef(context, AtomicT_int)-&gt;newData = -1;
        Gearef(context, AtomicT_int)-&gt;next = C_thinkingPhilsImpl;
        goto mcMeta(context, left_fork-&gt;set);
    }

</pre>
となる。メタレベルでは引数は context と次の codeGearの番号だけ。
<p>
GearsAgda でも、同様の実装ができる。
<p>
<img src="fig/meta_cg_dg.svg" width="80%" height="600">

<p>

<hr/>
<h2><a name="content002">Gears OSのモデル検査</a></h2>

<pre>
    __ncode mcMeta(struct Context* context, enum Code next) {
        context-&gt;next = next; // remember next Code Gear
        int found = visit_StateDB(out, &amp;mcti-&gt;state_db, &amp;out,mcWorker-&gt;visit);
        if (found) {
          while(!(list = takeNextIterator(mcWorker-&gt;task_iter))) {

</pre>
mcMeta で状態を記録し、非決定的な実行を網羅する。
<p>
<img src="fig/model_checking.svg" width="80%" height="600">

<p>

<hr/>
<h2><a name="content003">GearAgda の Hoare Logic</a></h2>

<pre>
    whileLoopSeg : {l : Level} {t : Set l} → {c10 :  ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
       → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 &lt; varn env → t) 
       → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t

</pre>
このように loop を Segment に切り出す。Pre condtion と Post condition が付いている。これは命題で証明する必要がある。(容易)
<p>

<pre>
    TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ)
       → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 &lt; reduce r  → t ) → t)
       → (r : Index) → (p : Invraiant r)  → t 
    TerminatingLoopS {_} {t} Index {Invraiant} reduce loop  r p with &lt;-cmp 0 (reduce r)
    ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) 
    ... | tri&lt; a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where 
        TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 &lt; suc j  → Invraiant r1 →  reduce r1 &lt; reduce r → t
        TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) 
        TerminatingLoop1 (suc j) r r1  n≤j p1 lt with &lt;-cmp (reduce r1) (suc j)
        ... | tri&lt; a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 
        ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 &lt; k ) b lt1 ) p2 lt1 )
        ... | tri&gt; ¬a ¬b c =  ⊥-elim ( nat-≤&gt; c n≤j )   

</pre>
減少列を使用して、停止性を保証する接続で停止性を含めて Hoare Logic による証明が可能。
<p>

<pre>
    whileTestSpec1 : (c10 : ℕ) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
    whileTestSpec1 _ _ x = tt

</pre>
仕様は、継続で入力として受ける。
<p>

<pre>
    proofGearsTermS : {c10 :  ℕ } → ⊤
    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 )) 

</pre>
これは、プログラムが証明を値として渡すので、実際に証明になっている。接続するだけでよい。
<p>

<hr/>
<h2><a name="content004">Gears OS による赤黒木のモデル検査</a></h2>
木ではなくループ構造を使う。ノードは子供を iterator で返す。これを前述のモデル検査器で調べる。
<p>
まだ、やってません。
<p>
赤黒木は実装済み。
<p>

<hr/>
<h2><a name="content005">GearsAgda による赤黒木の証明</a></h2>
まず、Binary Tree 
<p>

<pre>
    data bt {n : Level} (A : Set n) : Set n where
      leaf : bt A
      node :  (key : ℕ) → (value : A) →
        (left : bt A ) → (right : bt A ) → bt A
    bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
    bt-depth leaf = 0
    bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ ))

</pre>
普通のデータ構造
<p>

<pre>
    find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
               → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
    find key leaf st _ exit = exit leaf st
    find key (node key₁ v tree tree₁) st next exit with &lt;-cmp key key₁
    find key n st _ exit | tri≈ ¬a b ¬c = exit n st
    find key n@(node key₁ v tree tree₁) st next _ | tri&lt; a ¬b ¬c = next tree (n ∷ st)
    find key n@(node key₁ v tree tree₁) st next _ | tri&gt; ¬a ¬b c = next tree₁ (n ∷ st)
    {-# TERMINATING #-}
    find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A)  → (exit : bt A → List (bt A) → t) → t
    find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where
        find-loop1 : bt A → List (bt A) → t
        find-loop1 tree st = find key tree st find-loop1  exit
    insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t
    insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit 
    insertTest1 = insertTree leaf 1 1 (λ x → x )
    insertTest2 = insertTree insertTest1 2 1 (λ x → x )

</pre>
継続( GearsAgda 形式)を用いた実装。これに Hoare条件をつける。
<p>

<pre>
    findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
               →  treeInvariant tree ∧ stackInvariant key tree tree0 stack  
               → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 &lt; bt-depth tree   → t )
               → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t

</pre>
invariant はこんな感じ。
<p>

<pre>
    data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
        t-leaf : treeInvariant leaf 
        t-node  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key &lt; key₁) → (key₁ &lt; key₂)
           → treeInvariant (node key value t₁ t₂) 
           → treeInvariant (node key₂ value₂ t₃ t₄)
           → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 
    data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack  : List (bt A)) → Set n where
        s-nil : stackInvariant  key0 leaf leaf [] 
        s-right      : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left  : bt A} → {st : List (bt A)}
             → key &lt; key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st )  → stackInvariant key0 tree tree0 (tree  ∷ node key value left tree ∷ st ) 
        s-left      : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right  : bt A} → {st : List (bt A)}
             → key0 &lt; key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st )  → stackInvariant key0 tree tree0 (tree  ∷ node key value tree right ∷ st ) 
    data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (tree tree1 : bt A ) → Set n where

</pre>
簡単とは言えない。条件をrecord にまとめた方がよい。
<p>

<pre>
    record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where
       field
         tree0 : bt A
         ti : treeInvariant tree0
         si : stackInvariant key tree tree0 stack
         ci : C tree stack     -- data continuation
   

</pre>
ci はテストとか記述する部分。データの継続になっている。この部分をあとで追加できる。
<p>

<pre>
    containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree  → ⊤
    containsTree {n} {m} {A} {t} tree tree1 key value P RT =
       TerminatingLoopS (bt A ∧ List (bt A) )
         {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p))
                  ⟪ tree1 , []  ⟫ {!!}
           $ λ p P loop → findPPC key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )  
           $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where

</pre>
みたいな感じで証明する。
<p>

<pre>
    insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
    insertTreeSpec0 _ _ _ = tt

</pre>
仕様記述は、継続の入力で受ける。
<p>

<hr/>
<h2><a name="content006">GearsAgdaのモデル検査</a></h2>
GearsOS と同じように構成することにより、並列実行を simulation できる。モデル検査器そのものを Hoare Logic base で証明、あるいは、展開した(比較的膨大な)部分を全部証明する。あるいは、モデル検査を実行することにより並列分散プログラムを検証できるはず。
<p>

<hr/>
<h2><a name="content007">Invariant の種類</a></h2>

<pre>
    等式
    生成データを限定した data 記述
    減少列
    生成されるものの有限性
    P_1 -&gt; P_n
</div>
<ol class="side" id="menu">
GearsAgda : Meta continuation based Hoare Logic
<li><a href="#content000">  Continuation based C and GearsAgda</a>
<li><a href="#content001">  Gears OS</a>
<li><a href="#content002">  Gears OSのモデル検査</a>
<li><a href="#content003">  GearAgda の Hoare Logic</a>
<li><a href="#content004">  Gears OS による赤黒木のモデル検査</a>
<li><a href="#content005">  GearsAgda による赤黒木の証明</a>
<li><a href="#content006">  GearsAgdaのモデル検査</a>
<li><a href="#content007">  Invariant の種類</a>
</ol>

<hr/> Shinji KONO <kono@ie.u-ryukyu.ac.jp> /  Thu Jan  6 10:48:24 2022
</body></html>