Mercurial > hg > Papers > 2018 > nozomi-master

comparison presentation/slide.md @ 114:5cca315b0230

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing slide...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 13 Feb 2017 16:01:38 +0900
parents e1d3317d5789
children ed6719c301fc
comparison
equal deleted inserted replaced
113:2e30ed0e2633 114:5cca315b0230
39 * CodeSegment とは 39 * CodeSegment とは
40 * 処理の単位 40 * 処理の単位
41 * 結合や分割が容易 41 * 結合や分割が容易
42 * 入力と出力を持つ 42 * 入力と出力を持つ
43 * CodeSegment どうしを接続することによりプログラム全体を作る 43 * CodeSegment どうしを接続することによりプログラム全体を作る
44 * TODO: 図 44
45 ![goto](./images/goto.svg){:width="50%"}
46
45 47
46 # DataSegment 48 # DataSegment
47 * DataSegment とは 49 * DataSegment とは
48 * データの単位 50 * データの単位
49 * CodeSegment の入出力にあたる 51 * CodeSegment の入出力にあたる
50 * 接続元の Output DataSegment は接続先の Input DataSegment 52 * 接続元の Output DataSegment は接続先の Input DataSegment
51 * TODO: 図 53
54 ![csds](./images/csds.svg){:width="50%"}
52 55
53 # メタ計算 56 # メタ計算
54 * とある計算を実現するための計算 57 * とある計算を実現するための計算
55 * ネットワーク接続、例外処理、メモリ確保、並列処理など 58 * ネットワーク接続、例外処理、メモリ確保、並列処理など
56 * CbC は通常レベルの計算とメタ計算を分離して考える 59 * CbC は通常レベルの計算とメタ計算を分離して考える
57 * 通常レベルではポインタは出てこない、など 60 * 通常レベルではポインタは出てこない、など
58 * CodeSegment の接続部分に処理を追加することで実現 61 * CodeSegment の接続部分に処理を追加することで実現
59 * TODO: 図 62
63 ![meta](./images/meta.svg){:width="50%"}
60 64
61 # Meta CodeSegment 65 # Meta CodeSegment
62 * メタ計算を行なう CodeSegment 66 * メタ計算を行なう CodeSegment
63 * 通常の CodeSegment どうしの接続の間に入る 67 * 通常の CodeSegment どうしの接続の間に入る
64 * TODO: 図 68 * TODO: 図
84 88
85 # GearsOS における赤黒木の利用例(ノードの挿入) 89 # GearsOS における赤黒木の利用例(ノードの挿入)
86 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto 90 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
87 * goto する前に Meta CodeSegment が実行されて木に挿入する 91 * goto する前に Meta CodeSegment が実行されて木に挿入する
88 * GearsOS では木の実装のためにスタックを用いて経路情報を保持している 92 * GearsOS では木の実装のためにスタックを用いて経路情報を保持している
89 * TODO: 図 93
94 ![put](./images/put.svg){:width="50%"}
90 95
91 # 仕様の記述とその確認 96 # 仕様の記述とその確認
92 * 「バランスが取れている」とは何かを表現できる必要がある 97 * 「バランスが取れている」とは何かを表現できる必要がある
93 * 実行可能な CbC の式を使った assert になる 98 * 実行可能な CbC の式を使った assert になる
94 * そしてそれを保証したい 99 * そしてそれを保証したい
113 # メタ計算ライブラリ akasha 118 # メタ計算ライブラリ akasha
114 * メタ計算としてプログラムの状態を数え上げる 119 * メタ計算としてプログラムの状態を数え上げる
115 * goto された時に挿入される要素の組み合わせを全て列挙して実行する 120 * goto された時に挿入される要素の組み合わせを全て列挙して実行する
116 * その度に仕様の式は成り立つかをチェックする 121 * その度に仕様の式は成り立つかをチェックする
117 * ノーマルレベルのコードを検証用に変更せず検証可能 122 * ノーマルレベルのコードを検証用に変更せず検証可能
118 * TODO: 図 123
124 ![akashaPut](./images/akashaPut.svg){:width="51%"}
119 125
120 # チェックする仕様 126 # チェックする仕様
121 * TODO: たかさについて 127 * 赤黒木のの高さに関する仕様に以下のものがある
128 * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
129 * 以下のように assert を用いて CbC で定義できる
130 * この仕様が満たされるかをチェックする
131
132 ```
133 void verifySpecification(struct Context* context, struct Tree* tree) {
134 assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
135 goto meta(context, EnumerateInputs);
136 }
137 ```
122 138
123 # akasha と CBMC の比較 139 # akasha と CBMC の比較
124 * akasha は有限の要素数の組み合わせをチェックする 140 * akasha は有限の要素数の組み合わせをチェックする
125 * 要素数が13個までならどの順で木に挿入しても良い 141 * 要素数が13個までならどの順で木に挿入しても良い
126 * 比較対象として C Bounded Model Checker を使用した 142 * 比較対象として C Bounded Model Checker を使用した
129 * が、恣意的にバグを入れ込んでも反例を返さない 145 * が、恣意的にバグを入れ込んでも反例を返さない
130 * akasha は返した 146 * akasha は返した
131 * 固定の要素数までの仕様検査で十分なのか? 147 * 固定の要素数までの仕様検査で十分なのか?
132 148
133 # 定理証明的なアプローチの流れ 149 # 定理証明的なアプローチの流れ
134 * 150 * プログラムを証明するにはどうするのか
151 * 証明支援系 Agda における証明
152 * Agda による CbC の定義
153 * Agda を用いて CbC のコードを証明する
135 154
136 # 定理証明を Continuation based C へ適用するには 155 # 定理証明を Continuation based C へ適用するには
137 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい 156 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
138 * そのままプログラムの性質を保証してやる 157 * そのままプログラムの性質を保証してやる
139 * Coq, Agda, ATS2 などのプログラミング言語で証明が可能 158 * Coq, Agda, ATS2 などのプログラミング言語で証明が可能
140 * 本当は CbC で CbC 自身を証明したい 159 * 本当は CbC で CbC 自身を証明したい
141 * しかし CbC の形式的な定義が無いために今はできない 160 * しかし CbC の形式的な定義が無いために今はできない
142 * Agda 上に CbC を定義することで形式的な定義を得る 161 * Agda 上に CbC を定義することで形式的な定義を得る
143 162
144 # Agda における CodeSegment と DataSegment 163 # Agda と DataSegment
164 * CbC の DataSegment は Agda のレコード型
165
166 ```
167 __code cs0(int a, int b){
168 goto cs1(a+b);
169 }
170 ```
171 ```
172 record ds0 : Set where
173 field
174 a : Int
175 b : Int
176 ```
177
145 # Agda と CodeSegment 178 # Agda と CodeSegment
146 # Agda と DataSegment 179 * CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)
180
181 ```
182 __code cs0(int a, int b){
183 goto cs1(a+b);
184 }
185 ```
186 ```
187 cs0 : CodeSegment ds0 ds1
188 cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
189 ```
147 190
148 # メタレベルの型付け 191 # メタレベルの型付け
149 * メタ計算とは通常のレベルとは区別された計算 192 * メタ計算とは通常のレベルとは区別された計算
150 * 任意の通常のレベルの計算を扱えなくてはならない 193 * 任意の通常のレベルの計算を扱えなくてはならない
151 * ライブラリが呼び出されるプログラムは無数にあるようなイメージ 194 * ライブラリが呼び出されるプログラムは無数にあるようなイメージ
152 * メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い 195 * メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い
153 * 部分型を使う 196 * 部分型を使う
154 * Java におけるインターフェース、Haskell における型クラス 197 * Java におけるインターフェース、Haskell における型クラス
155 * 「このデータにはこのフィールドさえあれば良い」 198 * 「このデータにはこのフィールドさえあれば良い」
156 199
157 # Agda 上の Meta CodeSegment 200 # Agda 上のメタ計算
158 # Agda 上の Meta DataSegment 201 * ノーマルレベルの型を保持したままメタレベルの計算を利用できる
202 * cs0 の定義はメタ計算用に変更しなくても良い
203
204 ```
205 main : ds1
206 main = goto cs0 (record {a = 100 ; b = 50})
207 ```
208 ```
209 main : Meta
210 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
211 ```
159 212
160 # Agda 上に CbC を記述した成果 213 # Agda 上に CbC を記述した成果
161 * 部分型で CbC の型付けができた 214 * 部分型で CbC の型付けができた
162 * メタ計算をきちんと階層化できた 215 * メタ計算をきちんと階層化できた
163 * メタ計算にもメタ計算が適用可能 216 * メタ計算にもメタ計算が適用可能