|
0
|
1 -title: Gears OSの CodeGear Management
|
|
|
2
|
|
6
|
3 -author: 仲吉菜々子 and 河野真治
|
|
|
4
|
|
|
5 --abstract:
|
|
|
6
|
|
|
7 GearsOSではすべてのプログラムはKernelやdriverを含めて CodeGear
|
|
|
8 で書かれている。これらは、CodeGear のSystem DBに格納される
|
|
|
9 べきである。Microwre OS9でもmoduleという形でメモリに展開さ
|
|
|
10 れていた。CodeGearの集合で一つのアプリやサービスが作られる。
|
|
|
11 このCodeGearnの組み合わせを指定する仕組みが必要である。また、
|
|
|
12 CodeGear を実行時にloadする機構を作ることにより、現在、clnag
|
|
|
13 のlinkerで行っている作業抜きでGearsOSを構成できる。これによ
|
|
|
14 り、GearsOSのbuildを簡単にすることができる。高速化が必要な
|
|
|
15 場合は、複数のCodeGearをまとめて最適化して、一つのCodeGearn
|
|
|
16 にする。しかし、実行時のメタ計算がが必要な場合は、それよう
|
|
|
17 のhookを用意する必要がある。これの仕組みについて考察する。
|
|
|
18
|
|
|
19 --abstract-e:
|
|
|
20
|
|
|
21 In GearsOS, all programs, including kernels and drivers, are
|
|
|
22 written in CodeGear. These should be stored in the System DB
|
|
|
23 of CodeGear. In Microwre OS9, they were deployed in memory
|
|
|
24 as modules. An application or service is created using a set
|
|
|
25 of CodeGear. A mechanism is needed to specify the combination
|
|
|
26 of CodeGear. Additionally, by creating a mechanism to load
|
|
|
27 CodeGear at runtime, GearsOS can be built without the work
|
|
|
28 currently done by the clnag linker. This simplifies the process
|
|
|
29 of building GearsOS. When optimization is necessary, multiple
|
|
|
30 CodeGear can be combined and optimized to create a single CodeGear.
|
|
|
31 However, if runtime metacalculation is necessary, a hook must
|
|
|
32 be provided for it.
|
|
0
|
33
|
|
1
|
34 --Gears OSによる信頼できるサービス
|
|
|
35
|
|
|
36 サービスやアプリケーションの信頼性は、OSとユーザプログラムのように分離することはできない。
|
|
|
37 プログラムの正しさは基本的にはコードの正しさであり、今のOSのようにコードの管理をユーザ空間の
|
|
|
38 問題として放り出す方法には限界がある。
|
|
|
39
|
|
|
40 Gears OSでは実行単位として codeGear、データ単位として dataGear を使う。さらに、これらは
|
|
|
41 Monad のようにメタ codeGeearやメタdataGearを持っている。
|
|
|
42
|
|
6
|
43 Gears OSでの検証は、Agda\cite{Agda,AgdaWiki}を使った GearsAgdaを用いる。これらの実行と並列実行は、
|
|
1
|
44 GearsAgdaに対して定義される。当然、すべてのGearsAgdaのcodeGearは、Gears OSに
|
|
|
45 登録されることになる。
|
|
|
46
|
|
6
|
47 OSでの証明よる検証はいろいろ行なわれているが、Haskellに近い形式に変換することが多い
|
|
|
48 \cite{Klein:2014:CFV:2584468.2560537,Chen:2015:UCH:2815400.2815402,Yang:2010:SLI:1806596.1806610}。
|
|
|
49 Gears OSでは、GearsAgda で直接に記述できる点が新しい。
|
|
|
50
|
|
1
|
51 この論文では、Gears OSのcodeGearの管理方法について考察する。
|
|
0
|
52
|
|
|
53 --Normal and Meta computation
|
|
|
54
|
|
6
|
55 Gears OSの基本は、CbC (Continuation based C)\cite{cbc-github}であり、input interfaceとoutput interfaceを有限な処理で
|
|
1
|
56 結ぶものになっている。これは、コンパイラの基本ブロックに大体相当する。これはさらに、GearsAgdaの
|
|
|
57 Agdaで記述された invariant あるいは、表示的意味論と直結している。
|
|
|
58
|
|
|
59 CbCの記述は以下のようなものである。
|
|
|
60
|
|
|
61 __code startTimer(struct TimerImpl* timer, __code next(...)) {
|
|
|
62 struct timeval tv;
|
|
|
63 gettimeofday(&tv, NULL);
|
|
|
64 timer->time = tv.tv_sec + (double)tv.tv_usec*1e-6;
|
|
|
65 goto next(...);
|
|
|
66 }
|
|
|
67
|
|
|
68 nextが軽量継続を表している。このcodeGearの実行は論理的に割り込まれない。つまり、並行実行は
|
|
|
69 この単位で行われ定義される。ハードウェアでの並行実行、割り込み処理などは、それにそって
|
|
|
70 実装される必要がある。これらは、GearsAgdaでは、外部環境へのアクセスがある。この場合は
|
|
|
71 時刻に対するアクセスである。
|
|
|
72
|
|
|
73 OS側からみると、これは詳細のない単なるコードに見える。実行の詳細、つまり、実行に関係する
|
|
6
|
74 すべての dataGear 、すべてのcodeGearは、プロセスに相当する Context metaDataGear(図\ref{Gears OS})に格納される。
|
|
1
|
75
|
|
|
76 つまり、OSからみた codeGearの実行は、
|
|
|
77
|
|
6
|
78 meta codeGearの番号から、codeGearを選ぶ
|
|
1
|
79 それを実行し、continuation としてshcedulerを指定する
|
|
|
80 これを CPU worker 毎に実行する
|
|
|
81
|
|
|
82 ということになる。CPU worker毎に Contextは一つなので、Contextはsingle threadで実行される。
|
|
|
83 これにより、並行実行の単位はcodeGearとなる。
|
|
|
84 ただし、Context関の共有データがある場合は意味的なずれがでる場合がある。それは、
|
|
|
85 Contextの実行をそうなるように実装することになる。
|
|
|
86
|
|
|
87 その実装の正しさは、実装を GearsAgdaで記述することより可能になるが、その実装が物理的に一致するかどうかの
|
|
|
88 保証はハードウェアの性質に依存する。
|
|
|
89
|
|
|
90 外界との対応もメタ計算になるが、それはGearsAgdaによるシミュレーションに対する正しさということになる。
|
|
|
91
|
|
|
92 scheduler から codeGearへの移行は、以下のmeta codeGear で実装される。
|
|
|
93
|
|
|
94 __code meta(struct Context* context, enum Code next) {
|
|
|
95 goto (context->code[next])(context);
|
|
|
96 }
|
|
|
97
|
|
|
98
|
|
|
99 \verb+context->code[next]+が codeGearのtableの呼び出しになるが、
|
|
|
100 これは表がコンパイル時に確定し、直接の呼び出しでは、コンパイラが最適化するので、overhead とはならない。
|
|
|
101 meta が書き換えられている場合は、ここで Context switchが起きることになる。
|
|
|
102
|
|
|
103 このContext switchでメモリ空間の切り替えが必要かどうかは application に依存する。
|
|
|
104 もし、codeGearの実行の正しさが証明されているなら、メモリ空間を切り替える必然性はない。
|
|
|
105 実際、Kernel 内や Realtime Monitor では切り替えない方が普通である。
|
|
|
106
|
|
6
|
107 <center><img src="fig/gears_structure.pdf" alt="Gears OS"></center>
|
|
|
108
|
|
1
|
109 --証明付きのコード
|
|
|
110
|
|
|
111 GearsAgdaで記述されていれば、codeGearやdataGearは証明を持つ。これらは単なる型なので実行時には
|
|
|
112 実態を持たない。ただし、それを実行時にチェックすることもできる。assertなどと同じ扱いである。
|
|
|
113
|
|
|
114 GearsAgdaの証明に閉じていれば、その範囲内での信頼性がある。しかし、動的にcodeが読み込まれる場合は
|
|
|
115 そうはならない。その時には、証明しなおす、簡易あるいは詳細なモデル検査を実施するなどが可能だが、
|
|
|
116 それらが実用的とは限らない。
|
|
|
117
|
|
|
118 codeはContextの表に登録されるが、システム全体のcodeは Database で管理される。その管理は
|
|
|
119 ファイルシステム上でも良い。codeは証明が付属している場合もあるが、それは何らかの形で
|
|
|
120 codeGear Databseに格納される。
|
|
|
121
|
|
2
|
122 現状では、証明はAgdaで記述されたデータ構造でしかない。それをcodeGear DBに入れても利用する方法は
|
|
|
123 ないがいくつかの利用法は考えられる。
|
|
1
|
124
|
|
2
|
125 証明とcodeGearの一致を確認する
|
|
|
126 型整合に使う
|
|
|
127 codeの認証に使う
|
|
1
|
128
|
|
2
|
129 この大域のcodeGear DBは、kernelを含めたすべてのcodeGearに対するもので全部で共有される。つまり、
|
|
|
130 あらゆるversionを含む共有ライブラリとなる。これは全世界でuniqueなDBとしても良い。
|
|
|
131
|
|
4
|
132 --CbCのcodeGear と GearsAgdaの違い
|
|
|
133
|
|
|
134 CbCのcodeGearとdataGearは、普通のCの関数と構造体であり、その意味で不思議なところはない。しかし、
|
|
|
135 normal levelではpointerが出てこないのが望ましい。なぜなら、メモリ配置は meta levelの問題で
|
|
|
136 プログラムの正しさとは直接関係しないからである。つまり、normal levelでの構造体は List や 木
|
|
|
137 など以外の再帰的構造でも直接的なポインタ操作は行わない。meta levelでは、メモリの直接操作
|
|
|
138 例えば mallocやfree、あるいは共有データの扱いなどをポインタを通して行う。
|
|
|
139
|
|
|
140 meta levelでのポインタ操作は、データ構造に対する操作であり、そのlevelに閉じる限り、
|
|
|
141 プログラムの正しさはポインタの実装に依存しない。その意味で、meta codeGear も単なる
|
|
|
142 noraml level のcodeGear に過ぎない。meta codeGearの証明あるいは、実装をさらにmeta level
|
|
|
143 で行うこともできる。
|
|
|
144
|
|
|
145 GearsAgda では、すべてはAgdaの構造体で表現される。これらは変数と項であり、基本的に複製可能
|
|
|
146 な項である。その意味で、ポインタを持たないと言ってよい。Listや木の実装を配列と番号で行う
|
|
|
147 ことはまったく実用的ではないので、普通に再帰的なデータ構造を使ってよい。ただし、それを
|
|
|
148 自分自身の codeGear の再帰呼び出しで行うと、codeGearの実行が有界な時間に閉じなくなる。
|
|
|
149 なので、loop は軽量継続を用いて、一旦、外にでることになる。これは、この段階でmeta level的に処理が
|
|
|
150 割り込まれることも意味している。
|
|
|
151
|
|
|
152 GearsAgda で処理された項は、ContextのdataGearに格納される。また、GearsAgdaのcodeGearは、
|
|
6
|
153 Contextのcode table(図\ref{code table})に格納される。どちらも、メモリ的には番号で管理されることになる。
|
|
4
|
154 GearsAgda の Context は、その意味で、プロセスのメモリ空間そのものを抽象化したものになっている。
|
|
|
155
|
|
|
156
|
|
|
157 つまり、CbCのcodeGearと GearsAgdaは、normal level ではポインタを使わないのだが、
|
|
|
158 その意味は、CbCと GearsAgda で若干異なる。CbCでの実装は、GearsAgdaでの実装の持つ
|
|
|
159 性質を保存する必要がある。
|
|
|
160
|
|
6
|
161 <center><img src="fig/codetable.pdf" alt="code table"></center>
|
|
|
162
|
|
4
|
163 --Contextを通した dataGearとcodeGearの連携
|
|
|
164
|
|
|
165 Gears OSでは、Context はCの構造体であり、一つのContextで使用するdataGearとcodeGearは、そこに格納される。
|
|
|
166 複数のContextから、dataGearもcodeGearも共有されることがある。その排他制御は、Gears OSのmeta codeGearに
|
|
|
167 よって行われる。
|
|
|
168
|
|
|
169 Gears OSは、interfaceという構造体でオブジェクト表現していて、これらには、メソッドを格納する配列がある。
|
|
|
170 この配列の添字を他のinterfaceが使用する。なので、interface間の呼び出しは、interfaceを表すdataGearと
|
|
|
171 そのメソッドの番号で決定される。
|
|
|
172
|
|
|
173 引数は、interface毎に Contextに決まった場所が確保される。これは、通常ではstack上に場所を確保する。
|
|
|
174 しかし、CbCでは関数呼び出しはstackを使わないので、このようにする必要がある。これは、もちろん、
|
|
|
175 マルチスレッドな実行では破壊されるおそれがあるが、Contextはシングルスレッドで実行することになっている
|
|
|
176 ので問題ない。
|
|
|
177
|
|
|
178 Contextの切り替えは、codeGearの境目で行われるので、Contextと実行しているcodeGearのcode tableの番号で
|
|
|
179 状態が決定する。つまり、Gears OSでは、Task Switchにはレジスタは関係しない。割り込みなどは、codeGearの
|
|
|
180 境界と独立に起きるが、それをmeta codeGearが境界で Context switchが起きたのと同じようにすることを
|
|
|
181 保証する。これは一種の遅延処理となる。もちろん、影響がないなら、割り込み中にmetaな処理を行ってもよい。
|
|
|
182 これは、本来はCPUなどのハードウェアでサポートされるべきかもしれない。
|
|
|
183
|
|
|
184 dataGearは、metaな情報として、dataGearの構造定義を番号として持っている。これを使うことにより
|
|
|
185 任意のdataGearの表示を正しく行うことができる。この情報を取り扱うことは meta level からでしか
|
|
|
186 許されないが、CbC的には特に制限はない。
|
|
|
187
|
|
|
188 引数として呼び出される dataGearは、Context上に前もって確保されているが、実行時にallocateされる
|
|
|
189 dataGearもContextから参照される pool に確保される。これの管理は meta dataGear (Gears OSのkernel)
|
|
|
190 が行う。GearsAgda は、この部分はAgdaが管理するので meta的な管理は行われない。しかし、
|
|
|
191 Context を用いた並行実行の場合は、Context上での管理の問題が生じる。
|
|
|
192
|
|
|
193
|
|
6
|
194 --code table
|
|
|
195
|
|
|
196 contextの初期化の中で、code table に実際の codeGear stub へのポインタが初期化される。
|
|
|
197
|
|
|
198 context->code[C_add] = add_stub;
|
|
|
199 context->code[C_checkAndSetAtomicReference]
|
|
|
200 = checkAndSetAtomicReference_stub;
|
|
|
201 context->code[C_clearSingleLinkedQueue] = clearSingleLinkedQueue_stub;
|
|
|
202 context->code[C_clearSynchronizedQueue] = clearSynchronizedQueue_stub;
|
|
|
203 context->code[C_code1] = code1_stub;
|
|
|
204 context->code[C_createTask1] = createTask1_stub;
|
|
|
205 context->code[C_createTask2] = createTask2_stub;
|
|
|
206 context->code[C_decrementTaskCountTaskManagerImpl]
|
|
|
207 = decrementTaskCountTaskManagerImpl_stub;
|
|
|
208 context->code[C_exit_code] = exit_code_stub;
|
|
|
209 context->code[C_getTaskCPUWorker] = getTaskCPUWorker_stub;
|
|
|
210 context->code[C_incrementTaskCountTaskManagerImpl]
|
|
|
211 = incrementTaskCountTaskManagerImpl_stub;
|
|
|
212
|
|
|
213 interfaceの初期化の中で、この番号が interfaceを表す dataGearに格納される。
|
|
|
214
|
|
|
215 Tree* createRedBlackTree(struct Context* context) {
|
|
|
216 struct Tree* tree = &ALLOCATE(context, Tree)->Tree;
|
|
|
217 struct RedBlackTree* redBlackTree
|
|
|
218 = &ALLOCATE(context, RedBlackTree)->RedBlackTree;
|
|
|
219 tree->tree = (union Data*)redBlackTree;
|
|
|
220 redBlackTree->root = NULL;
|
|
|
221 redBlackTree->nodeStack = createSingleLinkedStack(context);
|
|
|
222 tree->put = C_putRedBlackTree;
|
|
|
223 tree->get = C_getRedBlackTree;
|
|
|
224 tree->remove = C_removeRedBlackTree;
|
|
|
225 return tree;
|
|
|
226 }
|
|
|
227
|
|
|
228 この辺の構造は、GearsAgda 側では簡素化されている。実際、pointer を直接操作しないとかも、厳密に守る必要はなく、
|
|
|
229 GearsAgda と CbC での実装が平行していれば問題はない。
|
|
|
230
|
|
2
|
231 --codeGearのlinkage
|
|
1
|
232
|
|
2
|
233 Gears OSのあらゆるコードは、codeGear DBのコードの組み合わせになる。しかし、そのためには、
|
|
|
234 Contextから詳細なデータを取り出して、実行し、次のcodeGearを呼び出す時にContextの正しい場所にdataGearを格納する
|
|
|
235 必要がある。これは codeGear 全体に対して必要になる。
|
|
1
|
236
|
|
2
|
237 現状では、これは stubとしてコンパイル時に生成される。
|
|
1
|
238
|
|
6
|
239 __code checkAndSetAtomicReference(struct AtomicReference* atomic,
|
|
|
240 union Data** ptr, union Data* oldData, union Data* newData, __code next(...),
|
|
|
241 __code fail(...)) {
|
|
2
|
242 if (__sync_bool_compare_and_swap(ptr, oldData, newData)) {
|
|
|
243 goto next(...);
|
|
|
244 }
|
|
|
245 goto fail(...);
|
|
|
246 }
|
|
|
247
|
|
|
248 では、Context 上には以下の構造と、それを呼び出す stub がある。
|
|
0
|
249
|
|
2
|
250 struct Atomic {
|
|
|
251 union Data* atomic;
|
|
|
252 union Data** ptr;
|
|
|
253 union Data* oldData;
|
|
|
254 union Data* newData;
|
|
|
255 enum Code checkAndSet;
|
|
|
256 enum Code next;
|
|
|
257 enum Code fail;
|
|
|
258 } Atomic;
|
|
0
|
259
|
|
2
|
260 __code checkAndSetAtomicReference_stub(struct Context* context) {
|
|
6
|
261 AtomicReference* atomic = (AtomicReference*)
|
|
|
262 GearImpl(context, Atomic, atomic);
|
|
2
|
263 Data** ptr = Gearef(context, Atomic)->ptr;
|
|
|
264 Data* oldData = Gearef(context, Atomic)->oldData;
|
|
|
265 Data* newData = Gearef(context, Atomic)->newData;
|
|
|
266 enum Code next = Gearef(context, Atomic)->next;
|
|
|
267 enum Code fail = Gearef(context, Atomic)->fail;
|
|
6
|
268 goto checkAndSetAtomicReference(context, atomic,
|
|
|
269 ptr, oldData, newData, next, fail);
|
|
2
|
270 }
|
|
0
|
271
|
|
2
|
272 これらは単一のGears OS内で整合する必要がある。実際には、これらは、stubが参照する Context内のoffsetにすぎない。
|
|
|
273 Atomic は dataGear の巨大な Union になっている。これは、GearsAgda でも状況は同じで、巨大な Sum type になっている。
|
|
|
274
|
|
|
275 このContext内での offsetと呼び出すcodeGearの番号が一致すれば、Kernel側で整合性の問題はない。
|
|
|
276
|
|
4
|
277 --codeGearのコンパイル方法
|
|
|
278
|
|
|
279 現在の Gears OSのcodeGearは、interfaceを含む記述を .cbc に書き、それを CbC に変換している。
|
|
|
280 この時に、meta codeGear として stub そして、meta dataGearとして Context の定義が生成される。
|
|
|
281
|
|
|
282 Context の定義は Application 毎に異なっているが、全部をそろえることも可能である。この変換は
|
|
|
283 Perl script で記述されていて、煩雑になっている。これを codeGear / interface 単位で .o と
|
|
|
284 meta dataGearにできれば、全体の構成と、interfaceのコンパイルが簡単になると期待される。
|
|
|
285
|
|
|
286 ただし、この場合は、Context の中での引数領域のoffset管理、code tableの初期化、code間の
|
|
|
287 遷移を扱う codeGearの番号の指定の書き換えなどが必要となる。
|
|
|
288
|
|
2
|
289 --static linkage
|
|
|
290
|
|
|
291 コンパイル時に codeGearの結合が明らかならば、それは一つのcodeGearとしてまとめてよい。Contextへの書き込みもさぼることが
|
|
|
292 可能になる。ただし、時分割実行される場合は、codeGearの切れ目で分割するのと同じ実行が要求される。
|
|
|
293 つまり、割り込み処理などで途中で実行が中断するならば、それはその単位まで実行してから、Contextを切り替える必要がある。
|
|
0
|
294
|
|
2
|
295 これを実現する手法はflagを参照する方法や、コードを書き換える方法あるいは、polingを埋め込むなどの方法が考えられる。
|
|
|
296 整合性が不要であれば途中で止めても問題ないが、その場合は register などの状態を従来のOSのように保持する必要がある。
|
|
|
297
|
|
|
298 codeGear単位で正直に分割コンパイルすると最適化の余地がない。しかし、その場合でもJITなどは可能である。
|
|
|
299
|
|
|
300 --boot codeGear
|
|
|
301
|
|
6
|
302 今の実装では、UEFIから Gears OSが読み出される。Gears OS自体は、x.v6\cite{xv6rpi}と同じで、ファイルシステムを
|
|
2
|
303 含む一体の binary になっている。
|
|
|
304
|
|
|
305 codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。
|
|
0
|
306
|
|
4
|
307
|
|
0
|
308 --まとめ
|
|
4
|
309
|
|
|
310 Gears OS と GearsAgda における codeGear の管理方法について考察した。将来的には GearsAgda で記述された
|
|
|
311 証明付きinterfaceのコードを CbC に変換し、それを Gears OSで正しさを確認しながら組み合わせて、meta計算の
|
|
|
312 変更を可能にしながら実行するシステムを作りたい。
|
|
|
313
|
|
|
314
|
|
|
315
|
|
|
316
|
|
|
317
|
