Mercurial > hg > Papers > 2017 > atton-master

comparison presentation/slide.md @ 107:e1d3317d5789

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 13:47:04 +0900
parents 3ead244513d5
children 5cca315b0230
comparison
equal deleted inserted replaced
106:cc2ca280345f 107:e1d3317d5789
19 * 依存型を持つ証明支援系言語 Agda による CbC の証明 19 * 依存型を持つ証明支援系言語 Agda による CbC の証明
20 * 部分型を利用して Agda 上に型付きの CbC の項を記述する 20 * 部分型を利用して Agda 上に型付きの CbC の項を記述する
21 * 型システムを通して CbC の形式的な定義を得る 21 * 型システムを通して CbC の形式的な定義を得る
22 * SingleLinkedStack の性質の証明 22 * SingleLinkedStack の性質の証明
23 23
24 # モデル検査的アプローチについての流れ
25 * Continuation based C (CbC) 言語について
26 * CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
27 * CbC とメタ計算について
28 * CbC で記述された GearsOS とそのデータ構造である赤黒木
29 * 赤黒木の仕様の定義とその検証手法
30
24 # Continuation based C 31 # Continuation based C
25 * 当研究室で開発しているプログラミング言語 32 * 当研究室で開発しているプログラミング言語
26 * アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語 33 * アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語
27 * OS や組み込みソフトウェアなどを対象にしている 34 * OS や組み込みソフトウェアなどを対象にしている
28 * CodeSegment と DataSegment という単位を用いてプログラミングする 35 * CodeSegment と DataSegment という単位を用いてプログラミングする
36 * 両検証手法をメタ計算として利用可能
29 37
30 # CodeSegment 38 # CodeSegment
31 * CodeSegment とは 39 * CodeSegment とは
32 * 処理の単位 40 * 処理の単位
33 * 結合や分割が容易 41 * 結合や分割が容易
43 * TODO: 図 51 * TODO: 図
44 52
45 # メタ計算 53 # メタ計算
46 * とある計算を実現するための計算 54 * とある計算を実現するための計算
47 * ネットワーク接続、例外処理、メモリ確保、並列処理など 55 * ネットワーク接続、例外処理、メモリ確保、並列処理など
48 * 時に本来行ないたい処理よりも複雑になる
49 * CbC は通常レベルの計算とメタ計算を分離して考える 56 * CbC は通常レベルの計算とメタ計算を分離して考える
50 * 通常レベルではポインタは出てこない、など 57 * 通常レベルではポインタは出てこない、など
58 * CodeSegment の接続部分に処理を追加することで実現
51 * TODO: 図 59 * TODO: 図
52 60
53 # Meta CodeSegment 61 # Meta CodeSegment
54 * メタ計算を行なう CodeSegment 62 * メタ計算を行なう CodeSegment
55 * 通常の CodeSegment どうしの接続の間に入る 63 * 通常の CodeSegment どうしの接続の間に入る
57 65
58 # Meta DataSegment 66 # Meta DataSegment
59 * メタ計算用の DataSegment 67 * メタ計算用の DataSegment
60 * 通常の DataSegment を含むような DataSegment 68 * 通常の DataSegment を含むような DataSegment
61 * TODO: 図 69 * TODO: 図
62
63 # C言語との対応
64 * CodeSegment は C 言語における返り値の無い関数
65 * DataSegment は C 言語における構造体
66 * Meta CodeSegment は CodeSegment の前後にある CodeSegment
67 * Meta DataSegment は全ての DataSegment の共用体を持つ構造体
68 * CodeSegment の接続は goto における軽量継続
69 * 末尾のみで行なうスタックを保持しない関数呼び出し
70 70
71 # 並列に信頼性高く動作する GearsOS 71 # 並列に信頼性高く動作する GearsOS
72 * CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある 72 * CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある
73 * 並列実行やモデル検査をメタ計算として提供する 73 * 並列実行やモデル検査をメタ計算として提供する
74 * 現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み 74 * 現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み
110 * 仕様は bool になる式を用いた assert 110 * 仕様は bool になる式を用いた assert
111 * 有限ステップ検証する有界モデル検査器 111 * 有限ステップ検証する有界モデル検査器
112 112
113 # メタ計算ライブラリ akasha 113 # メタ計算ライブラリ akasha
114 * メタ計算としてプログラムの状態を数え上げる 114 * メタ計算としてプログラムの状態を数え上げる
115 * goto された時に挿入される要素の組み合わせを全て列挙して実行する 115 * goto された時に挿入される要素の組み合わせを全て列挙して実行する
116 * その度に仕様の式は成り立つかをチェックする 116 * その度に仕様の式は成り立つかをチェックする
117 * ノーマルレベルのコードを検証用に変更せず検証可能
117 * TODO: 図 118 * TODO: 図
118 119
119 # チェックする仕様 120 # チェックする仕様
120 * TODO: たかさについて 121 * TODO: たかさについて
121 122
127 * 実行可能なステップ数411だけ展開しても仕様は満たされる 128 * 実行可能なステップ数411だけ展開しても仕様は満たされる
128 * が、恣意的にバグを入れ込んでも反例を返さない 129 * が、恣意的にバグを入れ込んでも反例を返さない
129 * akasha は返した 130 * akasha は返した
130 * 固定の要素数までの仕様検査で十分なのか? 131 * 固定の要素数までの仕様検査で十分なのか?
131 132
132 # 定理証明 133 # 定理証明的なアプローチの流れ
134 *
135
136 # 定理証明を Continuation based C へ適用するには
133 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい 137 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
134 * そのままプログラムの性質を保証してやる 138 * そのままプログラムの性質を保証してやる
135 * プログラムと証明は Curry-Howard Isomorphism により、自然演繹と型付ラムダ計算が対応 139 * Coq, Agda, ATS2 などのプログラミング言語で証明が可能
136 * プログラムにおける命題は型であり、証明はその導出が存在するかどうか 140 * 本当は CbC で CbC 自身を証明したい
137 * 例えば三段論法が書ける 141 * しかし CbC の形式的な定義が無いために今はできない
138 * (A -> B) -> (B -> C) -> (A -> C) 142 * Agda 上に CbC を定義することで形式的な定義を得る
139 * (int -> bool) -> (bool -> float) -> (int -> float)
140 143
141 # 証明支援系 Agda 144 # Agda における CodeSegment と DataSegment
142 * 依存型を持つ言語 145 # Agda と CodeSegment
143 * 型が第一級(型が値である) 146 # Agda と DataSegment
144 * 「型を取って型を返す型」などが定義可能
145 * 定理証明が記述可能
146 * この言語の上に CbC の項を表現する
147 * Agda 経由で CbC の形式的な定義を得る
148
149 # Agda 上に CbC を記述するには?
150 * CbC と CbC の対応で書ける?
151 * DataSegment -> 構造体(複数の値と名前によって成り立つ)
152 * CodeSegment -> 関数型(型を取って型を返す)
153 * Meta DataSegment -> 構造体の共用体
154 * Meta CodeSegment -> 関数型?
155 * Meta CodeSegment の階層構造をどう定義するか
156 * 構造体に相当するレコード型はAgdaにある
157 * 共用体に相当する直和型も定義可能
158 147
159 # メタレベルの型付け 148 # メタレベルの型付け
160 * Meta CodeSegment が持っているべき性質 149 * メタ計算とは通常のレベルとは区別された計算
161 * メタレベルは階層構造を持つ 150 * 任意の通常のレベルの計算を扱えなくてはならない
162 * メタ計算は組み合わせられる 151 * ライブラリが呼び出されるプログラムは無数にあるようなイメージ
163 * ノーマルレベルの DataSegment を一様に扱える 152 * メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い
164 * ノーマルレベルの CodeSegment へと goto できる 153 * 部分型を使う
165 * どんなプログラムからもライブラリとして使える 154 * Java におけるインターフェース、Haskell における型クラス
166 * 構造体では融通が効かない 155 * 「このデータにはこのフィールドさえあれば良い」
167 * 完全にマッチしなくてはいけない
168 * TODO: ソース
169 156
170 # 部分型 157 # Agda 上の Meta CodeSegment
171 * DataSegment が持つべき制約を表現できる型 158 # Agda 上の Meta DataSegment
172 * 型 T が期待される文脈で S を用いても良い、というようなことができる
173 * 「S <: T」で「S は T の部分型である」と読む
174 * 全てのDataSegment に対して「MDS <: DS」となるような MDS を用意する
175 * DataSegment X が期待される CodeSegment に Meta DataSegment を渡してやる
176 159
177 # 入力の部分型 160 # Agda 上に CbC を記述した成果
178 # 出力の部分型 161 * 部分型で CbC の型付けができた
179 162 * メタ計算をきちんと階層化できた
180 # 部分型で何ができたか? 163 * メタ計算にもメタ計算が適用可能
181 * Meta CodeSegment を部分型とすることで 164 * 赤黒木で利用しているデータ構造スタックの性質を証明できた
182 * ノーマルレベルの CodeSegment の前後に処理を入れても型は整合する 165 * 任意の回数だけ値を積んで同じだけ取り出すとスタックは変化しない
183 * Meta CodeSegment を CodeSegment とすることで階層構造を作れる
184 * Meta DataSegment を部分型とすることで
185 * ノーマルレベルからはアクセスできないデータを保持してもOK
186 * ノーマルレベルに Meta DataSegment を渡しても良い
187 * こちらも階層構造を取ることができる
188
189 # SingleLinkedStack の証明
190 * 証明支援系 Agda に GearsOS のデータ構造 SingleLinkedStack を定義
191 * スタックは赤黒木に用いられている
192 * その性質を証明する
193 * 性質もいくつか考えられる
194 * 「push して pop するとスタックは元に戻る」
195
196 # Agda を用いた証明手法
197 * 基本的にはデータの構造に関する帰納法
198 * スタックは内部に SingleLinkedList を持つ
199 * SingleLinkedList は NULL か値と次のノードを持つ
200 * 値がある場合と無い場合との場合分け
201 * 挿入する要素を指定せずに push を呼ぶとどうなるのか?
202 * 実装依存のコード
203 * 証明には表れる
204 * TODO: かく...
205 166
206 # まとめ 167 # まとめ
207 * Continuation based C 言語を対象にした二種類の検証アプローチ 168 * Continuation based C 言語を対象にした二種類の検証アプローチ
208 * モデル検査的なアプローチ 169 * モデル検査的なアプローチ
209 * 継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装 170 * 継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装
215 176
216 # 今後の課題 177 # 今後の課題
217 * 部分型を利用してCbCを型付け 178 * 部分型を利用してCbCを型付け
218 * 依存型をCbC に導入して自身を証明可能にする 179 * 依存型をCbC に導入して自身を証明可能にする
219 * 型情報から stub を自動生成すkる 180 * 型情報から stub を自動生成すkる
220 * 赤黒木の挿入を証明する 181 * 赤黒木の挿入に関する性質を証明する
221 182
222 <!-- vim: set filetype=markdown.slide: --> 183 <!-- vim: set filetype=markdown.slide: -->
223 184