|
26
|
1 ---
|
|
|
2 marp: true
|
|
|
3 title: GearsOSのメタ計算
|
|
|
4 paginate: true
|
|
|
5 ---
|
|
|
6
|
|
|
7
|
|
116
|
8 # GearsOSのメタ計算
|
|
26
|
9
|
|
|
10 - 清水 隆博
|
|
116
|
11 - 琉球大学理工学研究科
|
|
26
|
12 - 198584B
|
|
|
13 - 河野研
|
|
|
14
|
|
116
|
15 ---
|
|
|
16 # 研究発表の構成
|
|
|
17 - 研究目的
|
|
|
18 - CbC、GearsOSの基礎概念
|
|
|
19 - 本研究での新たなGearsOSのシステムの解説
|
|
|
20 - GearsOSのInterfaceシステムの改善
|
|
|
21 - Perlトランパイラの改善
|
|
|
22
|
|
26
|
23
|
|
|
24 ---
|
|
|
25
|
|
|
26 # 研究目的
|
|
|
27
|
|
116
|
28 - アプリケーションの信頼性を保証したい
|
|
|
29 - この為には土台のOSの信頼性を高く保証する必要がある
|
|
26
|
30 - OSそのものも巨大なプログラム
|
|
116
|
31 - プログラムの信頼性の保証にはテストが一般的に使われる
|
|
26
|
32 - 並列並行処理など起因するバグや、そもそもOSを構成する処理が巨大
|
|
|
33 - テストコードで信頼性を保証しきれない
|
|
116
|
34 - 形式手法を用いてテストに頼らず信頼性を保証したい
|
|
|
35 - 定理証明
|
|
26
|
36 - モデル検査
|
|
|
37
|
|
|
38 ---
|
|
|
39
|
|
|
40 # ノーマルレベルとメタレベルを用いた信頼性の向上
|
|
|
41
|
|
|
42 - プログラムの実行部分は以下の2つからなる
|
|
|
43 - 入力と出力の関係を決める計算(ノーマルレベル)
|
|
|
44 - プログラムを実行したり、 信頼性を保証するために必要な計算(メタレベル)
|
|
|
45 - メタレベルの例
|
|
|
46 - メモリやCPUの資源管理
|
|
|
47 - システムコールの動作(副作用)
|
|
|
48 - 並行実行(他のプロセスとの干渉)
|
|
|
49 - モデル検査(可能な実行を列挙する方式の実行)
|
|
|
50 - 証明(入力時と出力時の論理的な条件)、(invariant)
|
|
|
51 - メタレベルの計算として信頼性を保証する
|
|
|
52
|
|
|
53 ---
|
|
116
|
54 # メタレベルの計算とGearsOS
|
|
|
55 - ノーマルレベル、メタレベルを一貫して記述できる言語CbCを用いてGearsOSを開発している
|
|
|
56 - GearsOSのメタレベルの処理は従来のものは手動で行うものが多かった
|
|
|
57 - 計算で使うすべてのデータ構造の管理
|
|
|
58 - 別のInterfaceの出力を受けるメタレベルの処理
|
|
|
59 - Perlでメタレベルに変換された後で気づくエラーも多い
|
|
|
60 - ノーマルレベルで検知したい
|
|
|
61
|
|
|
62 ---
|
|
26
|
63
|
|
|
64 # モデル検査
|
|
116
|
65 - プログラムの可能な実行を数え上げて仕様を満たしているかどうかの確認
|
|
26
|
66 - 実際に想定されるパターンを全て動かして検証する
|
|
|
67 - デッドロック発生の検知
|
|
|
68 - JavaPathFinderなど
|
|
|
69 - 状態爆発が問題になる
|
|
|
70 - Spinを用いる方法では、 promelaという言語で実装し直す必要がある
|
|
116
|
71 - 実装を変更せず、カジュアルにモデル検査を行いたい
|
|
26
|
72
|
|
|
73 ---
|
|
|
74
|
|
|
75 # 定理証明支援系
|
|
|
76 - 論理学的なモデルに変更して証明する
|
|
|
77 - Agda
|
|
|
78 - Coq
|
|
|
79 - HoareLogicを用いる
|
|
|
80 - PreCondition -> Statement -> PostCondition
|
|
|
81 - 従来の方法ではStatementには限られたコマンドしか使えない
|
|
|
82 - ループは不変条件を使うが、 条件を見つけることが一般的には困難
|
|
|
83 - 実装言語と同じ記述で証明をすることはできない
|
|
|
84
|
|
|
85 ---
|
|
|
86 # GearsOSでの信頼性の保証
|
|
|
87 - メタレベルのみで信頼性の保証を行う
|
|
|
88 - ノーマルレベルでの記述は変更しない
|
|
|
89 - Continuation Based C(CbC)をつかって、ノーマルレベルとメタレベルの分離を行う
|
|
|
90 - C言語の下位言語であり、 いくつかのCコンパイラ上で実装している
|
|
|
91 - C言語の構文は使用可能だが、 関数呼び出しの他に軽量継続を持つ
|
|
|
92 - 関数呼び出し時のスタックの操作を行わず`jmp`命令で次の処理に移動する
|
|
|
93 - schemaなどと違い環境を持たず継続するために軽量継続と呼ぶ
|
|
|
94
|
|
|
95 ---
|
|
|
96 # GearsOSでの信頼性の保証
|
|
|
97
|
|
|
98 - デフォルトのメタレベルの計算は自動生成される
|
|
|
99 - 資源管理あるいは検証用のメタ計算は必要に応じて挿入する
|
|
|
100 - これにより大きなコード変更が無くモデル検査や定理証明を行うことができる
|
|
|
101 - モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する
|
|
|
102 - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮
|
|
|
103 - OSの検証に利用できるinvariantの提供
|
|
|
104 - CbCを用いたOSであるGearsOSを開発している
|
|
|
105
|
|
|
106 ---
|
|
116
|
107 # GearsOSの課題(1)
|
|
|
108 ### 本研究で改善した従来のGearsOSの課題を列挙する
|
|
|
109
|
|
|
110 - メタレベルの計算、データの定義を従来は手動で行っていた
|
|
|
111 - 自動的にコンパイル時に決定するはずの情報をすべて手書き
|
|
|
112 - メタレベルのCodeGearの定義やユーザーからの制御が困難であった
|
|
|
113 - モデル検査などをメタ計算として定義できない
|
|
|
114 - 書いたGearsOSのプログラムを、メタを含むコードに変換し、コンパイルしないとバグに気づかない状態があった
|
|
|
115 - メタを含むコードに変換する前に気づきたい
|
|
|
116 - 例題を作製する際にコピペを行う回数が多く、バグを発生させがちであった
|
|
|
117
|
|
|
118 ---
|
|
|
119 # GearsOSの課題(2)
|
|
|
120 - Interfaceシステムが不十分
|
|
|
121 - 未実装のAPIがあっても警告が発生しない
|
|
|
122 - メソッド呼び出し時の引数の数が足りなくても警告が発生しない
|
|
|
123 - 定義していないAPIを呼び出してもエラーが出ない
|
|
|
124 - 並行呼び出しに対応していなかった
|
|
|
125 - Interfaceの実装の型には型定義ファイルが存在しなかった
|
|
|
126 - 型定義の方法の一貫性がなかった
|
|
|
127 - メタ情報を手動で実装する必要性があった
|
|
|
128 - Interface間の連携が上手くいっていなかった
|
|
|
129 - 入出力の受け取りするメタ部分を手動で実装する必要があった
|
|
|
130
|
|
|
131 ---
|
|
|
132 # 研究発表の構成
|
|
|
133 - 研究目的
|
|
|
134 - **CbC、GearsOSの基礎概念**
|
|
|
135 - 本研究での新たなGearsOSのシステムの解説
|
|
|
136 - GearsOSのInterfaceシステムの改善
|
|
|
137 - Perlトランパイラの改善
|
|
|
138
|
|
|
139 ---
|
|
|
140 # GearsOSの基礎概念
|
|
|
141 - CodeGear、DataGear
|
|
|
142 - Interface
|
|
|
143 - par goto
|
|
|
144 - GearsOSのビルドシステム
|
|
|
145 - cmake
|
|
|
146 - Perlトランスパイラ
|
|
|
147
|
|
|
148 ---
|
|
26
|
149 # CbCとCodeGear(ノーマルレベル)
|
|
|
150 - 軽量継続で表現する単位をCodeGearと呼ぶ
|
|
|
151 - CodeGearはCの関数とアセンブラの中間の様に使える
|
|
|
152 - CodeGearは返り値の型の代わりに`__code`で宣言する
|
|
|
153
|
|
|
154
|
|
|
155 ---
|
|
116
|
156 # DataGear
|
|
|
157 - GearsOSで扱うデータの単位
|
|
|
158 - Cの構造体の形でメタレベルでは表現される
|
|
|
159 - GearsOS自体の処理にかかわるMetaDataGearが存在する
|
|
|
160 - Context(プロセス)
|
|
|
161 - TaskManager
|
|
|
162 - Worker
|
|
|
163 - ...
|
|
|
164 - DataGearの定義ではInterfaceシステムが使用できる
|
|
26
|
165
|
|
|
166 ---
|
|
116
|
167 # Interface
|
|
|
168 - GearsOSのモジュール化の仕組み
|
|
|
169 - Interface はある Data Gear と、それに対する操作(API)を行う Code Gear とその操作に用いる Data Gear の集合を表現する。
|
|
|
170 - JavaのInteface、Haskellの型クラスに相当する
|
|
|
171 - GearsOSではこの他にもgoto時の値の保管に利用される
|
|
26
|
172
|
|
116
|
173 ---
|
|
|
174 # Interfaceの定義
|
