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