|
18
|
1 # CbCインターフェースによる CbCXv6 の書き換え
|
|
|
2 - 並列信頼研
|
|
|
3 - 桃原 優
|
|
|
4
|
|
|
5 ---
|
|
|
6
|
|
21
|
7 # 概要
|
|
23
|
8 - OS の信頼性を上げたい
|
|
|
9 - CbCを使って xv6 を書き換える
|
|
|
10 - Paging の書き換えを行った
|
|
|
11 - まだ実装中
|
|
|
12 - 将来はコンテナやVMをメタ計算として実装できるはず
|
|
18
|
13
|
|
|
14 ---
|
|
|
15
|
|
23
|
16 # OS の信頼性を上げたい
|
|
|
17 - 仕様を満たすことを証明する
|
|
|
18 - 証明しやすい形の記述を作る
|
|
|
19 - CbCの goto で書く
|
|
|
20 - 状態遷移系に近い形で記述できる
|
|
|
21 - 関数型の記述
|
|
|
22 - CbCのinterface で書く
|
|
|
23 - 記述のモジュール化
|
|
18
|
24
|
|
|
25 ---
|
|
|
26
|
|
|
27 # メタレベルとノーマルレベル
|
|
|
28 - ノーマルレベル
|
|
23
|
29 - CbCで記述される普通のアルゴリズム
|
|
18
|
30 - メタレベル
|
|
23
|
31 - Paging などのメモリやCPU自体の操作
|
|
|
32 - プログラムの正しさの証明
|
|
|
33 - Context
|
|
|
34 - メタレベルで使用される Meta Data を置く場所
|
|
18
|
35
|
|
|
36 ---
|
|
|
37
|
|
|
38 # Continuation based C
|
|
|
39 - ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC)
|
|
|
40 - Code Gear
|
|
|
41 - 基本的な処理の単位
|
|
23
|
42 - goto 文で遷移する
|
|
18
|
43 - Data Gear
|
|
|
44 - データの単位
|
|
23
|
45 - Meta Code Gear
|
|
|
46 - goto meta
|
|
|
47 - Code Gear の間に挟める計算
|
|
|
48 - Meta Data Gear
|
|
|
49 - Context
|
|
|
50 - Code Gearの間の接続など
|
|
18
|
51
|
|
|
52 ---
|
|
|
53
|
|
|
54 # goto による継続
|
|
|
55
|
|
|
56 - Code Gear の処理の間を goto によって遷移していく
|
|
|
57
|
|
|
58 
|
|
|
59
|
|
19
|
60
|
|
18
|
61 ---
|
|
|
62
|
|
|
63 # Data Gear の継続
|
|
|
64 - goto の際に Data Gear も継続される
|
|
|
65
|
|
|
66 
|
|
|
67
|
|
|
68 ---
|
|
|
69
|
|
|
70 # インターフェース
|
|
|
71 - 書き換えを防ぐために見える Data Gear に違いが生じる
|
|
|
72 - -> Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入
|
|
21
|
73 - インターフェースによる他のメリット
|
|
18
|
74 - 煩雑な記述の解消
|
|
|
75 - 機能の入れ替え
|
|
|
76 - Agda による証明
|
|
|
77
|
|
|
78 ---
|
|
|
79
|
|
23
|
80
|
|
|
81 # Meta Code Gear
|
|
|
82 - 実際にはノーマルレベルの間にメタレベルの処理がある
|
|
|
83 - Meta Level では Data Gear の見え方は変わる(Meta Data Gear)
|
|
|
84 - 書き換えやアクセスを防ぐため
|
|
|
85
|
|
|
86 
|
|
18
|
87
|
|
|
88 ---
|
|
|
89
|
|
23
|
90 # Geas OS
|
|
|
91 - Xv6 をCbCで書き換える
|
|
18
|
92 - MIT の講義用教材として作られたOS
|
|
|
93 - 企画課される前のCで書かれたUNIX V6 を書き換えた
|
|
|
94 - 1万行程の軽量なOS
|
|
|
95 - Linuxだと数千万行
|
|
|
96 - Xv6 を参考に CbC で書き直すことで Gears OS を実装する
|
|
|
97
|
|
|
98 ---
|
|
|
99
|
|
23
|
100
|
|
|
101 # Xv6の構成
|
|
|
102 - systemcall
|
|
|
103 - Scheduler
|
|
|
104 - VM
|
|
|
105 - file system
|
|
|
106 - tty
|
|
|
107
|
|
|
108
|
|
|
109 ---
|
|
|
110
|
|
|
111 # Context
|
|
|
112 - Meta Data Gear
|
|
|
113 - ユーザープロセスに対応して1つのcontextがある
|
|
|
114 - Contextには実行されるすべてのCode Gear が登録される
|
|
|
115 - Data GearもContext上にある
|
|
|
116
|
|
|
117 ---
|
|
18
|
118 # カーネル空間
|
|
|
119 - OS の中核となるプログラムで Meta Level に相当する
|
|
|
120 - Xv6 ではカーネルとユーザープログラムは分離されている
|
|
|
121 - ユーザープログラムはカーネルに直接アクセスできない。
|
|
|
122 - 書き換えやアクセスを防ぐため
|
|
|
123 - 呼び出す場合は system call
|
|
|
124
|
|
|
125 ---
|
|
|
126
|
|
|
127 # system call
|
|
|
128 - system call 呼び出し
|
|
|
129 - トラップ の発生
|
|
|
130 - ユーザープログラムの中断
|
|
|
131 - 処理がカーネルに切り替わる
|
|
|
132
|
|
|
133 # CbCXv6 での Paging
|
|
23
|
134 - OS の信頼性の1つであるメモリ管理部分
|
|
|
135 - メモリ管理するpage table
|
|
18
|
136 - Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理
|
|
|
137 - 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる
|
|
|
138
|
|
|
139 ---
|
|
|
140
|
|
|
141 # Pagingの図
|
|
|
142 - 必要？
|
|
21
|
143 
|
|
|
144
|
|
18
|
145
|
|
|
146 ---
|
|
19
|
147 # CbC インターフェース
|
|
|
148 - インターフェースは Data Gear に対しての操作を行う Code Gear
|
|
|
149 - 実装は別で定義し、呼び出す
|
|
|
150 - インターフェースによって機能を置き換えることができる
|
|
|
151
|
|
|
152 ---
|
|
|
153
|
|
|
154 # インターフェースの定義
|
|
|
155 - Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する **Meta Data Gear**
|
|
|
156
|
|
|
157 ---
|
|
|
158
|
|
|
159 # インターフェースのソースコード
|
|
|
160 - vm.c をインターフェースで書き換えた vm.h のコードの説明をしていく
|
|
|
161
|
|
|
162
|
|
|
163 ---
|
|
|
164
|
|
|
165
|
|
|
166 # 実装名の定義
|
|
|
167 - typedef struct の直後に実装名(vm)を書く
|
|
|
168
|
|
|
169
|
|
|
170 ``` c
|
|
|
171 typedef struct vm<Type,Impl> {
|
|
|
172 ```
|
|
|
173
|
|
|
174 ---
|
|
|
175
|
|
23
|
176 # init_vmm
|
|
|
177
|
|
|
178
|
|
19
|
179 # Code Gear の定義
|
|
|
180 - Code Gear は __Code CodeGear名(引数); で記述する
|
|
|
181 - 第1引数の Impl* vm が Code Gear の型になる
|
|
|
182 - 初期化された Data Gear が それぞれの Code Gear の引数として扱われる
|
|
|
183 - 例)定義された uinit が kpt_freerange の Code Gear の第1引数と対応している
|
|
|
184
|
|
|
185
|
|
|
186 ``` c
|
|
21
|
187 typedef struct vm<Type,Impl> {
|
|
19
|
188 __code init_vmm(Impl* vm, __code next(...));
|
|
|
189 __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...));
|
|
|
190 __code kpt_alloc(Impl* vm ,__code next(...));
|
|
|
191 __code switchuvm(Impl* vm ,struct proc* p, __code next(...));
|
|
|
192 __code init_inituvm(Impl* vm, pde_t* pgdir, char* init, uint sz, __code next(...));
|
|
|
193 __code loaduvm(Impl* vm,pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz, __code next(...));
|
|
|
194 __code allocuvm(Impl* vm, pde_t* pgdir, uint oldsz, uint newsz, __code next(...));
|
|
|
195
|
|
|
196 ```
|
|
|
197
|
|
|
198 ---
|
|
|
199
|
|
|
200
|
|
|
201 # next(...)
|
|
|
202 - __code next(...) は条件分岐によって複数の継続先が設定される
|
|
|
203 - それぞれの Code Gear の引数の1つに設定する
|
|
|
204 ``` c
|
|
|
205 __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...));
|
|
|
206 ....
|
|
|
207 __code next(...);
|
|
|
208 } vm;
|
|
|
209 ```
|
|
|
210
|
|
|
211 ---
|
|
|
212
|
|
|
213 # インターフェースの実装
|
|
|
214 - インターフェースの実装は別ファイルで定義する(vm_impl.cbc)
|
|
|
215 - ヘッダーファイルの呼び出しは #include ではなく #interface で呼び出す
|
|
|
216
|
|
|
217 ``` c
|
|
|
218 #include "../../context.h"
|
|
|
219 #interface "vm.h"
|
|
|
220
|
|
|
221 ```
|
|
|
222
|
|
|
223
|
|
|
224 ---
|
|
|
225
|
|
|
226 # create_impl
|
|
|
227 - create_imple の関数内で vm の型を定義し、vm->CodeGear名 で対応させていく
|
|
|
228 - 実装を Code Gear で記述していく。
|
|
|
229
|
|
|
230
|
|
|
231 ``` c
|
|
|
232
|
|
|
233 vm* createvm_impl(struct Context* cbc_context) {
|
|
|
234 struct vm* vm = new vm();
|
|
|
235 ....
|
|
|
236 vm->void_ret = C_vm_void_ret;
|
|
|
237 vm->init_vmm = C_init_vmmvm_impl;
|
|
|
238 vm->kpt_freerange = C_kpt_freerangevm_impl;
|
|
|
239 vm->kpt_alloc = C_kpt_allocvm_impl;
|
|
|
240 ...
|
|
|
241 __code init_vmmvm_impl(struct vm_impl* vm,__code next(...)) {
|
|
|
242 initlock(&kpt_mem.lock, "vm");
|
|
|
243 kpt_mem.freelist = NULL;
|
|
|
244
|
|
|
245 goto next(...);
|
|
|
246 }
|
|
|
247 ```
|
|
|
248
|
|
|
249 ---
|
|
|
250
|
|
|
251 # private
|
|
|
252 - CbC は信頼性を保証するためにそれぞれの Code Gear を細かくする必要があるので、for文やif文がある場合はさらに実装を分ける
|
|
|
253 - Code Gear は基本的にインターフェースで指定された Code Gear 内からのみ継続さ れるため、Java の private メソッドのように扱われる。
|
|
|
254 - 実際に vm.c の loaduvm の実装を分けた記述を説明する
|
|
|
255
|
|
|
256
|
|
|
257 ``` c
|
|
|
258 int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz)
|
|
|
259 {
|
|
|
260 uint i, pa, n;
|
|
|
261 pte_t *pte;
|
|
|
262
|
|
|
263 if ((uint) addr % PTE_SZ != 0) {
|
|
|
264 panic("loaduvm: addr must be page aligned");
|
|
|
265 }
|
|
|
266
|
|
|
267 for (i = 0; i < sz; i += PTE_SZ) {
|
|
|
268 if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) {
|
|
|
269 panic("loaduvm: address should exist");
|
|
|
270 }
|
|
|
271
|
|
|
272 pa = PTE_ADDR(*pte);
|
|
|
273
|
|
|
274 if (sz - i < PTE_SZ) {
|
|
|
275 n = sz - i;
|
|
|
276 } else {
|
|
|
277 n = PTE_SZ;
|
|
|
278 }
|
|
|
279
|
|
|
280 if (readi(ip, p2v(pa), offset + i, n) != n) {
|
|
|
281 return -1;
|
|
|
282 }
|
|
|
283 }
|
|
|
284
|
|
|
285 return 0;
|
|
|
286 }
|
|
|
287 ```
|
|
|
288
|
|
|
289 ---
|
|
|
290
|
|
|
291 # goto private
|
|
|
292 - vm と同じ create_impl 内で vm_impl を定義し、private で実装する Code Gear を定義する
|
|
|
293 - loaduvmvm_impl で goto によって private に遷移する
|
|
|
294
|
|
|
295
|
|
|
296 ``` c
|
|
|
297 vm* createvm_impl(struct Context* cbc_context) {
|
|
|
298 ...
|
|
|
299 struct vm_impl* vm_impl = new vm_impl();
|
|
|
300 ...
|
|
|
301 vm_impl->loaduvm_ptesize_check = C_loaduvm_ptesize_checkvm_impl;
|
|
|
302 ....
|
|
|
303 vm->loaduvm = C_loaduvmvm_impl;
|
|
|
304 ....
|
|
|
305 }
|
|
|
306
|
|
|
307 __code loaduvmvm_impl(struct vm_impl* vm, pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz, __code next(...)) {
|
|
|
308 Gearef(cbc_context, vm_impl)->pgdir = pgdir;
|
|
|
309 Gearef(cbc_context, vm_impl)->addr = addr;
|
|
|
310 Gearef(cbc_context, vm_impl)->ip = ip;
|
|
|
311 Gearef(cbc_context, vm_impl)->offset = offset;
|
|
|
312 Gearef(cbc_context, vm_impl)->sz = sz;
|
|
|
313 Gearef(cbc_context, vm_impl)->next = next;
|
|
|
314
|
|
|
315 goto loaduvm_ptesize_checkvm_impl(vm, next(...));
|
|
|
316 }
|
|
|
317 ```
|
|
|
318 ---
|
|
|
319
|
|
|
320 # private のヘッダー
|
|
|
321 - private 側のヘッダーファイルも vm_impl と同じように用意する
|
|
|
322
|
|
|
323 ``` c
|
|
|
324 typedef struct vm_impl<Impl, Isa> impl vm{
|
|
|
325 ...
|
|
|
326 __code loaduvm_ptesize_check(Type* vm_impl, uint i, pte_t* pte, uint sz,
|
|
|
327 __code next(int ret, ...));
|
|
|
328 ```
|
|
|
329
|
|
|
330 ---
|
|
|
331
|
|
|
332 # private の記述
|
|
|
333
|
|
|
334 ``` c
|
|
|
335 #interface "vm_impl.h"
|
|
|
336
|
|
|
337 __code loaduvm_ptesize_checkvm_impl(struct vm_impl* vm_impl, __code next(int ret, ...)) {
|
|
|
338 char* addr = vm_impl->addr;
|
|
|
339
|
|
|
340 if ((uint) addr %PTE_SZ != 0) {
|
|
|
341 // goto panic
|
|
|
342 }
|
|
|
343
|
|
|
344 goto loaduvm_loopvm_impl(vm_impl, next(ret, ...));
|
|
|
345 }
|
|
|
346 ```
|
|
|
347
|
|
|
348 - vm.cではここから for だが CbC は if文の中と外にgoto を用意して実装する
|
|
|
349
|
|
|
350 
|
|
|
351
|
|
|
352 ```c
|
|
|
353 __code loaduvm_loopvm_impl(struct vm_impl* vm_impl, __code next(int ret, ...)) {
|
|
|
354 uint i = vm_impl->i;
|
|
|
355 uint sz = vm_impl->sz;
|
|
|
356
|
|
|
357 if (i < sz) {
|
|
|
358 goto loaduvm_check_pgdir(vm_impl, next(ret, ...));
|
|
|
359 }
|
|
|
360
|
|
|
361 goto loaduvm_exit(vm_impl, next(ret, ...));
|
|
|
362 }
|
|
|
363
|
|
|
364
|
|
|
365 __code loaduvm_check_pgdir(struct vm_impl* vm_impl, __code next(int ret, ...)) {
|
|
|
366 pte_t* pte = vm_impl->pte;
|
|
|
367 pde_t* pgdir = vm_impl->pgdir;
|
|
|
368 uint i = vm_impl->i;
|
|
|
369 char* addr = vm_impl->addr;
|
|
|
370 uint pa = vm_impl->pa;
|
|
|
371
|
|
|
372 if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) {
|
|
|
373 // goto panic
|
|
|
374 }
|
|
|
375 pa = PTE_ADDR(*pte);
|
|
|
376
|
|
|
377 vm_impl->pte = pte;
|
|
|
378 vm_impl->pgdir = pgdir;
|
|
|
379 vm_impl->addr = addr;
|
|
|
380 vm_impl->pa = pa;
|
|
|
381
|
|
|
382 goto loaduvm_check_PTE_SZ(vm_impl, next(ret, ...));
|
|
|
383 }
|
|
|
384
|
|
|
385 __code loaduvm_check_PTE_SZ(struct vm_impl* vm_impl, __code next(int ret, ...)) {
|
|
|
386 uint sz = vm_impl->sz;
|
|
|
387 uint i = vm_impl->i;
|
|
|
388 uint n = vm_impl->n;
|
|
|
389 struct inode* ip = vm_impl->ip;
|
|
|
390 uint pa = vm_impl->pa;
|
|
|
391 uint offset = vm_impl->offset;
|
|
|
392
|
|
|
393 if (sz - i < PTE_SZ) {
|
|
|
394 n = sz - i;
|
|
|
395 } else {
|
|
|
396 n = PTE_SZ;
|
|
|
397 }
|
|
|
398
|
|
|
399 if (readi(ip, p2v(pa), offset + i, n) != n) {
|
|
|
400 ret = -1;
|
|
|
401 goto next(ret, ...);
|
|
|
402 }
|
|
|
403
|
|
|
404 vm_impl->n = n;
|
|
|
405
|
|
|
406 goto loaduvm_loopvm_impl(vm_impl, next(ret, ...));
|
|
|
407 }
|
|
|
408
|
|
|
409 __code loaduvm_exit(struct vm_impl* vm_impl, __code next(int ret, ...)) {
|
|
|
410 ret = 0;
|
|
|
411 goto next(ret, ...);
|
|
|
412 }
|
|
|
413 ```
|
|
18
|
414
|
|
|
415
|
|
|
416
|
|
19
|
417 ``` c
|
|
|
418
|
|
|
419 int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz)
|
|
|
420 {
|
|
|
421 uint i, pa, n;
|
|
|
422 pte_t *pte;
|
|
|
423
|
|
|
424 if ((uint) addr % PTE_SZ != 0) {
|
|
|
425 panic("loaduvm: addr must be page aligned");
|
|
|
426 }
|
|
|
427
|
|
|
428 for (i = 0; i < sz; i += PTE_SZ) {
|
|
|
429 if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) {
|
|
|
430 panic("loaduvm: address should exist");
|
|
|
431 }
|
|
|
432
|
|
|
433 pa = PTE_ADDR(*pte);
|
|
|
434
|
|
|
435 if (sz - i < PTE_SZ) {
|
|
|
436 n = sz - i;
|
|
|
437 } else {
|
|
|
438 n = PTE_SZ;
|
|
|
439 }
|
|
|
440
|
|
|
441 if (readi(ip, p2v(pa), offset + i, n) != n) {
|
|
|
442 return -1;
|
|
|
443 }
|
|
|
444 }
|
|
|
445
|
|
|
446 return 0;
|
|
|
447 }
|
|
|
448 ```
|
|
|
449
|
|
|
450
|
|
|
451 # インターフェースの呼び出し
|
|
|
452 - 定義したインターフェースの呼び出しについて説明する
|
|
|
453 - CbC の場合 goto による 遷移を行うので、関数呼び出しのように goto 以降のコードを実行できない
|
|
|
454 - 例) goto すると戻ってこれないため それ以降が実行されなくなる。
|
|
|
455
|
|
|
456 ``` c
|
|
|
457 void userinit(void)
|
|
|
458 {
|
|
|
459 struct proc* p;
|
|
|
460 extern char _binary_initcode_start[], _binary_initcode_size[];
|
|
|
461
|
|
|
462 p = allocproc();
|
|
|
463 initContext(&p->cbc_context);
|
|
|
464
|
|
|
465 initproc = p;
|
|
|
466
|
|
|
467 if((p->pgdir = kpt_alloc()) == NULL) {
|
|
|
468 panic("userinit: out of memory?");
|
|
|
469 }
|
|
|
470
|
|
|
471 goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
|
|
|
472 p->sz = PTE_SZ;
|
|
|
473
|
|
|
474 // craft the trapframe as if
|
|
|
475 memset(p->tf, 0, sizeof(*p->tf));
|
|
|
476 ~
|
|
|
477 ```
|
|
|
478
|
|
|
479 # 呼び出しの解決
|
|
|
480 - 最初の命令は next で戻ってこれるので、dummy の関数を用意してそこで実行する
|
|
|
481
|
|
|
482 ``` c
|
|
|
483 void dummy(struct proc *p, char _binary_initcode_start[], char _binary_initcode_size[])
|
|
|
484 {
|
|
|
485 // inituvm(p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
|
|
|
486 goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
|
|
|
487
|
|
|
488 }
|
|
|
489
|
|
|
490
|
|
|
491
|
|
|
492 __ncode cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz){//:skip
|
|
|
493
|
|
|
494 struct vm* vm = createvm_impl(cbc_context);
|
|
|
495 // goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret);
|
|
|
496 Gearef(cbc_context, vm)->vm = (union Data*) vm;
|
|
|
497 Gearef(cbc_context, vm)->pgdir = pgdir;
|
|
|
498 Gearef(cbc_context, vm)->init = init;
|
|
|
499 Gearef(cbc_context, vm)->sz = sz ;
|
|
|
500 Gearef(cbc_context, vm)->next = C_vm_void_ret ;
|
|
|
501 goto meta(cbc_context, vm->init_inituvm);
|
|
|
502 }
|
|
|
503
|
|
|
504
|
|
|
505 void userinit(void)
|
|
|
506 {
|
|
|
507 struct proc* p;
|
|
|
508 extern char _binary_initcode_start[], _binary_initcode_size[];
|
|
|
509
|
|
|
510 p = allocproc();
|
|
|
511 initContext(&p->cbc_context);
|
|
|
512
|
|
|
513 initproc = p;
|
|
|
514
|
|
|
515 if((p->pgdir = kpt_alloc()) == NULL) {
|
|
|
516 panic("userinit: out of memory?");
|
|
|
517 }
|
|
|
518
|
|
21
|
519 dummy(p, _binary_initcode_start, _binary_initcode_size);
|
|
|
520 ```
|
|
19
|
521
|
|
21
|
522
|
