メタ計算を用いた Continuation based C の検証手法
Yasutaka Higa

プログラミング言語とソフトウェアの信頼性

二つのアプローチを用いたソフトウェア検証

モデル検査的アプローチについての流れ

既存のモデル検査器 spin

assert(x < 10);

既存のモデル検査器 CBMC

assert(x < 10);

Continuation based C

CodeSegment

cs

__code cs0(int a, int b){
  goto cs1(a+b);
}

DataSegment

ds

__code cs0(int a, int b){
  goto cs1(a+b);
}

メタ計算

meta

Meta CodeSegment

mcs

Meta DataSegment

mds

並列に信頼性高く動作する GearsOS

赤黒木

rbtree

GearsOS における赤黒木の利用例(ノードの挿入)

put

goto meta(context, Put);

仕様の記述とその確認

チェックする仕様

__code verifySpecificationFinish(struct Context* context) {
    if (context->data[AkashaInfo]->akashaInfo.maxHeight >
        2*context->data[AkashaInfo]->akashaInfo.minHeight)
    {
        context->next = Exit;
        goto meta(context, ShowTrace);
    }
    goto meta(context, DuplicateIterator);
}

メタ計算ライブラリ akasha

akashaPut

akasha と CBMC の比較

定理証明を Continuation based C へ適用するには

Agda における証明

f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C)
f = \p x -> (snd p) ((fst p) x)

Agda における等式の証明

addSym : (n m : Nat) -> n + m ≡ m + n
addSym O       O   = refl
addSym O    (S m)  = cong S (addSym O m)
addSym (S n)   O   = cong S (addSym n O)
addSym (S n) (S m) = begin
  (S n) + (S m)  ≡⟨ refl ⟩
  S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
  S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
  S (m + S n)    ≡⟨ refl ⟩
  (S m) + (S n)  ∎

Agda と DataSegment

__code cs0(int a, int b){
  goto cs1(a+b);
}

record ds0 : Set where
  field
    a : Int
    b : Int

Agda と CodeSegment

__code cs0(int a, int b){
  goto cs1(a+b);
}

data CodeSegment (A B : Set) : Set where
  cs : (A -> B) -> CodeSegment A B

cs0 : CodeSegment ds0 ds1
cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))

メタレベルの型付け

Agda 上のメタ計算

cs0 : CodeSegment ds0 ds1
cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))

main : ds1
main = goto cs0 (record {a = 100 ; b = 50})

main : Meta
main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70})
                                 ; c' = 0 ; next = (N.cs id)})

Agda 上で証明できた性質

comp-associative : > (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
                   -> csComp  c (csComp b a) ≡ csComp  (csComp c b) a
comp-associative (cs _) (cs _) (cs _) = refl
-- c . (b . a) ≡ (c . b) . a

push-pop-type : ℕ -> ℕ  -> ℕ -> Element ℕ -> Set₁
push-pop-type n e x s = M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
-- goto (pop . push) mds ≡ mds

n-push-pop-type : ℕ ->  ℕ  -> ℕ -> SingleLinkedStack ℕ -> Set₁
n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop  n) (n-push n)) meta ≡ meta
-- goto (pop*n . push*n) mds ≡ mds

Agda 上に CbC を記述した成果

まとめ

今後の課題

発表履歴