|
102
|
1 title: メタ計算を用いた Continuation based C の検証手法
|
|
|
2 author: Yasutaka Higa
|
|
|
3 profile:
|
|
|
4 lang: Japanese
|
|
|
5
|
|
|
6
|
|
|
7 # プログラミング言語とソフトウェアの信頼性
|
|
|
8 * 信頼性の高いソフトウェアを提供したい
|
|
|
9 * ソフトウェアの仕様を検証するには二つの手法がある
|
|
|
10 * プログラムの持つ状態を数え上げ、仕様から外れた状態が無いかを確認するモデル検査
|
|
|
11 * プログラムの性質を直接証明してしまう定理証明
|
|
|
12 * モデル検査も証明も行ないやすい言語として Continuation based C 言語を開発している
|
|
|
13
|
|
|
14 # 二つのアプローチを用いたソフトウェア検証
|
|
|
15 * モデル検査的アプローチ
|
|
|
16 * メタ計算ライブラリ akasha による網羅的な実行
|
|
|
17 * 非破壊赤黒木の仕様定義と検証
|
|
|
18 * 定理証明的なアプローチ
|
|
|
19 * 依存型を持つ証明支援系言語 Agda による CbC の証明
|
|
|
20 * 部分型を利用して Agda 上に型付きの CbC の項を記述する
|
|
|
21 * 型システムを通して CbC の形式的な定義を得る
|
|
|
22 * SingleLinkedStack の性質の証明
|
|
|
23
|
|
|
24 # Continuation based C
|
|
|
25 * 当研究室で開発しているプログラミング言語
|
|
|
26 * アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語
|
|
|
27 * OS や組み込みソフトウェアなどを対象にしている
|
|
|
28 * CodeSegment と DataSegment という単位を用いてプログラミングする
|
|
|
29
|
|
|
30 # CodeSegment
|
|
|
31 * CodeSegment とは
|
|
|
32 * 処理の単位
|
|
|
33 * 結合や分割が容易
|
|
|
34 * 入力と出力を持つ
|
|
|
35 * CodeSegment どうしを接続することによりプログラム全体を作る
|
|
|
36 * TODO: 図
|
|
|
37
|
|
|
38 # DataSegment
|
|
|
39 * DataSegment とは
|
|
|
40 * データの単位
|
|
|
41 * CodeSegment の入出力にあたる
|
|
|
42 * 接続元の Output DataSegment は接続先の Input DataSegment
|
|
|
43 * TODO: 図
|
|
|
44
|
|
|
45 # メタ計算
|
|
|
46 * とある計算を実現するための計算
|
|
|
47 * ネットワーク接続、例外処理、メモリ確保、並列処理など
|
|
|
48 * 時に本来行ないたい処理よりも複雑になる
|
|
|
49 * CbC は通常レベルの計算とメタ計算を分離して考える
|
|
|
50 * 通常レベルではポインタは出てこない、など
|
|
|
51 * TODO: 図
|
|
|
52
|
|
|
53 # Meta CodeSegment
|
|
|
54 * メタ計算を行なう CodeSegment
|
|
|
55 * 通常の CodeSegment どうしの接続の間に入る
|
|
|
56 * TODO: 図
|
|
|
57
|
|
|
58 # Meta DataSegment
|
|
|
59 * メタ計算用の DataSegment
|
|
|
60 * 通常の DataSegment を含むような DataSegment
|
|
|
61 * TODO: 図
|
|
|
62
|
|
|
63 # C言語との対応
|
|
|
64 * CodeSegment は C 言語における返り値の無い関数
|
|
|
65 * DataSegment は C 言語における構造体
|
|
|
66 * Meta CodeSegment は CodeSegment の前後にある CodeSegment
|
|
|
67 * Meta DataSegment は全ての DataSegment の共用体を持つ構造体
|
|
|
68 * CodeSegment の接続は goto における軽量継続
|
|
|
69 * 末尾のみで行なうスタックを保持しない関数呼び出し
|
|
|
70
|
|
|
71 # 並列に信頼性高く動作する GearsOS
|
|
|
72 * CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある
|
|
|
73 * 並列実行やモデル検査をメタ計算として提供する
|
|
|
74 * 現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み
|
|
|
75 * 今回はこの非破壊赤黒木の検証を行なう
|
|
|
76
|
|
|
77 # 赤黒木
|
|
|
78 * データの保存に用いる二分木
|
|
|
79 * 特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
|
|
|
80 * ルートノードと葉ノードの色は黒
|
|
|
81 * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)
|
|
|
82 * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定
|
|
|
83 * TODO: 図
|
|
|
84
|
|
|
85 # GearsOS における赤黒木の利用例(ノードの挿入)
|
|
|
86 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
|
|
|
87 * goto する前に Meta CodeSegment が実行されて木に挿入する
|
|
|
88 * GearsOS では木の実装のためにスタックを用いて経路情報を保持している
|
|
|
89 * TODO: 図
|
|
|
90
|
|
|
91 # 仕様の記述とその確認
|
|
|
92 * 「バランスが取れている」とは何かを表現できる必要がある
|
|
|
93 * 実行可能な CbC の式を使った assert になる
|
|
|
94 * そしてそれを保証したい
|
|
|
95 * プログラムの全ての状態においてこれは常に成り立つのか?
|
|
|
96
|
|
|
97 # 既存のモデル検査器 spin
|
|
|
98 * spin
|
|
|
99 * promela と呼ばれる言語でプログラムを記述
|
|
|
100 * 並列に動作するプログラムの仕様を検証可能
|
|
|
101 * 検証した promela から実行可能な C ソースを生成可能
|
|
|
102 * 仕様は bool になる式を用いた assert
|
|
|
103 * promela は C とは記述が異なる
|
|
|
104
|
|
|
105 # 既存のモデル検査器 CBMC
|
|
|
106 * CBMC
|
|
|
107 * 検証対象のCソースを変更しないでも良い
|
|
|
108 * C/C++ 言語の記号実行が可能
|
|
|
109 * 条件分岐を網羅的に実行
|
|
|
110 * 仕様は bool になる式を用いた assert
|
|
|
111 * 有限ステップ検証する有界モデル検査器
|
|
|
112
|
|
|
113 # メタ計算ライブラリ akasha
|
|
|
114 * メタ計算としてプログラムの状態を数え上げる
|
|
|
115 * goto された時に挿入される要素の組み合わせを全て列挙して実行する
|
|
|
116 * その度に仕様の式は成り立つかをチェックする
|
|
|
117 * TODO: 図
|
|
|
118
|
|
|
119 # チェックする仕様
|
|
|
120 * TODO: たかさについて
|
|
|
121
|
|
|
122 # akasha と CBMC の比較
|
|
|
123 * akasha は有限の要素数の組み合わせをチェックする
|
|
|
124 * 要素数が13個までならどの順で木に挿入しても良い
|
|
|
125 * 比較対象として C Bounded Model Checker を使用した
|
|
|
126 * C/C++ の記号実行を行なう
|
|
|
127 * 実行可能なステップ数411だけ展開しても仕様は満たされる
|
|
|
128 * が、恣意的にバグを入れ込んでも反例を返さない
|
|
|
129 * akasha は返した
|
|
|
130 * 固定の要素数までの仕様検査で十分なのか?
|
|
|
131
|
|
|
132 # 定理証明
|
|
|
133 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
|
|
|
134 * そのままプログラムの性質を保証してやる
|
|
|
135 * プログラムと証明は Curry-Howard Isomorphism により、自然演繹と型付ラムダ計算が対応
|
|
|
136 * プログラムにおける命題は型であり、証明はその導出が存在するかどうか
|
|
|
137 * 例えば三段論法が書ける
|
|
|
138 * (A -> B) -> (B -> C) -> (A -> C)
|
|
|
139 * (int -> bool) -> (bool -> float) -> (int -> float)
|
|
|
140
|
|
|
141 # 証明支援系 Agda
|
|
|
142 * 依存型を持つ言語
|
|
|
143 * 型が第一級(型が値である)
|
|
|
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
|
|
|
159 # メタレベルの型付け
|
|
|
160 * Meta CodeSegment が持っているべき性質
|
|
|
161 * メタレベルは階層構造を持つ
|
|
|
162 * メタ計算は組み合わせられる
|
|
|
163 * ノーマルレベルの DataSegment を一様に扱える
|
|
|
164 * ノーマルレベルの CodeSegment へと goto できる
|
|
|
165 * どんなプログラムからもライブラリとして使える
|
|
|
166 * 構造体では融通が効かない
|
|
|
167 * 完全にマッチしなくてはいけない
|
|
|
168 * TODO: ソース
|
|
|
169
|
|
|
170 # 部分型
|
|
|
171 * DataSegment が持つべき制約を表現できる型
|
|
|
172 * 型 T が期待される文脈で S を用いても良い、というようなことができる
|
|
|
173 * 「S <: T」で「S は T の部分型である」と読む
|
|
|
174 * 全てのDataSegment に対して「MDS <: DS」となるような MDS を用意する
|
|
|
175 * DataSegment X が期待される CodeSegment に Meta DataSegment を渡してやる
|
|
|
176
|
|
|
177 # 入力の部分型
|
|
|
178 # 出力の部分型
|
|
|
179
|
|
|
180 # 部分型で何ができたか?
|
|
|
181 * Meta CodeSegment を部分型とすることで
|
|
|
182 * ノーマルレベルの CodeSegment の前後に処理を入れても型は整合する
|
|
|
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
|
|
|
206 # まとめ
|
|
|
207 * Continuation based C 言語を対象にした二種類の検証アプローチ
|
|
|
208 * モデル検査的なアプローチ
|
|
|
209 * 継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装
|
|
|
210 * 有限の要素数まで保証できた
|
|
|
211 * 証明的なアプローチ
|
|
|
212 * 証明支援系 Agda 上で CbC のプログラムを定義して直接証明
|
|
|
213 * 部分型を利用して CbC を型付け
|
|
|
214 * データ構造 SingleLinkedStack の証明ができた
|
|
|
215
|
|
|
216 # 今後の課題
|
|
|
217 * 部分型を利用してCbCを型付け
|
|
|
218 * 依存型をCbC に導入して自身を証明可能にする
|
|
|
219 * 型情報から stub を自動生成すkる
|
|
|
220 * 赤黒木の挿入を証明する
|
|
|
221
|
|
|
222 <!-- vim: set filetype=markdown.slide: -->
|
|
|
223
|
