|
0
|
1 -title: Gears OSの CodeGear Management
|
|
|
2
|
|
|
3 -author: 河野真治
|
|
|
4
|
|
1
|
5 --Gears OSによる信頼できるサービス
|
|
|
6
|
|
|
7 サービスやアプリケーションの信頼性は、OSとユーザプログラムのように分離することはできない。
|
|
|
8 プログラムの正しさは基本的にはコードの正しさであり、今のOSのようにコードの管理をユーザ空間の
|
|
|
9 問題として放り出す方法には限界がある。
|
|
|
10
|
|
|
11 Gears OSでは実行単位として codeGear、データ単位として dataGear を使う。さらに、これらは
|
|
|
12 Monad のようにメタ codeGeearやメタdataGearを持っている。
|
|
|
13
|
|
|
14 Gears OSでの検証は、Agdaを使った GearsAgdaを用いる。これらの実行と並列実行は、
|
|
|
15 GearsAgdaに対して定義される。当然、すべてのGearsAgdaのcodeGearは、Gears OSに
|
|
|
16 登録されることになる。
|
|
|
17
|
|
|
18 この論文では、Gears OSのcodeGearの管理方法について考察する。
|
|
0
|
19
|
|
|
20 --Normal and Meta computation
|
|
|
21
|
|
1
|
22 Gears OSの基本は、CbC (Continuation based C)であり、input interfaceとoutput interfaceを有限な処理で
|
|
|
23 結ぶものになっている。これは、コンパイラの基本ブロックに大体相当する。これはさらに、GearsAgdaの
|
|
|
24 Agdaで記述された invariant あるいは、表示的意味論と直結している。
|
|
|
25
|
|
|
26 CbCの記述は以下のようなものである。
|
|
|
27
|
|
|
28 __code startTimer(struct TimerImpl* timer, __code next(...)) {
|
|
|
29 struct timeval tv;
|
|
|
30 gettimeofday(&tv, NULL);
|
|
|
31 timer->time = tv.tv_sec + (double)tv.tv_usec*1e-6;
|
|
|
32 goto next(...);
|
|
|
33 }
|
|
|
34
|
|
|
35 nextが軽量継続を表している。このcodeGearの実行は論理的に割り込まれない。つまり、並行実行は
|
|
|
36 この単位で行われ定義される。ハードウェアでの並行実行、割り込み処理などは、それにそって
|
|
|
37 実装される必要がある。これらは、GearsAgdaでは、外部環境へのアクセスがある。この場合は
|
|
|
38 時刻に対するアクセスである。
|
|
|
39
|
|
|
40 OS側からみると、これは詳細のない単なるコードに見える。実行の詳細、つまり、実行に関係する
|
|
|
41 すべての dataGear 、すべてのcodeGearは、プロセスに相当する Context metaDataGearに格納される。
|
|
|
42
|
|
|
43 つまり、OSからみた codeGearの実行は、
|
|
|
44
|
|
|
45 Contextから詳細を取り出すmeta codeGearの番号から、codeGearを選ぶ
|
|
|
46 それを実行し、continuation としてshcedulerを指定する
|
|
|
47 これを CPU worker 毎に実行する
|
|
|
48
|
|
|
49 ということになる。CPU worker毎に Contextは一つなので、Contextはsingle threadで実行される。
|
|
|
50 これにより、並行実行の単位はcodeGearとなる。
|
|
|
51 ただし、Context関の共有データがある場合は意味的なずれがでる場合がある。それは、
|
|
|
52 Contextの実行をそうなるように実装することになる。
|
|
|
53
|
|
|
54 その実装の正しさは、実装を GearsAgdaで記述することより可能になるが、その実装が物理的に一致するかどうかの
|
|
|
55 保証はハードウェアの性質に依存する。
|
|
|
56
|
|
|
57 外界との対応もメタ計算になるが、それはGearsAgdaによるシミュレーションに対する正しさということになる。
|
|
|
58
|
|
|
59 scheduler から codeGearへの移行は、以下のmeta codeGear で実装される。
|
|
|
60
|
|
|
61 __code meta(struct Context* context, enum Code next) {
|
|
|
62 goto (context->code[next])(context);
|
|
|
63 }
|
|
|
64
|
|
|
65
|
|
|
66 \verb+context->code[next]+が codeGearのtableの呼び出しになるが、
|
|
|
67 これは表がコンパイル時に確定し、直接の呼び出しでは、コンパイラが最適化するので、overhead とはならない。
|
|
|
68 meta が書き換えられている場合は、ここで Context switchが起きることになる。
|
|
|
69
|
|
|
70 このContext switchでメモリ空間の切り替えが必要かどうかは application に依存する。
|
|
|
71 もし、codeGearの実行の正しさが証明されているなら、メモリ空間を切り替える必然性はない。
|
|
|
72 実際、Kernel 内や Realtime Monitor では切り替えない方が普通である。
|
|
|
73
|
|
|
74 --証明付きのコード
|
|
|
75
|
|
|
76 GearsAgdaで記述されていれば、codeGearやdataGearは証明を持つ。これらは単なる型なので実行時には
|
|
|
77 実態を持たない。ただし、それを実行時にチェックすることもできる。assertなどと同じ扱いである。
|
|
|
78
|
|
|
79 GearsAgdaの証明に閉じていれば、その範囲内での信頼性がある。しかし、動的にcodeが読み込まれる場合は
|
|
|
80 そうはならない。その時には、証明しなおす、簡易あるいは詳細なモデル検査を実施するなどが可能だが、
|
|
|
81 それらが実用的とは限らない。
|
|
|
82
|
|
|
83 codeはContextの表に登録されるが、システム全体のcodeは Database で管理される。その管理は
|
|
|
84 ファイルシステム上でも良い。codeは証明が付属している場合もあるが、それは何らかの形で
|
|
|
85 codeGear Databseに格納される。
|
|
|
86
|
|
2
|
87 現状では、証明はAgdaで記述されたデータ構造でしかない。それをcodeGear DBに入れても利用する方法は
|
|
|
88 ないがいくつかの利用法は考えられる。
|
|
1
|
89
|
|
2
|
90 証明とcodeGearの一致を確認する
|
|
|
91 型整合に使う
|
|
|
92 codeの認証に使う
|
|
1
|
93
|
|
2
|
94 この大域のcodeGear DBは、kernelを含めたすべてのcodeGearに対するもので全部で共有される。つまり、
|
|
|
95 あらゆるversionを含む共有ライブラリとなる。これは全世界でuniqueなDBとしても良い。
|
|
|
96
|
|
|
97 --codeGearのlinkage
|
|
1
|
98
|
|
2
|
99 Gears OSのあらゆるコードは、codeGear DBのコードの組み合わせになる。しかし、そのためには、
|
|
|
100 Contextから詳細なデータを取り出して、実行し、次のcodeGearを呼び出す時にContextの正しい場所にdataGearを格納する
|
|
|
101 必要がある。これは codeGear 全体に対して必要になる。
|
|
1
|
102
|
|
2
|
103 現状では、これは stubとしてコンパイル時に生成される。
|
|
1
|
104
|
|
2
|
105 __code checkAndSetAtomicReference(struct AtomicReference* atomic, union Data** ptr, union Data* oldData, union Data* newData, __code next(...), __code fail(...)) {
|
|
|
106 if (__sync_bool_compare_and_swap(ptr, oldData, newData)) {
|
|
|
107 goto next(...);
|
|
|
108 }
|
|
|
109 goto fail(...);
|
|
|
110 }
|
|
|
111
|
|
|
112 では、Context 上には以下の構造と、それを呼び出す stub がある。
|
|
0
|
113
|
|
2
|
114 struct Atomic {
|
|
|
115 union Data* atomic;
|
|
|
116 union Data** ptr;
|
|
|
117 union Data* oldData;
|
|
|
118 union Data* newData;
|
|
|
119 enum Code checkAndSet;
|
|
|
120 enum Code next;
|
|
|
121 enum Code fail;
|
|
|
122 } Atomic;
|
|
0
|
123
|
|
2
|
124 __code checkAndSetAtomicReference_stub(struct Context* context) {
|
|
|
125 AtomicReference* atomic = (AtomicReference*)GearImpl(context, Atomic, atomic);
|
|
|
126 Data** ptr = Gearef(context, Atomic)->ptr;
|
|
|
127 Data* oldData = Gearef(context, Atomic)->oldData;
|
|
|
128 Data* newData = Gearef(context, Atomic)->newData;
|
|
|
129 enum Code next = Gearef(context, Atomic)->next;
|
|
|
130 enum Code fail = Gearef(context, Atomic)->fail;
|
|
|
131 goto checkAndSetAtomicReference(context, atomic, ptr, oldData, newData, next, fail);
|
|
|
132 }
|
|
0
|
133
|
|
2
|
134 これらは単一のGears OS内で整合する必要がある。実際には、これらは、stubが参照する Context内のoffsetにすぎない。
|
|
|
135 Atomic は dataGear の巨大な Union になっている。これは、GearsAgda でも状況は同じで、巨大な Sum type になっている。
|
|
|
136
|
|
|
137 このContext内での offsetと呼び出すcodeGearの番号が一致すれば、Kernel側で整合性の問題はない。
|
|
|
138
|
|
|
139 --static linkage
|
|
|
140
|
|
|
141 コンパイル時に codeGearの結合が明らかならば、それは一つのcodeGearとしてまとめてよい。Contextへの書き込みもさぼることが
|
|
|
142 可能になる。ただし、時分割実行される場合は、codeGearの切れ目で分割するのと同じ実行が要求される。
|
|
|
143 つまり、割り込み処理などで途中で実行が中断するならば、それはその単位まで実行してから、Contextを切り替える必要がある。
|
|
0
|
144
|
|
2
|
145 これを実現する手法はflagを参照する方法や、コードを書き換える方法あるいは、polingを埋め込むなどの方法が考えられる。
|
|
|
146 整合性が不要であれば途中で止めても問題ないが、その場合は register などの状態を従来のOSのように保持する必要がある。
|
|
|
147
|
|
|
148 codeGear単位で正直に分割コンパイルすると最適化の余地がない。しかし、その場合でもJITなどは可能である。
|
|
|
149
|
|
|
150 --boot codeGear
|
|
|
151
|
|
|
152 今の実装では、UEFIから Gears OSが読み出される。Gears OS自体は、x.v6\cite{}と同じで、ファイルシステムを
|
|
|
153 含む一体の binary になっている。
|
|
|
154
|
|
|
155 codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。
|
|
0
|
156
|
|
|
157 --まとめ
|
