Mercurial > hg > Gears > GearsAgda
annotate Todo.txt @ 819:66726208b9f4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Jan 2024 17:03:59 +0900 |
| parents | 2955d5b7debd |
| children | 91137bc52ddd |
| rev | line source |
|---|---|
| 780 | 1 Mon Jul 3 19:04:29 JST 2023 |
| 2 | |
| 3 Red Black Tree の Invariant を完成させる | |
| 4 GearsOS のコードとの対応を取る (既にバグがあることがわかってる) | |
| 5 | |
| 6 バグはメタ部分にある | |
| 7 pointer (CbCはCだから pointer がある) | |
| 8 heap (CbCは GC もってない。なので、メモリリークしてる) | |
| 9 | |
| 10 Meta計算部分を含む Invariant になる | |
| 11 | |
| 12 ここまで複雑で実用になる? | |
| 13 | |
| 14 部分ではそんなに難しくはない? | |
| 15 | |
| 710 | 16 Wed May 4 22:07:32 JST 2022 |
| 17 | |
| 18 Context memory に DataGear を Binary Tree で入れる。List で良いのだが | |
| 19 Libaryの Data.Tree.Binary には insert はない ( まぁ、alloc / read / update くらいで map で書けるとか?) | |
| 20 共有データは、memory に入れる | |
| 21 free はしない(?) | |
| 22 | |
| 709 | 23 Sun May 1 15:04:57 JST 2022 |
| 24 | |
| 25 Model checking | |
| 26 | |
| 27 goto 先の番号を stub に書くのは変 | |
| 28 | |
| 29 process : context が別々 | |
| 30 thread : context 一緒、goto 先が異なる | |
| 31 context は共有 実行は codeGear は atomic | |
| 32 shared file descriptor など | |
| 33 | |
| 34 single phils direct connection single thread | |
| 35 no shared data | |
| 36 | |
| 37 multi process phils separate process | |
| 38 shared context | |
| 39 | |
| 40 multi threaded phils shared process | |
| 41 serate next | |
| 42 atomic codeGear execution | |
| 43 | |
| 44 | |
|
578
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
45 Thu May 17 15:26:56 JST 2018 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
46 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
47 findNode -> replaceNode -> getRedBlackTree だが |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
48 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
49 findNode -> P0 -> replaceNode -> P1 -> getRedBlackTree |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
50 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
51 という形で証明しても良い。一挙に証明するのは,可能だろうけど、良くないはず。 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
52 |
| 573 | 53 Sun May 6 17:54:50 JST 2018 |
| 54 | |
| 55 do1 a $ \b -> do2 b next を、do1 と do2 に分離することはできる? | |
| 56 | |
| 57 | |
| 58 Mon Apr 30 17:15:16 JST 2018 | |
| 59 | |
| 60 Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない | |
| 61 やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい | |
| 62 | |
| 553 | 63 Mon Mar 26 17:43:06 JST 2018 |
| 64 | |
| 573 | 65 Decidable を使って Compare の場合分けを行う |
| 553 | 66 Decidable を使うと Eq から x ≡ y の証明を取り出すことができる |
| 67 場合分けには Trichotomous を使う | |
| 573 | 68 compareTri を完成させる Done |
| 553 | 69 |
| 524 | 70 Fri Jan 5 16:43:26 JST 2018 |
| 71 | |
| 72 unbalanced binary search tree の動作を調べる | |
| 73 | |
| 74 RedBlackTree の put を完成させる | |
| 75 | |
| 76 RedBlackTree の Deletion を完成させる | |
| 77 | |
| 78 unbalanced binary search tree と同様の動作をする | |
| 79 | |
| 80 木の深さの最小と最大の差が２倍を超えない | |
| 81 | |
| 82 CodeGear/DataGear が構成する圏を定義する | |
| 83 | |
| 84 goto を定義して meta 計算を可能にする | |
| 85 | |
| 86 DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする | |
| 87 | |
| 88 実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する | |
| 89 | |
| 90 Monad の合成に必要な規則を上の圏上に定義する | |
| 91 | |
| 92 synchronizedQueue の仕様をCTLを使って定義する | |
| 93 | |
| 94 Gearsで記述したsynchornizedQueueを検証する | |
| 95 | |
| 96 gotoを用いてモデル検査と証明の組み合わせを実現する | |
| 97 | |
| 98 | |
| 575 | 99 Wed Aug 27 17:52:00 JST 2019 |
| 100 | |
| 101 別で定義した TriCotomos や \=? などの Relation の関数を | |
| 102 Agdaで定義してあるものに置き換える,まとめる | |
| 103 | |
| 104 HoareLogic をベースにした SingleLinkedStack の作成 | |
| 105 | |
| 106 HoareLogic ベースの Tree の証明 |