GearsOS と gearsAgda 上の
モデル検査について

河野真治
琉球大学工学部

発表の概要

 Reflection のための言語 Continuation based C (2000年)
 Gears OS 
 gearsAgda
 gearsAgdaをつかったプログラムの証明 
 gearsAgda上のモデル検査
  

GearsOSの歴史

 Reflection のための言語 Continuation based C (2000年)
 gcc版 (2009年)
 llvm版 (2013年)
 Gears OS (2015年)
 Model Checking on Gears OS (2021年)
 gearsAgda (2018年)
 Binary Tree の証明 (2021年)
 Red Binary Tree の証明 (2021年)
 gearsAgdaでのModel Checking (2024年)

Continuation based C (CbC)

 Reflcationを使った file system を作る
 言語には xscheme を使って multi thread にしよう
 xscheme は stack を heap に取っている
 Reflection には stack が邪魔

だったら、stack をなくそう

codeGear

  __code f(struct input) { goto input->next(output); }

goto なのでstackは使わない。単に接続される code の一片

CbC の実装系

Micro C な CbC (2000年)

    さきがけで採用

GCC baed な CbC (2009年)

    goto を　tail callで実装する
    Cに戻るには nested function を使う

Clang/LLVM baed な CbC (2013年)

    Cに戻るには buildin setjmp を使う

GearsOS

で、大きなプログラムを作れるようになった

 code をsegmentedにするだけではなく、dataも segmentedになる
 TaskManager が codeGear を context を使って抽象化して
 scheduler と worker で実行する

Context

 GearsOSのProcess。single thread である
 すべての Process 内の code と data を id で管理している
 Context から stub で data を抜き出して、実行し、goto で戻る
 stub または goto 文の時点で Reflection の操作を行う

Context

これが、すべてCbCで記述されている

Model Checker

 codeGear の goto を上書きして、そこでモデル検査を行うことができる
 書き換えはパターンマッチで行う
 Dining Philosophers の例を実行できた

Agda と圏論

2013に圏論と Curry Howard logic を学ぶ

  Hihger order categorical logic
  Proofs and Types

両方とも Sony CSL 時代に手に入れた本。80年代

Agda と数学

以下のことを Agda で証明付きで理解できる

  圏論
  ZF集合論
  Galois理論
  Automaton

gearsAgda

agda による CbC の形式化

   code : {t : Set } → Input → (Output → t )

という形式を使う

これに対応したλ計算を作れるかもしれないし、作れないかもしれない

gearsAgdaによるプログラムの証明

   code : {t : Set } → Input → Pre → (Output → Post → t )

Hoare logic になるように、Pre condition と Post condition をつける

これは普通の codeGear であり、メタなデータが引数として付加されている

gearsAgdaによるプログラムの証明 (Loop connector)

codeGearには、loop は継続を呼び出すことで実現される

これを loop にするには、CbCでは問題ないが、Agda の場合は終了条件が必要になる。

TerminatingLoopS

  TerminatingLoopS :  {t : Set } (Index : Set  ) 
     → {Invraiant : Index → Set  } → ( reduce : Index → ℕ)
   → (r : Index) → (p : Invraiant r)
   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  
      → Invraiant r1 → reduce r1 < reduce r  → t ) → t) 
   → t

これはinductionの命題であり、実際にAgdaで証明される。

gearsAgda によるプログラムの証明

 Hoare logic のinvariantを用意すると、プログラムの証明が可能になる。

BTree

  Binary Tree の証明
  treeInvariant 2分木の性質
  stackInvariant 木をたどるstackの性質
  replacedTree 木の置き換え

gearsAgda による赤黒木の証明

RBTree

  赤黒木の証明
  RBtreeInvariant 赤黒木の深さと色の性質
  replacedRBTree 木の置き換え

gearsAgda上のモデル検査

 geasAgdaで記述したcodeGearを抽象化して、Schedulerを作る
 それを shuffle して実行する
 システム全体の Invariant を記述する
 Index は状態の数になる

eventuality (Buchi automaton)

[]<> p などの Eventuality の記述にはω Automatonである Buchi automaton を用いる

 ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → Q →  ( ℕ → Σ )  → ( ℕ → Q )
 ω-run Ω x s zero = x
 ω-run Ω x s (suc n) = δ Ω (ω-run Ω x s n) ( s n )
 record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) 
  ( S : ℕ → Σ ) : Set where
   field
    next     : (n : ℕ ) → ℕ
    infinite : (x : Q) → (n : ℕ ) 
     →  aend Ω ( ω-run Ω x  S (n + (suc (next n)))) ≡ true
                       not p
                   ------------>
        [] <> p *                 [] <> p
                   <-----------
                       p

Model Checkingの構成

以下の r を List Context として、Invariant をつくればよい

  ModelChecking :  {t : Set } (Index : Set  ) 
     → {Invraiant : Index → Set  } → ( reduce : Index → ℕ)
   → (r : Index) → (p : Invraiant r)
   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  
      → Invraiant r1 → reduce r1 < reduce r  → t ) → t) 
   → t

まだ、できてません

今後の展開

 二分木や赤黒木の削除
 二分木や赤黒木のより詳細な証明 (並行性、メモリ)
 モデル検査の実装
 Agdaの展開
 Gears OSのgearsAgdaによる証明