|
26
|
1 ---
|
|
|
2 marp: true
|
|
|
3 title: GearsOSのメタ計算
|
|
|
4 paginate: true
|
|
|
5 ---
|
|
|
6
|
|
|
7
|
|
|
8 # <!--fit--> GearsOSのメタ計算
|
|
|
9
|
|
|
10 - 清水 隆博
|
|
|
11 - 198584B
|
|
|
12 - 河野研
|
|
|
13
|
|
|
14
|
|
|
15 ---
|
|
|
16
|
|
|
17 # 研究目的
|
|
|
18
|
|
|
19 - アプリケーションの信頼性を向上させたい
|
|
|
20 - その為には土台となる OS 自体の信頼性が重要である
|
|
|
21 - OSそのものも巨大なプログラム
|
|
|
22 - 並列並行処理など起因するバグや、そもそもOSを構成する処理が巨大
|
|
|
23 - テストコードで信頼性を保証しきれない
|
|
|
24 - 形式手法を用いて信頼性を保証したい
|
|
|
25 - モデル検査
|
|
|
26
|
|
|
27 ---
|
|
|
28
|
|
|
29 # ノーマルレベルとメタレベルを用いた信頼性の向上
|
|
|
30
|
|
|
31 - プログラムの実行部分は以下の2つからなる
|
|
|
32 - 入力と出力の関係を決める計算(ノーマルレベル)
|
|
|
33 - プログラムを実行したり、 信頼性を保証するために必要な計算(メタレベル)
|
|
|
34 - メタレベルの例
|
|
|
35 - メモリやCPUの資源管理
|
|
|
36 - システムコールの動作(副作用)
|
|
|
37 - 並行実行(他のプロセスとの干渉)
|
|
|
38 - モデル検査(可能な実行を列挙する方式の実行)
|
|
|
39 - 証明(入力時と出力時の論理的な条件)、(invariant)
|
|
|
40 - メタレベルの計算として信頼性を保証する
|
|
|
41
|
|
|
42 ---
|
|
|
43
|
|
|
44 # モデル検査
|
|
|
45 - 実際に想定されるパターンを全て動かして検証する
|
|
|
46 - デッドロック発生の検知
|
|
|
47 - JavaPathFinderなど
|
|
|
48 - 状態爆発が問題になる
|
|
|
49 - Spinを用いる方法では、 promelaという言語で実装し直す必要がある
|
|
|
50
|
|
|
51 ---
|
|
|
52
|
|
|
53 # 定理証明支援系
|
|
|
54 - 論理学的なモデルに変更して証明する
|
|
|
55 - Agda
|
|
|
56 - Coq
|
|
|
57 - HoareLogicを用いる
|
|
|
58 - PreCondition -> Statement -> PostCondition
|
|
|
59 - 従来の方法ではStatementには限られたコマンドしか使えない
|
|
|
60 - ループは不変条件を使うが、 条件を見つけることが一般的には困難
|
|
|
61 - 実装言語と同じ記述で証明をすることはできない
|
|
|
62
|
|
|
63 ---
|
|
|
64 # GearsOSでの信頼性の保証
|
|
|
65 - メタレベルのみで信頼性の保証を行う
|
|
|
66 - ノーマルレベルでの記述は変更しない
|
|
|
67 - Continuation Based C(CbC)をつかって、ノーマルレベルとメタレベルの分離を行う
|
|
|
68 - C言語の下位言語であり、 いくつかのCコンパイラ上で実装している
|
|
|
69 - C言語の構文は使用可能だが、 関数呼び出しの他に軽量継続を持つ
|
|
|
70 - 関数呼び出し時のスタックの操作を行わず`jmp`命令で次の処理に移動する
|
|
|
71 - schemaなどと違い環境を持たず継続するために軽量継続と呼ぶ
|
|
|
72
|
|
|
73 ---
|
|
|
74 # GearsOSでの信頼性の保証
|
|
|
75
|
|
|
76 - デフォルトのメタレベルの計算は自動生成される
|
|
|
77 - 資源管理あるいは検証用のメタ計算は必要に応じて挿入する
|
|
|
78 - これにより大きなコード変更が無くモデル検査や定理証明を行うことができる
|
|
|
79 - モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する
|
|
|
80 - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮
|
|
|
81 - OSの検証に利用できるinvariantの提供
|
|
|
82 - CbCを用いたOSであるGearsOSを開発している
|
|
|
83
|
|
|
84 ---
|
|
|
85 # CbCとCodeGear(ノーマルレベル)
|
|
|
86 - 軽量継続で表現する単位をCodeGearと呼ぶ
|
|
|
87 - CodeGearはCの関数とアセンブラの中間の様に使える
|
|
|
88 - CodeGearは返り値の型の代わりに`__code`で宣言する
|
|
|
89
|
|
|
90 ```
|
|
|
91 __code cbc_read(__code (*next)(int ret)){
|
|
|
92 struct file *f;
|
|
|
93 int n;
|
|
|
94 char *p;
|
|
|
95
|
|
|
96 if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
|
|
|
97 goto next(-1);
|
|
|
98 }
|
|
|
99 goto cbc_fileread(f, p, n, next);
|
|
|
100 }
|
|
|
101 ```
|
|
|
102 - cbcで書き直したxv6の`read`システムコールの例
|
|
|
103
|
|
|
104
|
|
|
105 ---
|
|
|
106 # CbCとCodeGear(メタレベル)
|
|
|
107
|
|
|
108 - `cbc_read_stub`内で必要な引数をcontextから取り出す
|
|
|
109 - 取得するものがなければノーマルレベルのCodeGearに継続する
|
|
|
110
|
|
|
111 ```c
|
|
|
112 __code cbc_read_stub(struct Context* cbc_context, enum Code next) {
|
|
|
113 goto cbc_read(cbc_context, next);
|
|
|
114 }
|
|
|
115 ```
|
|
|
116
|
|
|
117 ---
|
|
|
118 # cbcで書き直したシステムコールディスパッチの例
|
|
|
119
|
|
|
120 - CbCは`goto`文で呼び出す
|
|
|
121 - 受け取ったシステムコール番号に対応するCodeGearに継続する
|
|
|
122
|
|
|
123 ```c
|
|
|
124 void syscall(void)
|
|
|
125 {
|
|
|
126 int num;
|
|
|
127 int ret;
|
|
|
128
|
|
|
129 if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
|
|
|
130 proc->cbc_arg.cbc_console_arg.num = num;
|
|
|
131 goto (cbccodes[num])(cbc_ret);
|
|
|
132 }
|
|
|
133 ```
|
|
|
134
|
