Mercurial > hg > Papers > 2017 > atton-master

comparison presentation/slide.md @ 120:8a84cda440f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slide
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 14 Feb 2017 11:31:08 +0900
parents 26563097333c
children 137aae675a94
comparison
equal deleted inserted replaced
119:26563097333c 120:8a84cda440f3
19 * 依存型を持つ証明支援系言語 Agda による CbC の証明 19 * 依存型を持つ証明支援系言語 Agda による CbC の証明
20 * 部分型を利用して Agda 上に型付きの CbC の項を記述する 20 * 部分型を利用して Agda 上に型付きの CbC の項を記述する
21 * 型システムを通して CbC の形式的な定義を得る 21 * 型システムを通して CbC の形式的な定義を得る
22 * SingleLinkedStack の性質の証明 22 * SingleLinkedStack の性質の証明
23 23
24 # 本発表ではモデル検査的アプローチについて中心に見ていきます
25 * 修士論文の内部の比率は半分半分くらい
26 * 定理証明の方は説明する内容が多くて複雑
27 * モデル検査的アプローチは過去論文を提出したもの
28 * なのでそちらをメインで発表します
29
24 # モデル検査的アプローチについての流れ 30 # モデル検査的アプローチについての流れ
25 * Continuation based C (CbC) 言語について 31 * Continuation based C (CbC) 言語について
26 * CbC における CodeSegment と DataSegment を用いたプログラミングスタイル 32 * CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
27 * CbC とメタ計算について 33 * CbC とメタ計算について
28 * CbC で記述された GearsOS とそのデータ構造である赤黒木 34 * CbC で記述された GearsOS とそのデータ構造である赤黒木
35 * CodeSegment と DataSegment という単位を用いてプログラミングする 41 * CodeSegment と DataSegment という単位を用いてプログラミングする
36 * 両検証手法をメタ計算として利用可能 42 * 両検証手法をメタ計算として利用可能
37 43
38 # CodeSegment 44 # CodeSegment
39 * CodeSegment とは 45 * CodeSegment とは
40 * 処理の単位 46 * 処理の単位であり、入力と出力を持つ
41 * 結合や分割が容易 47 * 結合や分割が容易
42 * 入力と出力を持つ
43 * CodeSegment どうしを接続することによりプログラム全体を作る 48 * CodeSegment どうしを接続することによりプログラム全体を作る
49 * 関数呼び出しと違って戻ってこない(goto)
44 50
45 ![cs](./images/cs.svg){:width="50%"} 51 ![cs](./images/cs.svg){:width="50%"}
52
53 ```
54 __code cs0(int a, int b){
55 goto cs1(a+b);
56 }
57 ```
46 58
47 59
48 # DataSegment 60 # DataSegment
49 * DataSegment とは 61 * DataSegment とは
50 * データの単位 62 * データの単位
51 * CodeSegment の入出力にあたる 63 * CodeSegment の入出力にあたる
52 * 接続元の Output DataSegment は接続先の Input DataSegment 64 * 接続元の Output DataSegment は接続先の Input DataSegment
53 65
54 ![ds](./images/ds.svg){:width="50%"} 66 ![ds](./images/ds.svg){:width="50%"}
67
68 ```
69 __code cs0(int a, int b){
70 goto cs1(a+b);
71 }
72 ```
55 73
56 # メタ計算 74 # メタ計算
57 * とある計算を実現するための計算 75 * とある計算を実現するための計算
58 * ネットワーク接続、例外処理、メモリ確保、並列処理など 76 * ネットワーク接続、例外処理、メモリ確保、並列処理など
59 * CbC は通常レベルの計算とメタ計算を分離して考える 77 * CbC は通常レベルの計算とメタ計算を分離して考える
85 * 特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る 103 * 特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
86 * ルートノードと葉ノードの色は黒 104 * ルートノードと葉ノードの色は黒
87 * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い) 105 * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)
88 * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定 106 * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定
89 107
90 ![rbtree](./images/rbtree.svg){:width="50%"} 108 ![rbtree](./images/rbtree.svg){:width="35%"}
91 109
92 # GearsOS における赤黒木の利用例(ノードの挿入) 110 # GearsOS における赤黒木の利用例(ノードの挿入)
93 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto 111 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
94 * goto する前に Meta CodeSegment が実行されて木に挿入する 112 * goto する前に Meta CodeSegment が実行されて木に挿入する
95 * GearsOS では木の実装のためにスタックを用いて経路情報を保持している 113 * GearsOS では木の実装のためにスタックを用いて経路情報を保持している
96 114
115
97 ![put](./images/put.svg){:width="50%"} 116 ![put](./images/put.svg){:width="50%"}
117
118 ```
119 goto meta(context, Put);
120 ```
98 121
99 # 仕様の記述とその確認 122 # 仕様の記述とその確認
100 * 「バランスが取れている」とは何かを表現できる必要がある 123 * 「バランスが取れている」とは何かを表現できる必要がある
101 * 実行可能な CbC の式を使った assert になる 124 * 実行可能な CbC の式を使った assert になる
102 * そしてそれを保証したい 125 * そしてそれを保証したい
108 * 並列に動作するプログラムの仕様を検証可能 131 * 並列に動作するプログラムの仕様を検証可能
109 * 検証した promela から実行可能な C ソースを生成可能 132 * 検証した promela から実行可能な C ソースを生成可能
110 * 仕様は bool になる式を用いた assert 133 * 仕様は bool になる式を用いた assert
111 * デメリット: promela は C とは記述が異なる 134 * デメリット: promela は C とは記述が異なる
112 135
136 ```
137 assert(x < 10);
138 ```
139
113 # 既存のモデル検査器 CBMC 140 # 既存のモデル検査器 CBMC
114 * CBMC 141 * CBMC
115 * 検証対象のCソースを変更しないでも良い 142 * 検証対象のCソースを変更しないでも良い
116 * C/C++ 言語の記号実行が可能 143 * C/C++ 言語の記号実行が可能
117 * 条件分岐を網羅的に実行 144 * 条件分岐を網羅的に実行
118 * 仕様は bool になる式を用いた assert 145 * 仕様は bool になる式を用いた assert
119 * 有限ステップ検証する有界モデル検査器 146 * 有限ステップ検証する有界モデル検査器
120 147
121 # メタ計算ライブラリ akasha 148 ```
122 * メタ計算としてプログラムの状態を数え上げる 149 assert(x < 10);
123 * goto された時に挿入される要素の組み合わせを全て列挙して実行する 150 ```
124 * その度に仕様の式は成り立つかをチェックする
125 * ノーマルレベルのコードを検証用に変更せず検証可能
126
127 ![akashaPut](./images/akashaPut.svg){:width="51%"}
128 151
129 # チェックする仕様 152 # チェックする仕様
130 * 赤黒木の高さに関する仕様に以下のものがある 153 * 赤黒木の高さに関する仕様に以下のものがある
131 * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる 154 * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
132 * 以下のように assert を用いて CbC で定義できる 155 * 以下のような条件式を仕様として CbC で定義、検証できる
133 * この仕様が満たされるかをチェックする
134 156
135 ``` 157 ```
136 __code verifySpecificationFinish(struct Context* context) { 158 __code verifySpecificationFinish(struct Context* context) {
137 if (context->data[AkashaInfo]->akashaInfo.maxHeight > 159 if (context->data[AkashaInfo]->akashaInfo.maxHeight >
138 2*context->data[AkashaInfo]->akashaInfo.minHeight) 160 2*context->data[AkashaInfo]->akashaInfo.minHeight)
141 goto meta(context, ShowTrace); 163 goto meta(context, ShowTrace);
142 } 164 }
143 goto meta(context, DuplicateIterator); 165 goto meta(context, DuplicateIterator);
144 } 166 }
145 ``` 167 ```
168
169 # メタ計算ライブラリ akasha
170 * メタ計算としてプログラムの状態を数え上げる
171 * goto された時に挿入される要素の組み合わせを全て列挙して実行する
172 * 赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……
173 * その度に仕様の式は成り立つかをチェックする
174 * ノーマルレベルのコードを検証用に変更せず検証可能
175
176 ![akashaPut](./images/akashaPut.svg){:width="51%"}
146 177
147 # akasha と CBMC の比較 178 # akasha と CBMC の比較
148 * akasha は有限の要素数の組み合わせをチェックする 179 * akasha は有限の要素数の組み合わせをチェックする
149 * 要素数が13個までならどの順で木に挿入しても良い 180 * 要素数が13個までならどの順で木に挿入しても良い
150 * 比較対象として C Bounded Model Checker を使用した 181 * 比較対象として C Bounded Model Checker を使用した
152 * 実行可能なステップ数411だけ展開しても仕様は満たされる 183 * 実行可能なステップ数411だけ展開しても仕様は満たされる
153 * が、恣意的にバグを入れ込んでも反例を返さない 184 * が、恣意的にバグを入れ込んでも反例を返さない
154 * akasha は返した 185 * akasha は返した
155 * 固定の要素数までの仕様検査で十分なのか? 186 * 固定の要素数までの仕様検査で十分なのか?
156 187
157 # 定理証明的なアプローチの流れ
158 * プログラムを証明するにはどうするのか
159 * 証明支援系 Agda における証明
160 * Agda による CbC の定義
161 * Agda を用いて CbC のコードを証明する
162
163 # 定理証明を Continuation based C へ適用するには 188 # 定理証明を Continuation based C へ適用するには
164 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい 189 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
165 * そのままプログラムの性質を保証してやる 190 * そのままプログラムの性質を保証してやる
166 * Coq, Agda, ATS2 などのプログラミング言語で証明が可能 191 * Coq, Agda, ATS2 などのプログラミング言語で証明が可能
167 * 本当は CbC で CbC 自身を証明したい 192 * 本当は CbC で CbC 自身を証明したい
204 * 任意の通常のレベルの計算を扱えなくてはならない 229 * 任意の通常のレベルの計算を扱えなくてはならない
205 * ライブラリが呼び出されるプログラムは無数にあるようなイメージ 230 * ライブラリが呼び出されるプログラムは無数にあるようなイメージ
206 * メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い 231 * メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い
207 * 部分型を使う 232 * 部分型を使う
208 * Java におけるインターフェース、Haskell における型クラス 233 * Java におけるインターフェース、Haskell における型クラス
209 * 「このデータにはこのフィールドさえあれば良い」 234 * 「このフィールドXがあればデータ型Tとみなして良い」
210 235
211 # Agda 上のメタ計算 236 # Agda 上のメタ計算
212 * ノーマルレベルの型を保持したままメタレベルの計算を利用できる 237 * ノーマルレベルの型を保持したままメタレベルの計算を利用できる
213 * cs0 の定義はメタ計算用に変更しなくても良い 238 * cs0 の定義はメタ計算用に変更しなくても良い
214 239
215 ``` 240 ```
241 cs0 : CodeSegment ds0 ds1
242 cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
243 ```
244
245 ```
216 main : ds1 246 main : ds1
217 main = goto cs0 (record {a = 100 ; b = 50}) 247 main = goto cs0 (record {a = 100 ; b = 50})
218 ``` 248 ```
219 ``` 249 ```
220 main : Meta 250 main : Meta
221 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) 251 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70})
252 ; c' = 0 ; next = (N.cs id)})
222 ``` 253 ```
223 254
224 # Agda 上に CbC を記述した成果 255 # Agda 上に CbC を記述した成果
225 * 部分型で CbC の型付けができた 256 * 部分型で CbC の型付けができた
226 * メタ計算をきちんと階層化できた 257 * メタ計算をきちんと階層化できた
242 * 部分型を利用してCbCを型付け 273 * 部分型を利用してCbCを型付け
243 * 依存型をCbC に導入して自身を証明可能にする 274 * 依存型をCbC に導入して自身を証明可能にする
244 * 型情報から stub を自動生成すkる 275 * 型情報から stub を自動生成すkる
245 * 赤黒木の挿入に関する性質を証明する 276 * 赤黒木の挿入に関する性質を証明する
246 277
278 # 発表履歴
279 * Agda 入門.
280 * オープンソースカンファレンス 2014 Okinawa, May 2014.
281 * 形式手法を学び始めて思うことと、形式手法を広めるには(2p).
282 * 情報処理学会ソフトウェア工学研究会 (IPSJ SIGSE) ウィンターワークショップ 2015・ イン・宜野湾 (WWS2015), Jan 2015.
283 * Continuation based C を用いたプログラムの検証手法(6p).
284 * 2016 年並列/分散/協調処理に関する『松本』サマー・ワークショップ (SWoPP2016)
285 * 情報処理学会・プログラミング研究会 第 110 回プログラミング研究会 (PRO-2016-2) Aug 2016.
286
247 <!-- vim: set filetype=markdown.slide: --> 287 <!-- vim: set filetype=markdown.slide: -->
248 288