|
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
|
|
4
|
97 --CbCのcodeGear と GearsAgdaの違い
|
|
|
98
|
|
|
99 CbCのcodeGearとdataGearは、普通のCの関数と構造体であり、その意味で不思議なところはない。しかし、
|
|
|
100 normal levelではpointerが出てこないのが望ましい。なぜなら、メモリ配置は meta levelの問題で
|
|
|
101 プログラムの正しさとは直接関係しないからである。つまり、normal levelでの構造体は List や 木
|
|
|
102 など以外の再帰的構造でも直接的なポインタ操作は行わない。meta levelでは、メモリの直接操作
|
|
|
103 例えば mallocやfree、あるいは共有データの扱いなどをポインタを通して行う。
|
|
|
104
|
|
|
105 meta levelでのポインタ操作は、データ構造に対する操作であり、そのlevelに閉じる限り、
|
|
|
106 プログラムの正しさはポインタの実装に依存しない。その意味で、meta codeGear も単なる
|
|
|
107 noraml level のcodeGear に過ぎない。meta codeGearの証明あるいは、実装をさらにmeta level
|
|
|
108 で行うこともできる。
|
|
|
109
|
|
|
110 GearsAgda では、すべてはAgdaの構造体で表現される。これらは変数と項であり、基本的に複製可能
|
|
|
111 な項である。その意味で、ポインタを持たないと言ってよい。Listや木の実装を配列と番号で行う
|
|
|
112 ことはまったく実用的ではないので、普通に再帰的なデータ構造を使ってよい。ただし、それを
|
|
|
113 自分自身の codeGear の再帰呼び出しで行うと、codeGearの実行が有界な時間に閉じなくなる。
|
|
|
114 なので、loop は軽量継続を用いて、一旦、外にでることになる。これは、この段階でmeta level的に処理が
|
|
|
115 割り込まれることも意味している。
|
|
|
116
|
|
|
117 GearsAgda で処理された項は、ContextのdataGearに格納される。また、GearsAgdaのcodeGearは、
|
|
|
118 Contextのcode tableに格納される。どちらも、メモリ的には番号で管理されることになる。
|
|
|
119 GearsAgda の Context は、その意味で、プロセスのメモリ空間そのものを抽象化したものになっている。
|
|
|
120
|
|
|
121
|
|
|
122 つまり、CbCのcodeGearと GearsAgdaは、normal level ではポインタを使わないのだが、
|
|
|
123 その意味は、CbCと GearsAgda で若干異なる。CbCでの実装は、GearsAgdaでの実装の持つ
|
|
|
124 性質を保存する必要がある。
|
|
|
125
|
|
|
126 --Contextを通した dataGearとcodeGearの連携
|
|
|
127
|
|
|
128 Gears OSでは、Context はCの構造体であり、一つのContextで使用するdataGearとcodeGearは、そこに格納される。
|
|
|
129 複数のContextから、dataGearもcodeGearも共有されることがある。その排他制御は、Gears OSのmeta codeGearに
|
|
|
130 よって行われる。
|
|
|
131
|
|
|
132 Gears OSは、interfaceという構造体でオブジェクト表現していて、これらには、メソッドを格納する配列がある。
|
|
|
133 この配列の添字を他のinterfaceが使用する。なので、interface間の呼び出しは、interfaceを表すdataGearと
|
|
|
134 そのメソッドの番号で決定される。
|
|
|
135
|
|
|
136 引数は、interface毎に Contextに決まった場所が確保される。これは、通常ではstack上に場所を確保する。
|
|
|
137 しかし、CbCでは関数呼び出しはstackを使わないので、このようにする必要がある。これは、もちろん、
|
|
|
138 マルチスレッドな実行では破壊されるおそれがあるが、Contextはシングルスレッドで実行することになっている
|
|
|
139 ので問題ない。
|
|
|
140
|
|
|
141 Contextの切り替えは、codeGearの境目で行われるので、Contextと実行しているcodeGearのcode tableの番号で
|
|
|
142 状態が決定する。つまり、Gears OSでは、Task Switchにはレジスタは関係しない。割り込みなどは、codeGearの
|
|
|
143 境界と独立に起きるが、それをmeta codeGearが境界で Context switchが起きたのと同じようにすることを
|
|
|
144 保証する。これは一種の遅延処理となる。もちろん、影響がないなら、割り込み中にmetaな処理を行ってもよい。
|
|
|
145 これは、本来はCPUなどのハードウェアでサポートされるべきかもしれない。
|
|
|
146
|
|
|
147 dataGearは、metaな情報として、dataGearの構造定義を番号として持っている。これを使うことにより
|
|
|
148 任意のdataGearの表示を正しく行うことができる。この情報を取り扱うことは meta level からでしか
|
|
|
149 許されないが、CbC的には特に制限はない。
|
|
|
150
|
|
|
151 引数として呼び出される dataGearは、Context上に前もって確保されているが、実行時にallocateされる
|
|
|
152 dataGearもContextから参照される pool に確保される。これの管理は meta dataGear (Gears OSのkernel)
|
|
|
153 が行う。GearsAgda は、この部分はAgdaが管理するので meta的な管理は行われない。しかし、
|
|
|
154 Context を用いた並行実行の場合は、Context上での管理の問題が生じる。
|
|
|
155
|
|
|
156
|
|
2
|
157 --codeGearのlinkage
|
|
1
|
158
|
|
2
|
159 Gears OSのあらゆるコードは、codeGear DBのコードの組み合わせになる。しかし、そのためには、
|
|
|
160 Contextから詳細なデータを取り出して、実行し、次のcodeGearを呼び出す時にContextの正しい場所にdataGearを格納する
|
|
|
161 必要がある。これは codeGear 全体に対して必要になる。
|
|
1
|
162
|
|
2
|
163 現状では、これは stubとしてコンパイル時に生成される。
|
|
1
|
164
|
|
2
|
165 __code checkAndSetAtomicReference(struct AtomicReference* atomic, union Data** ptr, union Data* oldData, union Data* newData, __code next(...), __code fail(...)) {
|
|
|
166 if (__sync_bool_compare_and_swap(ptr, oldData, newData)) {
|
|
|
167 goto next(...);
|
|
|
168 }
|
|
|
169 goto fail(...);
|
|
|
170 }
|
|
|
171
|
|
|
172 では、Context 上には以下の構造と、それを呼び出す stub がある。
|
|
0
|
173
|
|
2
|
174 struct Atomic {
|
|
|
175 union Data* atomic;
|
|
|
176 union Data** ptr;
|
|
|
177 union Data* oldData;
|
|
|
178 union Data* newData;
|
|
|
179 enum Code checkAndSet;
|
|
|
180 enum Code next;
|
|
|
181 enum Code fail;
|
|
|
182 } Atomic;
|
|
0
|
183
|
|
2
|
184 __code checkAndSetAtomicReference_stub(struct Context* context) {
|
|
|
185 AtomicReference* atomic = (AtomicReference*)GearImpl(context, Atomic, atomic);
|
|
|
186 Data** ptr = Gearef(context, Atomic)->ptr;
|
|
|
187 Data* oldData = Gearef(context, Atomic)->oldData;
|
|
|
188 Data* newData = Gearef(context, Atomic)->newData;
|
|
|
189 enum Code next = Gearef(context, Atomic)->next;
|
|
|
190 enum Code fail = Gearef(context, Atomic)->fail;
|
|
|
191 goto checkAndSetAtomicReference(context, atomic, ptr, oldData, newData, next, fail);
|
|
|
192 }
|
|
0
|
193
|
|
2
|
194 これらは単一のGears OS内で整合する必要がある。実際には、これらは、stubが参照する Context内のoffsetにすぎない。
|
|
|
195 Atomic は dataGear の巨大な Union になっている。これは、GearsAgda でも状況は同じで、巨大な Sum type になっている。
|
|
|
196
|
|
|
197 このContext内での offsetと呼び出すcodeGearの番号が一致すれば、Kernel側で整合性の問題はない。
|
|
|
198
|
|
4
|
199 --codeGearのコンパイル方法
|
|
|
200
|
|
|
201 現在の Gears OSのcodeGearは、interfaceを含む記述を .cbc に書き、それを CbC に変換している。
|
|
|
202 この時に、meta codeGear として stub そして、meta dataGearとして Context の定義が生成される。
|
|
|
203
|
|
|
204 Context の定義は Application 毎に異なっているが、全部をそろえることも可能である。この変換は
|
|
|
205 Perl script で記述されていて、煩雑になっている。これを codeGear / interface 単位で .o と
|
|
|
206 meta dataGearにできれば、全体の構成と、interfaceのコンパイルが簡単になると期待される。
|
|
|
207
|
|
|
208 ただし、この場合は、Context の中での引数領域のoffset管理、code tableの初期化、code間の
|
|
|
209 遷移を扱う codeGearの番号の指定の書き換えなどが必要となる。
|
|
|
210
|
|
2
|
211 --static linkage
|
|
|
212
|
|
|
213 コンパイル時に codeGearの結合が明らかならば、それは一つのcodeGearとしてまとめてよい。Contextへの書き込みもさぼることが
|
|
|
214 可能になる。ただし、時分割実行される場合は、codeGearの切れ目で分割するのと同じ実行が要求される。
|
|
|
215 つまり、割り込み処理などで途中で実行が中断するならば、それはその単位まで実行してから、Contextを切り替える必要がある。
|
|
0
|
216
|
|
2
|
217 これを実現する手法はflagを参照する方法や、コードを書き換える方法あるいは、polingを埋め込むなどの方法が考えられる。
|
|
|
218 整合性が不要であれば途中で止めても問題ないが、その場合は register などの状態を従来のOSのように保持する必要がある。
|
|
|
219
|
|
|
220 codeGear単位で正直に分割コンパイルすると最適化の余地がない。しかし、その場合でもJITなどは可能である。
|
|
|
221
|
|
|
222 --boot codeGear
|
|
|
223
|
|
|
224 今の実装では、UEFIから Gears OSが読み出される。Gears OS自体は、x.v6\cite{}と同じで、ファイルシステムを
|
|
|
225 含む一体の binary になっている。
|
|
|
226
|
|
|
227 codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。
|
|
0
|
228
|
|
4
|
229
|
|
0
|
230 --まとめ
|
|
4
|
231
|
|
|
232 Gears OS と GearsAgda における codeGear の管理方法について考察した。将来的には GearsAgda で記述された
|
|
|
233 証明付きinterfaceのコードを CbC に変換し、それを Gears OSで正しさを確認しながら組み合わせて、meta計算の
|
|
|
234 変更を可能にしながら実行するシステムを作りたい。
|
|
|
235
|
|
|
236
|
|
|
237
|
|
|
238
|
|
|
239
|
