Mercurial > hg > Papers > 2020 > tobaru-master
diff slide/CbCXv6.md @ 33:e68c3bd31098
after Master's Thesis Examination
| author | tobaru |
|---|---|
| date | Mon, 10 Feb 2020 18:01:43 +0900 |
| parents | 69ac4230c3f2 |
| children |
line wrap: on
line diff
--- a/slide/CbCXv6.md Sun Feb 09 22:55:38 2020 +0900 +++ b/slide/CbCXv6.md Mon Feb 10 18:01:43 2020 +0900 @@ -6,79 +6,98 @@ # 概要 - OS の信頼性を上げたい -- CbCを使って xv6 という OS を書き換える +- CbCという言語を使って xv6 という OS を書き換える - Paging の書き換えを行った -- まだ実装中 -- 将来はコンテナやVMをメタ計算として実装できるはず +- 実装中だが、将来はコンテナやVMを実装できるはず --- # OS の信頼性を上げたい -- 仕様を満たすことを証明する +- OS自体が複雑で検証が困難。 + - バグの原因に +- OSの仕様を定義してそれを満たすことを証明する - 証明しやすい形の記述を作る - CbCの goto で書く - 状態遷移系に近い形で記述できる(証明しやすい) - 関数型の記述 -- CbCのinterface で書く + - 入力に対しての出力を検証する - 記述のモジュール化 + - CbCのインターフェースで書く + - 煩雑な記述の解消 + - 入力の切り替えによる機能の入れ替え --- -# メタレベルとノーマルレベル +# ノーマルレベルとメタレベル - ノーマルレベル - - CbCで記述される普通のアルゴリズム + - CbCで記述される部分 - メタレベル - Paging などのメモリやCPU自体の操作 - - プログラムの正しさの証明 -- Context - - メタレベルで使用される Meta Data を置く場所 + - (ノーマルレベルの)プログラムの正しさの証明 + - cmake で生成している --- # Continuation based C -- ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC) +- 状態遷移ベースで記述できる言語(以下CbC) +- cmake で CbC からメタレベルの記述を生成する - Code Gear - 基本的な処理の単位 - goto 文で遷移する - Data Gear - - データの単位 + - Code Gear からアクセスできるデータの単位 + - 引数など - Meta Code Gear - - goto meta - - Code Gear の間に挟める計算 + - Code Gear の間に挟まれるメタレベルの処理 - Meta Data Gear - - Context - - Code Gearの間の接続など + - Code Gearの間の接続などの情報 + - Context(後ほど説明) --- -# goto による継続 +# ノーマルレベル +--- +# Code Gear による継続 - Code Gear の処理の間を goto によって遷移していく - +- __code CodeGear名 で定義  --- # Data Gear の継続 -- Code Gear で定義されたデータ -- goto の際に 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 のリスト +- ノーマルレベルでの書き換えやアクセスを防ぐために存在 +- CbC の 接続可能な Code Gear, Data Gear のリスト - Data Gear を確保するメモリ空間 -- ノーマルレベルでの書き換えやアクセスを防ぐために存在 +- Context + +--- + +# Context +- Meta Data Gear +- Contextには全てのData Gear と Code Gear が登録されている +- Xv6ではユーザープロセスに対応して1つのcontextが存在する +- 将来的なVMやコンテナの実装はContextの切り替えるによる実装を目指している + --- @@ -91,17 +110,17 @@ --- - # Xv6の構成 -- systemcall -- Scheduler -- Virtual Memory -- file system -- tty - - +- system call + - カーネル空間の処理の呼び出し +- VM(仮想メモリ) + - Paging +- File System + - I/O, Read, Write +- Scheduler など --- + # カーネル空間 - OS の中核となるプログラムで Meta Level に相当する - Xv6 ではカーネルとユーザープログラムは分離されている @@ -111,14 +130,6 @@ --- -# system call -- system call 呼び出し -- トラップ の発生 -- ユーザープログラムの中断 -- 処理がカーネルに切り替わる - ---- - # Paging - Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理 - 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる @@ -126,7 +137,7 @@ --- # Xv6の書き換え方針 -- メタレベルとノーマルレベルを記述できるOSを実装したい +- メタレベルからノーマルレベルを保証するOSを作りたい - 段階的に書き換えていきたい - Paging を書き換える理由 - OS の信頼性を保証する上で重要なメモリ管理部分 @@ -135,26 +146,25 @@ --- -# CbCインターフェース +# インターフェースの導入 - ノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入 -- インターフェースによる他のメリット +- インターフェースによるメリット - 煩雑な記述の解消 - - 実装の入れ替え - + - 入力の切り替えによる実装の入れ替え - 実装は別で定義し、呼び出す -- インターフェースによって実装を置き換えることができる + - 後ほど説明 --- # CbCインターフェース - Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する **Meta Data Gear** - -- インターフェース実装と定義の図入れる +- インターフェースを定義してそこから呼び出す --- # インターフェースの定義 - Xv6 の Virtual Memory の API 部分のインターフェース +- 以下のコードについて説明していく ``` c typedef struct vm<Type,Impl> { @@ -171,9 +181,8 @@ --- -# インターフェースの命名 +# インターフェースの命名(1行目) - typedef struct の直後にインターフェース名(vm)を書く -- Data Gear にマッピングされる ``` c typedef struct vm<Type,Impl> { @@ -182,7 +191,8 @@ --- -# インターフェースの Code Gear +# インターフェースの Code Gear(2行目~) +- vm で使う Code Gear を登録する - Code Gear は __code CodeGear名(引数); で記述する - 引数が Data Gear に相当する - 第1引数の Impl* vm がインターフェースの実装の型になる @@ -211,6 +221,7 @@ __code next(...); } vm; ``` +- 例) goto vm->kpt_freerange の引数に exit を設定すると Code Gear である exit に遷移する ``` c __code exit(){ //.... @@ -244,23 +255,26 @@ --- -# vm_impl のコンストラクタ -- create_imple の関数内で vm の型を定義し、vm->CodeGear名 で対応させていく -- 実装を Code Gear で記述していく。 - -- struct vm* vm = new vm(); - - インターフェースのメモリ空間を確保 -- vm->void_ret = C_vm_void_ret; - - Code Gear の enum の設定 - - インターフェースのAPIと enum の番号を紐付けている +# 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; ``` @@ -287,8 +301,11 @@ --- + + +--- # 実装内の明示的な遷移の処理 -- vm と同じ create_impl 内で vm_impl を定義し、private で実装する Code Gear を定義する +- **vm と同じ create_impl 内で** vm_impl を定義し、private で実装する Code Gear を定義する - loaduvmvm_impl で goto によって private に遷移する ``` c @@ -304,10 +321,16 @@ } ``` +- 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; .... @@ -318,7 +341,12 @@ --- # loaduvmの CbCによる書き換え -- loaduvmは何でなぜ書き換えてるのか +- loaduvmは + - swapから呼び出す + - kernelの中をloopしてreadiに入る + - 入った場合は待ちになる + - user proc側が待ちになる + - vm.cのloaduvmの処理をCbC で書き換える ``` c @@ -385,6 +413,41 @@ ``` +- 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 を用意して実装する  @@ -445,46 +508,6 @@ } ``` ---- - -``` 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; -} -``` - ---- - -# stub -- goto meta はstub を呼び込んでいる -- 説明 --- @@ -533,4 +556,6 @@ --- # まとめ - +- OS 内部で CbC インターフェースを扱えるようになった +- CbC の書 き換えが完了すれば、継続の入力と出力を検査することで OS の信頼性を保証したり、インターフェースの実装の入れ替えが可能になる。 +- Context による複数環境の入れ替えや同時実行を可能にすることで CbCXv6 に おいて コンテナと VM を実装ができると予想される。