Mercurial > hg > Gears > GearsAgda

Mon Jul  3 19:04:29 JST 2023

    Red Black Tree の Invariant を完成させる
    GearsOS のコードとの対応を取る (既にバグがあることがわかってる)

    バグはメタ部分にある
    　　pointer    (CbCはCだから pointer がある)
        heap       (CbCは GC もってない。なので、メモリリークしてる)

    Meta計算部分を含む Invariant になる

    ここまで複雑で実用になる?

      部分ではそんなに難しくはない?

Wed May  4 22:07:32 JST 2022

    Context memory に DataGear を Binary Tree で入れる。List で良いのだが
    Libaryの Data.Tree.Binary には insert はない ( まぁ、alloc / read / update くらいで map で書けるとか?)
    共有データは、memory に入れる
    free はしない(?)

Sun May  1 15:04:57 JST 2022

    Model checking

    goto 先の番号を stub に書くのは変

　　process : context が別々
　　thread  : context 一緒、goto 先が異なる
              context は共有 実行は codeGear は atomic
    shared    file descriptor など

    single phils    direct connection single thread
                    no shared data

    multi process phils    separate process
                           shared context

    multi threaded phils   shared process
                           serate next
                           atomic codeGear execution


Thu May 17 15:26:56 JST 2018

    findNode -> replaceNode -> getRedBlackTree だが

        findNode -> P0 -> replaceNode -> P1 -> getRedBlackTree

   という形で証明しても良い。一挙に証明するのは,可能だろうけど、良くないはず。

Sun May  6 17:54:50 JST 2018

    do1 a $ \b ->  do2 b next を、do1 と do2  に分離することはできる?


Mon Apr 30 17:15:16 JST 2018

    Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない
    やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい

Mon Mar 26 17:43:06 JST 2018

    Decidable を使って Compare の場合分けを行う
    Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
    場合分けには Trichotomous を使う
    compareTri を完成させる    Done

Fri Jan  5 16:43:26 JST 2018

    unbalanced binary search tree の動作を調べる

    RedBlackTree の put を完成させる

    RedBlackTree の Deletion を完成させる

                 unbalanced binary search tree と同様の動作をする

                  木の深さの最小と最大の差が２倍を超えない

    CodeGear/DataGear が構成する圏を定義する

    goto を定義して meta 計算を可能にする

    DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする

    実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する

    Monad の合成に必要な規則を上の圏上に定義する

    synchronizedQueue の仕様をCTLを使って定義する

    Gearsで記述したsynchornizedQueueを検証する

    gotoを用いてモデル検査と証明の組み合わせを実現する


Wed Aug 27 17:52:00 JST 2019

    別で定義した TriCotomos や \=? などの Relation の関数を
    Agdaで定義してあるものに置き換える,まとめる

    HoareLogic をベースにした SingleLinkedStack の作成

    HoareLogic ベースの Tree の証明
author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 06 Apr 2024 18:19:23 +0900
parents	2955d5b7debd
children