Canvas 1

# HG changeset patch # User soto # Date 1653293769 -32400 # Node ID bc8222372b9dcbd2fc88cf85a7a3014220e7a551 # Parent 971da38e75963c37e971ae43d93714605d6a5161 ADD スライドの流れを一旦push diff -r 971da38e7596 -r bc8222372b9d slide/cbc_codegear.jpg Binary file slide/cbc_codegear.jpg has changed diff -r 971da38e7596 -r bc8222372b9d slide/logo.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/logo.svg Mon May 23 17:16:09 2022 +0900 @@ -0,0 +1,683 @@ + + + + \ No newline at end of file diff -r 971da38e7596 -r bc8222372b9d slide/meta-ca-dg.jpg Binary file slide/meta-ca-dg.jpg has changed diff -r 971da38e7596 -r bc8222372b9d slide/meta_cg_dg.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/meta_cg_dg.svg Mon May 23 17:16:09 2022 +0900 @@ -0,0 +1,131 @@ + + + diff -r 971da38e7596 -r bc8222372b9d slide/note.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/note.md Mon May 23 17:16:09 2022 +0900 @@ -0,0 +1,164 @@ + + +# タイトル + +Gears Agdaにおける +Left Learning Red Black Tree の検証について + +琉球大学並列信頼研究室の上地が発表します + +# 目的 +そのまま読む + +# CbC +もそのまま読む + +# Agda +もそのまま読む + +# Agda の基本 +Agda の基本となる型の１つである Record 型について説明します + +record Env とあるところで Env という Record 型を定義 +することを示しています + +そしてその中にvarnとvariがあり、その型が自然数であることを定義しています + +次に、記述する際の導入が以下のようになり +varnに0を、variに1を定義しています + +導入後は変数スペース record名でその中身にアクセスできます + +# Gears Agda の記法 +何と対応しているからLoopで記述するんだっけ + +Agdaの構文的に禁止していないので再帰呼び出しは使用しないよう注意が必要です + +以下がwhile loopのノーマルレベルでの記述になります + +まず型の方で +Envを受け取り、Codeを受け取り、 +tを返すといった流れになっています + +このCodeはEnvを受け取った後にｔを返すというものです + +次に、入力を env next で受け取っています + +このcodeは後で再び説明するので、withの方はおいておいてください + +パターンマッチの方で、false trueの場合をかんがえています +これはfalseの場合はnextにenvを渡します +nextはenvを受け取ってtを返すので正しいです +これがtを返すことでこの後も関数が続くこと、継続を示します + + +# Gears Agdaと Gears CbCの対応 +そのまま読むでよさそう +Contextだけ調べた方がよいかも + + +# Normal levelと～ +今回検証に使用するHoare Conditionと証明も Meta levelです + +画像はよなおせ + +# Hoare logic +コマンドが事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという + +簡単な例としてGears Agdaにてwhile loopを検証します + +以下のコードを詳細に説明します + +入力と出力に関しては前述しました +このたーみねーてぃんぐはこの関数が停止することを示しています +この実装ではagdaはloopが終了するのかわからず、コンパイルできないので +このあのてーとをつけて停止することを明示します + +with文は引数であたえられた値を展開します。 +今回はその値をパターンマッチしています。 + +これがless than で0とvarnを比較しています + +このwhileloopは、 +varnがこれからループする回数で、variがループした回数になります + +なので、これが0になると終了し次の関数であるnextに遷移し +0でないならループする回数varxから今回分の１引いて +variには今回分の1を足したものをEnvとしてもう一度関数を実行するという記述になっています + +# post condition +先ほど実装したノーマルレベルなwhile loopに対して +条件となるPre / Post Condition を追加した実装をします + +そのまえにterminatingが付いていると停止性の証明をしたことにはならないので～ +loopを分割した実装を行います + +このconditionはループしたい回数は +これからループする回数とループした回数の和と等しいというものです + + +# loopの接続 +loopが前のページのWhile LoopSeg だな + +loopの部分の証明のみだな + +# 実際のloopの接続 +最終的にはループした回数が入力のループしたい回数と一致していることを +証明したいので以下のようになります + +で、前回のものは最初から構造体（record）に値が格納されている状態から始まっていたので +proofGearsTermS では、入力が自然数で、recordの定義から検証を行っている + +そしてそれを行っているのが最初の関数であるwhileTest'で +ここでvarnが入力c10と一致し、variが0であることを証明している + +次の関数であるversionでは、whileTest'のrecord定義時のConditionから +loop時のconditionを生成しています + +# testとの違い +そのまま読むよ + +Condition + +# BTの実装 +これはノーマルレベルの BinaryTree の find 実装になります + +これが行っているのはkeyと等しいnodeを見つける + +なので入力されているtreeのkeyと比較し +等しかった場合は終了 + +入力のkeyの方が小さい場合は +左のtreeを次のfindの対象とし +今回対象のtreeをstackに積む + +# replace tree + +先ほどと同じように入力のkeyと比較し +今度は木を再構成するので + +# Invariant +Binary Treeの証明には３つのInvariant（不変条件）をもちいる +あとはそのまま読む + +# find hoare condition + +最初のtreeInvariant tree ∧ stackInvariantが +pre conditionで、 +treeInvariant と stackInvariantを満たしていることを証明する + +nextには次のInvariant と現在の木の深さが最大ではないことを示しています + +exitなのでfindを終了する際には +valueを見つけられなかったことを表す +tree1がleefか + +valueを見つけたことを表す +tree1のkeyが入力のkeyといっちしていることを表します + +# カンペ +synchronized queue +- 読めない間は待っている +concurrent tree +- + diff -r 971da38e7596 -r bc8222372b9d slide/slide.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/slide.md Mon May 23 17:16:09 2022 +0900 @@ -0,0 +1,186 @@ +--- +marp: true +title: Geas Agda による Left Learning Red Black Tree の検証 +paginate: true + +theme: default +size: 16:9 +style: | + section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; + } + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + + section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; + } + + section.fig_cg p { + top: 300px; + text-align: center; + } + +--- + + +# Gears Agda による
Left Learning Red Black Tree の検証 + + +Uechi Yuto, Shinji Kono 琉球大学 + +# Gears Agda によるプログラムの改善 + + + +- 思い思いにプログラムを書くと、冗長なコードができてしまい、実行時間も遅い場合がある。この場合にコードに対してアルゴリズムを適応すると、一般的に良いコードが作成できる。 + +- しかし、世の中にはすでに大量のアルゴリズムが存在するため、これを一人のプログラマーが全て覚え、適応できる場面を思いつくというのは初学者には難しい。そのため、人が書いたコードに対してアルゴリズムを使用するコードに自動的に変換できるようにしたい。 + +- この際、アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。このアルゴリズム適応前後の処理の恒等性を検証するため、Gears Agda を用いる。 + +# Gears Agda と CbCの説明 (いらないかも +- Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のこと +- 通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。この際メインルーチンで使用していた変数などの環境はスタックされ、サブルーチンが終了した際にメインルーチンに戻り、スタックしていた変数をもとに戻す流れとなる。 +- CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ、スタックを持たず環境を保持しない。更に遷移後にメインルーチンに戻ることもない。つまり関数の実行では暗黙な環境が存在せず、関数が受け取った引数のみを使用する。 +- これにより限定的な実行条件を作成でき、検証がしやすくなる。 + +# Gears Agda でのアルゴリズム入れ替え判定 +- 現在、アルゴリズムの適応可否は以下の方法を考えている。 + + - あらかじめ、アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく + + - 書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき、満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える + +- この際、実装が仕様を満たしているか検証する手法には、定理証明やモデル検査などが挙げられる。 + +# Gears Agda でのモデル検査 +- アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い、アルゴリズムの仕様がコードに適応できるか検証するのが妥当だと考えている + +- 思い思いに書いたコードに対して定理証明を行うのはコストが高く、適応するものの内部動作が一致しない場合定理証明を行っても使えないためである + +- アルゴリズムの入れ替え可否をモデル検査で判定し、入れ替えたあとに適応前後で同じ処理をしていることを定理証明で検証することを目標としている + +- この Gears Agda でのモデル検査の先駆けとして今回は Dining Philosophers Programのモデル検査を行った + +# CbC について +- CbCとは当研究室で開発しているC言語の下位言語 + - 継続呼び出しは引数付き goto 文で表現される。 + - 関数呼び出し時のスタックの操作を行わずjmp命令で次の処理に移動する + - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語 +- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。 + + +# Agda の基本 +- Agdaとは定理証明支援器であり、関数型言語 +- Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する +- 型の定義部分で、入力と出力の型を定義できる + - input → output のようになる +- 関数の定義は = を用いて行う + - 関数名の後、 = の前で受け取る引数を記述します + + + + +# Gears Agda の記法 + +Gears Agda では CbC と対応させるためにすべてLoopで記述する +loopは`→ t`の形式で表現する +再帰呼び出しは使わない(構文的には禁止していないので注意が必要) +``` +{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next +``` +- t を返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える) +- tail call により light weight continuation を定義している + +# Normal level と Meta Level を用いた信頼性の向上 +Normal Level +- 軽量継続 +- Code Gear 単位で関数型プログラミングとなる +- atomic(Code Gear 自体の実行は割り込まれない) +- ポインタの操作は含まれない + + +Meta Level +- メモリやCPUなどの資源管理, ポインタ操作 +- Hoare Condition と証明 +- Contextによる並列実行 +- monadに相当するData構造 + + +# Normal level と Meta Level の対応 +![height:400px](meta-cg-dg.jpg) + +# DPPの説明 +哲学者がいて〜 +フォークがあって〜 + +# モデル検査と定理証明の説明 +モデル検査はコストが安いが完全な検証にはならない +定理証明はコスト高いが完全な検証になる + +# DPPの記述 +DPPをこんな感じで書いて行くよ的な + +# モデル検査 +ビット全探索を今回は行った + +# モデル検査 +デッドロック検知 + +# 今後の研究方針 +- Deleteの実装 +- Red Black Tree の実装 + - 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず +- Contextを用いた並列実行時のプログラムの正しさの証明 + - synchronized queue + - concurrent tree +- xv.6への適用 +- モデル検査 + +# まとめ +- Gears Agda にて Binary Tree を検証することができた + - Gears Agda における Termination を使用しない実装の仕方を確立した + - Hoare Logic による検証もできるようになった + - 今後は Red Black Tree の検証をすすめる +- モデル検査をしたい + + diff -r 971da38e7596 -r bc8222372b9d slide/slide.pdf Binary file slide/slide.pdf has changed