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