Mercurial > hg > Papers > 2020 > tobaru-master
view slide/CbCXv6.md @ 48:eb651ae37444 default tip
fix spell
| author | tobaru |
|---|---|
| date | Sat, 07 Mar 2020 01:29:41 +0900 |
| parents | e68c3bd31098 |
| children |
line wrap: on
line source
# CbCインターフェースによる CbCXv6 の書き換え - 並列信頼研 - 桃原 優 --- # 概要 - OS の信頼性を上げたい - CbCという言語を使って xv6 という OS を書き換える - Paging の書き換えを行った - 実装中だが、将来はコンテナやVMを実装できるはず --- # OS の信頼性を上げたい - OS自体が複雑で検証が困難。 - バグの原因に - OSの仕様を定義してそれを満たすことを証明する - 証明しやすい形の記述を作る - CbCの goto で書く - 状態遷移系に近い形で記述できる(証明しやすい) - 関数型の記述 - 入力に対しての出力を検証する - 記述のモジュール化 - CbCのインターフェースで書く - 煩雑な記述の解消 - 入力の切り替えによる機能の入れ替え --- # ノーマルレベルとメタレベル - ノーマルレベル - CbCで記述される部分 - メタレベル - Paging などのメモリやCPU自体の操作 - (ノーマルレベルの)プログラムの正しさの証明 - cmake で生成している --- # Continuation based C - 状態遷移ベースで記述できる言語(以下CbC) - cmake で CbC からメタレベルの記述を生成する - Code Gear - 基本的な処理の単位 - goto 文で遷移する - Data Gear - Code Gear からアクセスできるデータの単位 - 引数など - Meta Code Gear - Code Gear の間に挟まれるメタレベルの処理 - Meta Data Gear - Code Gearの間の接続などの情報 - Context(後ほど説明) --- # ノーマルレベル --- # Code Gear による継続 - Code Gear の処理の間を goto によって遷移していく - __code CodeGear名 で定義  --- # Data Gear の継続 - Code Gear からアクセスできるデータ - input Data Gear と Output Data Gear で証明する  --- # メタレベル --- # Meta Code Gear - メタレベルで見ると Code Gear の間にメタレベルの処理が挟まっている - cmake で __code CodeGear名_stub が生成される  --- # Meta Data Gear - ノーマルレベルでの書き換えやアクセスを防ぐために存在 - CbC の 接続可能な Code Gear, Data Gear のリスト - Data Gear を確保するメモリ空間 - Context --- # Context - Meta Data Gear - Contextには全てのData Gear と Code Gear が登録されている - Xv6ではユーザープロセスに対応して1つのcontextが存在する - 将来的なVMやコンテナの実装はContextの切り替えるによる実装を目指している  --- # Xv6 - MIT の講義用教材として作られたOS - 規格化される前のCで書かれたUNIX V6 を書き換えた - 1万行程の軽量なOS - Linuxだと数千万行 - Xv6 をCbCで書き換える --- # Xv6の構成 - system call - カーネル空間の処理の呼び出し - VM(仮想メモリ) - Paging - File System - I/O, Read, Write - Scheduler など --- # カーネル空間 - OS の中核となるプログラムで Meta Level に相当する - Xv6 ではカーネルとユーザープログラムは分離されている - ユーザープログラムはカーネルに直接アクセスできない。 - ユーザープログラムによる書き換えやアクセスを防ぐため - 呼び出す場合は system call --- # Paging - Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理 - 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる --- # Xv6の書き換え方針 - メタレベルからノーマルレベルを保証するOSを作りたい - 段階的に書き換えていきたい - Paging を書き換える理由 - OS の信頼性を保証する上で重要なメモリ管理部分 - __code で書き直していく --- # インターフェースの導入 - ノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入 - インターフェースによるメリット - 煩雑な記述の解消 - 入力の切り替えによる実装の入れ替え - 実装は別で定義し、呼び出す - 後ほど説明 --- # CbCインターフェース - Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する **Meta Data Gear** - インターフェースを定義してそこから呼び出す --- # インターフェースの定義 - Xv6 の Virtual Memory の API 部分のインターフェース - 以下のコードについて説明していく ``` c typedef struct vm<Type,Impl> { __code init_vmm(Impl* vm, __code next(...)); __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...)); __code kpt_alloc(Impl* vm ,__code next(...)); __code switchuvm(Impl* vm ,struct proc* p, __code next(...)); __code init_inituvm(Impl* vm, pde_t* pgdir, char* init, uint sz, __code next(...)); __code loaduvm(Impl* vm,pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz, __code next(...)); __code allocuvm(Impl* vm, pde_t* pgdir, uint oldsz, uint newsz, __code next(...)); ``` --- # インターフェースの命名(1行目) - typedef struct の直後にインターフェース名(vm)を書く ``` c typedef struct vm<Type,Impl> { ``` --- # インターフェースの Code Gear(2行目~) - vm で使う Code Gear を登録する - Code Gear は __code CodeGear名(引数); で記述する - 引数が Data Gear に相当する - 第1引数の Impl* vm がインターフェースの実装の型になる ``` c typedef struct vm<Type,Impl> { __code init_vmm(Impl* vm, __code next(...)); __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...)); __code kpt_alloc(Impl* vm ,__code next(...)); __code switchuvm(Impl* vm ,struct proc* p, __code next(...)); __code init_inituvm(Impl* vm, pde_t* pgdir, char* init, uint sz, __code next(...)); __code loaduvm(Impl* vm,pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz, __code next(...)); __code allocuvm(Impl* vm, pde_t* pgdir, uint oldsz, uint newsz, __code next(...)); ``` --- # next(...) - __code next(...) は次の Code Gear の継続先 - それぞれの Code Gear の引数の1つに設定する ``` c __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...)); //.... __code next(...); } vm; ``` - 例) goto vm->kpt_freerange の引数に exit を設定すると Code Gear である exit に遷移する ``` c __code exit(){ //.... } goto vm->kpt_freerange(vm, low, hi, exit); ``` --- # Interface の実装の型 - 実装側のヘッダーファイルも vm_impl と同じように用意する ``` c typedef struct vm_impl<Impl, Isa> impl vm{ ... __code loaduvm_ptesize_check(Type* vm_impl, uint i, pte_t* pte, uint sz, __code next(...)); ``` --- # インターフェースの実装 - 実装は型と実装をそれぞれ別ファイルで定義する(vm_impl.h と vm_impl.cbc) - 実装するインターフェースは #interface で宣言する ``` c #interface "vm.h" ``` --- # vmインターフェースの実装の初期化 - 定義が終わったのでインターフェースを使用したい - メモリ上にインターフェースの置き場所と実装を確保 - struct vm* vm = new vm(); - インターフェースと実装の紐付け - vm->void_ret = C_vm_void_ret; - Code Gear の enum の設定 - インターフェースのAPIと enum の番号を紐付けている ``` c vm* createvm_impl(struct Context* cbc_context) { struct vm* vm = new vm(); struct vm_impl* vm_impl = new vm_impl(); vm->vm = (union Data*)vm_impl; .... vm->void_ret = C_vm_void_ret; vm->init_vmm = C_init_vmmvm_impl; vm->kpt_freerange = C_kpt_freerangevm_impl; vm->loaduvm = C_loaduvmvm_impl; vm->kpt_alloc = C_kpt_allocvm_impl; ``` - APIの実装の例(init_vmm) - C_init_vmmvm_impl が メタレベルでinit_vmmvm_impl と対応する ``` c __code init_vmmvm_impl(struct vm_impl* vm,__code next(...)) { initlock(&kpt_mem.lock, "vm"); kpt_mem.freelist = NULL; goto next(...); } ``` --- # インターフェース実装内の CbC - for文やif文がある場合はさらに実装を分ける - 状態遷移ベースで記述したい - インターフェースは外から呼び出されるAPI - それに対してインターフェースの実装の Code Gearから明示的に呼び出される Code Gearは、Java の private メソッドのように扱われる。 - 実際に vm.c の loaduvm の実装を分けた記述を説明する ---  --- # 実装内の明示的な遷移の処理 - **vm と同じ create_impl 内で** vm_impl を定義し、private で実装する Code Gear を定義する - loaduvmvm_impl で goto によって private に遷移する ``` c __code loaduvmvm_impl(struct vm_impl* vm, pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz, __code next(...)) { Gearef(cbc_context, vm_impl)->pgdir = pgdir; Gearef(cbc_context, vm_impl)->addr = addr; Gearef(cbc_context, vm_impl)->ip = ip; Gearef(cbc_context, vm_impl)->offset = offset; Gearef(cbc_context, vm_impl)->sz = sz; Gearef(cbc_context, vm_impl)->next = next; goto loaduvm_ptesize_checkvm_impl(vm, next(...)); } ``` - vm のインターフェースの実装を vm_impl に設定している - vm の実装内で使用する Code Gear も enum の番号で指定する - vm_impl->loaduvm_ptesize_check = C_loaduvm_ptesize_checkvm_impl; ``` c vm* createvm_impl(struct Context* cbc_context) { struct vm* vm = new vm(); struct vm_impl* vm_impl = new vm_impl(); vm->vm = (union Data*)vm_impl; ... vm_impl->loaduvm_ptesize_check = C_loaduvm_ptesize_checkvm_impl; .... vm->loaduvm = C_loaduvmvm_impl; .... } ``` --- # loaduvmの CbCによる書き換え - loaduvmは - swapから呼び出す - kernelの中をloopしてreadiに入る - 入った場合は待ちになる - user proc側が待ちになる - vm.cのloaduvmの処理をCbC で書き換える ``` c int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz) { uint i, pa, n; pte_t *pte; if ((uint) addr % PTE_SZ != 0) { panic("loaduvm: addr must be page aligned"); } for (i = 0; i < sz; i += PTE_SZ) { if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) { panic("loaduvm: address should exist"); } pa = PTE_ADDR(*pte); if (sz - i < PTE_SZ) { n = sz - i; } else { n = PTE_SZ; } if (readi(ip, p2v(pa), offset + i, n) != n) { return -1; } } return 0; } ``` - loaduvm_impl がインターフェースから呼ばれる実装 ``` c __code loaduvmvm_impl(struct vm_impl* vm, pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz, __code next(...)) { Gearef(cbc_context, vm_impl)->pgdir = pgdir; Gearef(cbc_context, vm_impl)->addr = addr; Gearef(cbc_context, vm_impl)->ip = ip; Gearef(cbc_context, vm_impl)->offset = offset; Gearef(cbc_context, vm_impl)->sz = sz; Gearef(cbc_context, vm_impl)->next = next; goto loaduvm_ptesize_checkvm_impl(vm, next(...)); } ``` - loaduvm_impl から private な Code Gear が呼ばれる ``` c #interface "vm_impl.h" __code loaduvm_ptesize_checkvm_impl(struct vm_impl* vm_impl, __code next(...)) { char* addr = vm_impl->addr; if ((uint) addr %PTE_SZ != 0) { // goto panic } goto loaduvm_loopvm_impl(vm_impl, next(...)); } ``` - vm.c のloaduvm の実装を CbC で書き直す ``` c int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz) { uint i, pa, n; pte_t *pte; if ((uint) addr % PTE_SZ != 0) { panic("loaduvm: addr must be page aligned"); } for (i = 0; i < sz; i += PTE_SZ) { if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) { panic("loaduvm: address should exist"); } pa = PTE_ADDR(*pte); if (sz - i < PTE_SZ) { n = sz - i; } else { n = PTE_SZ; } if (readi(ip, p2v(pa), offset + i, n) != n) { return -1; } } return 0; } ``` - vm.cではここから for だが CbC は if文の中と外にgoto を用意して実装する  ```c __code loaduvm_loopvm_impl(struct vm_impl* vm_impl, __code next(...)) { uint i = vm_impl->i; uint sz = vm_impl->sz; if (i < sz) { goto loaduvm_check_pgdir(vm_impl, next(ret, ...)); } goto loaduvm_exit(vm_impl, next(...)); } __code loaduvm_check_pgdir(struct vm_impl* vm_impl, __code next(...)) { pte_t* pte = vm_impl->pte; pde_t* pgdir = vm_impl->pgdir; uint i = vm_impl->i; char* addr = vm_impl->addr; uint pa = vm_impl->pa; if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) { // goto panic } pa = PTE_ADDR(*pte); vm_impl->pte = pte; vm_impl->pgdir = pgdir; vm_impl->addr = addr; vm_impl->pa = pa; goto loaduvm_check_PTE_SZ(vm_impl, next(...)); } __code loaduvm_check_PTE_SZ(struct vm_impl* vm_impl, __code next(int ret, ...)) { if (sz - i < PTE_SZ) { n = sz - i; } else { n = PTE_SZ; } if (readi(ip, p2v(pa), offset + i, n) != n) { ret = -1; goto next(ret, ...); } vm_impl->n = n; goto loaduvm_loopvm_impl(vm_impl, next(ret, ...)); } __code loaduvm_exit(struct vm_impl* vm_impl, __code next(int ret, ...)) { ret = 0; goto next(ret, ...); } ``` --- # C を CbC に部分的に書き直す手法 - CbC の場合 goto による 遷移を行うので、関数呼び出しのように goto 以降のコードを実行できない - 例) goto すると戻ってこれないため それ以降が実行されなくなる。 --- # CbC から C への遷移 - 最初の命令は next で戻ってこれるので、dummy の関数を用意してそこで実行する ``` c void cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz) { // inituvm(p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); struct vm* vm = createvm_impl(cbc_context); // goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret); Gearef(cbc_context, vm)->vm = (union Data*) vm; Gearef(cbc_context, vm)->pgdir = pgdir; Gearef(cbc_context, vm)->init = init; Gearef(cbc_context, vm)->sz = sz ; Gearef(cbc_context, vm)->next = C_vm_void_ret ; goto meta(cbc_context, vm->init_inituvm); } void userinit(void) { struct proc* p; extern char _binary_initcode_start[], _binary_initcode_size[]; p = allocproc(); initContext(&p->cbc_context); initproc = p; if((p->pgdir = kpt_alloc()) == NULL) { panic("userinit: out of memory?"); } cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); ``` --- # まとめ - OS 内部で CbC インターフェースを扱えるようになった - CbC の書 き換えが完了すれば、継続の入力と出力を検査することで OS の信頼性を保証したり、インターフェースの実装の入れ替えが可能になる。 - Context による複数環境の入れ替えや同時実行を可能にすることで CbCXv6 に おいて コンテナと VM を実装ができると予想される。