Mercurial > hg > Document > Growi
changeset 28:36c9c8f982f0
backup 2021-01-21
| author | autobackup |
|---|---|
| date | Thu, 21 Jan 2021 00:10:03 +0900 |
| parents | 459b9fa6f047 |
| children | 0bd2a99a349e |
| files | user/anatofuz/note/2021/01/20.md user/soto/log/2020-12-01.md user/soto/log/2021-01-19.md user/soto/log/untitled.md user/tobiuo.md |
| diffstat | 5 files changed, 229 insertions(+), 122 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/anatofuz/note/2021/01/20.md Thu Jan 21 00:10:03 2021 +0900 @@ -0,0 +1,29 @@ + +``` + AtomicT { + int [ + [0] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h", + file_type "header", + impl "PhilsImpl", + interface "Phils", + in_type_name "PhilsImpl", + vname "Leftfork" + }, +``` + +- `AtomicT != in_type_name` + - この場合はフィールドの置換と型の置換 + + +``` + }, + [3] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c", + file_type "CbC", + impl "PhilsImpl", + interface "Phils", + in_type_name "AtomicT", + vname "left" + }, +```
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/soto/log/2020-12-01.md Thu Jan 21 00:10:03 2021 +0900 @@ -0,0 +1,75 @@ +# 研究目的 + +- OSやアプリケーションの信頼性を高めることは重要な課題である。 + +- 研究室でCbCという言語を開発している。その信頼性を証明したい。 + +- CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。 + +- プログラムの正当性を証明するためにHoare Logicという検証手法がある。これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。 + +- CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。 + +- これらのことから、Hoare Logicを用いてCbCを検証できるか実験していく。 + +- cbcはサブルーチンとスープ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。 + +- 先行研究ではCbCにおけるWhileLoopの検証を行なった。 + +- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う + +## 今週の進捗 +- continuationなLLRB-Treeのinsertを若干修正 + - あまりよろしく無い実装をしていたのでそれを修正 + - ループ部分のterminationは外せなさそう(外す際にその部分で実装を行わないといけなくなり、意味が変わってくる) + +- nextとexitに投げるものに着いて悩んでいる + +- 水を購入 + +- ダージリンを設置 + +### 修正部分 + +```Agda +skew' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +skew' env exit = skew-bt env (λ env → merge-rotate-left env exit exit ) exit + +split' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +split' env exit = split-branch env (λ env → merge-rotate-right env (λ env → split env exit exit ) (λ env → split env exit exit ) ) exit + +{-# TERMINATING #-} +mergeP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit + +whileTestPCall' : (tree : rbt) → (n : ℕ) → Env +whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) ) +``` + +- skewとsplitの動作をまとめた +- skew,split関数はループしないのでterminationを落とした + +### nextとexitの話 + +``` Agda +-- 左回転、exitはsplit_branchへ nextもsplit_branchへ +merge-rotate-left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit + = next record { vart = bt-node record { key = record { coler = y ; number = rx } + ; ltree = (bt-node record { key = record { coler = red ; number = x } ; ltree = l ; rtree = rl }) + ; rtree = rr} + ; varn = varn ; varl = varl } +``` + +本来は動かない部分をexitとしている。この部分をどうしようか考えている。 +- 全てnext/exitのどちらかに統一する方法 +- exitに例外処理を渡す +- 現在はexitに、nextと同じ遷移先を示している。 + + +## 余談 +- air podsを買った + - コスパはあまりよくなさそうですが、apple製品との連携が良い +- Agdaのコードを一切ハイライトしてくれなかった… \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/soto/log/2021-01-19.md Thu Jan 21 00:10:03 2021 +0900 @@ -0,0 +1,122 @@ +# 研究目的 + +- OSやアプリケーションの信頼性を高めることは重要な課題である。 + +- 研究室でCbCという言語を開発している。その信頼性を証明したい。 + - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。 + +- cbcはサブルーチンとループ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。 + +- プログラムの検証手法のひとつに、Hoare Logic がある。 + - これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。 + + - つまり、関数が任意の値が引数として実行された際に、任意の値が帰ってきた場合を「関数は正常に実行される」といえる。 + + - CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。 + + +- cbcの実行を継続するという性質に Hoare Logicを連続して用いると、個々の関数の正当性の証明と接続の健全性について証明する事でプログラム全体の検証を行う事ができる。 + +- これらのことから、Hoare Logicを用いてCbCを検証する。 + + +- 先行研究ではCbCにおけるWhileLoopの検証を行なった。 + +- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う + +# 今週やった事 +- meta-dataの作成 + - 木の深さカウント(途中) + - black-nodeの数え上げ + +- 関数の実装 + - find-min(最小値を返す) + - find(値を検索する) + - delete(途中) + +## meta-dataの作成 +前回と同じく再起処理を使ってなんとかした + +## 関数の実装 + +### find-min +左ノードをみていく感じにして実装 +```Agda +rbt-search-min : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +rbt-search-min env next exit with Env.vart env +... | bt-empty = exit env +... | bt-node node with tree.ltree node +... | bt-empty = exit env +... | bt-node lnode = next (record + { vart = bt-node lnode + ; varn = Env.varn env + ; varl = Env.varl env + }) +``` +一番下の実装もっと綺麗な書き方があったはずですが忘れてしまいました… + +### find +こちらも普通に実装 +見つかった場合とemptyに行った場合にexitしている。 +上に当てはまらない場合に大小関係によって探索する部分を切り替えている。 + +```Agda +rbt-find : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +rbt-find env next exit with (Env.varn env) +... | n with (Env.vart env) +... | bt-empty = exit (record + { vart = bt-empty + ; varn = Env.varn env + ; varl = Env.varl env + }) +... | bt-node node with node.number (tree.key node) +... | x with <-cmp n x +... | tri≈ ¬a b ¬c = exit env +... | tri< a ¬b ¬c = next (record + { vart = tree.ltree node + ; varn = Env.varn env + ; varl = Env.varl env + }) +... | tri> ¬a ¬b c = next (record + { vart = tree.rtree node + ; varn = Env.varn env + ; varl = Env.varl env + }) +``` + +見つかった場合にTrue, 存在しない場合にFalseを返すようにした。 + +### delete +実装途中。 +若干面倒ではあるができそうではある。 + +## 余談 +- 来週院試なのでスライドを作成したい。 + +# 作業ログ + +## 赤黒木のノード数を数える関数を作成する +- 深さをひとつづつ数えて、l-node,r-nodeがenptyになるまで繰り返す +- 終わったら、r-nodeとl-nodeで深さを比較、大きい方を上に上げる +- すると最終的に最大のdeepが取ってこれる。 + +deepのカウントまではできた +get-deepで深さを簡単に取れるようにできたらいいな + +## 上から数えた際の黒ノードの数え上げ +- そのノードが黒ならsucするようにする + +## metadetaの作成をどうしようか +方法としては以下が挙げられる +- 全て同時にやる方法 + - コードが冗長になる… +- ひとつづつやる方法 + - ひとつづつやるには、作らない部分のフィールドにNanを入れてやらないといけない + +~~同時にやる方を採用してみる~~\ +最初にフィールド変数として持っておいて、 +ひとつづつ編集していく方式の方が綺麗そう + +## node数の数え上げ +加えてlog_2 nする関数を作成しないといけない +
--- a/user/soto/log/untitled.md Wed Jan 20 00:10:03 2021 +0900 +++ b/user/soto/log/untitled.md Thu Jan 21 00:10:03 2021 +0900 @@ -1,122 +1,1 @@ -# 研究目的 - -- OSやアプリケーションの信頼性を高めることは重要な課題である。 - -- 研究室でCbCという言語を開発している。その信頼性を証明したい。 - - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。 - -- cbcはサブルーチンとループ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。 - -- プログラムの検証手法のひとつに、Hoare Logic がある。 - - これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。 - - - つまり、関数が任意の値が引数として実行された際に、任意の値が帰ってきた場合を「関数は正常に実行される」といえる。 - - - CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。 - - -- cbcの実行を継続するという性質に Hoare Logicを連続して用いると、個々の関数の正当性の証明と接続の健全性について証明する事でプログラム全体の検証を行う事ができる。 - -- これらのことから、Hoare Logicを用いてCbCを検証する。 - - -- 先行研究ではCbCにおけるWhileLoopの検証を行なった。 - -- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う - -# 今週やった事 -- meta-dataの作成 - - 木の深さカウント(途中) - - black-nodeの数え上げ - -- 関数の実装 - - find-min(最小値を返す) - - find(値を検索する) - - delete(途中) - -## meta-dataの作成 -前回と同じく再起処理を使ってなんとかした - -## 関数の実装 - -### find-min -左ノードをみていく感じにして実装 -```Agda -rbt-search-min : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t -rbt-search-min env next exit with Env.vart env -... | bt-empty = exit env -... | bt-node node with tree.ltree node -... | bt-empty = exit env -... | bt-node lnode = next (record - { vart = bt-node lnode - ; varn = Env.varn env - ; varl = Env.varl env - }) -``` -一番下の実装もっと綺麗な書き方があったはずですが忘れてしまいました… - -### find -こちらも普通に実装 -見つかった場合とemptyに行った場合にexitしている。 -上に当てはまらない場合に大小関係によって探索する部分を切り替えている。 - -```Agda -rbt-find : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t -rbt-find env next exit with (Env.varn env) -... | n with (Env.vart env) -... | bt-empty = exit (record - { vart = bt-empty - ; varn = Env.varn env - ; varl = Env.varl env - }) -... | bt-node node with node.number (tree.key node) -... | x with <-cmp n x -... | tri≈ ¬a b ¬c = exit env -... | tri< a ¬b ¬c = next (record - { vart = tree.ltree node - ; varn = Env.varn env - ; varl = Env.varl env - }) -... | tri> ¬a ¬b c = next (record - { vart = tree.rtree node - ; varn = Env.varn env - ; varl = Env.varl env - }) -``` - -見つかった場合にTrue, 存在しない場合にFalseを返すようにした。 - -### delete -実装途中。 -若干面倒ではあるができそうではある。 - -## 余談 -- 来週院試なのでスライドを作成したい。 - -# 作業ログ - -## 赤黒木のノード数を数える関数を作成する -- 深さをひとつづつ数えて、l-node,r-nodeがenptyになるまで繰り返す -- 終わったら、r-nodeとl-nodeで深さを比較、大きい方を上に上げる -- すると最終的に最大のdeepが取ってこれる。 - -deepのカウントまではできた -get-deepで深さを簡単に取れるようにできたらいいな - -## 上から数えた際の黒ノードの数え上げ -- そのノードが黒ならsucするようにする - -## metadetaの作成をどうしようか -方法としては以下が挙げられる -- 全て同時にやる方法 - - コードが冗長になる… -- ひとつづつやる方法 - - ひとつづつやるには、作らない部分のフィールドにNanを入れてやらないといけない - -~~同時にやる方を採用してみる~~\ -最初にフィールド変数として持っておいて、 -ひとつづつ編集していく方式の方が綺麗そう - -## node数の数え上げ -加えてlog_2 nする関数を作成しないといけない - +redirect /user/soto/log/2021-01-19 \ No newline at end of file