Mercurial > hg > Papers > 2020 > tobaru-master

changeset 31:69ac4230c3f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix slide
author tobaru
date Sun, 09 Feb 2020 22:52:56 +0900
parents 61c4015fed19
children 4c24694af0b0
files paper/Paging.tex paper/master_paper.pdf paper/master_paper.synctex.gz paper/master_paper.tex slide/CbCXv6.md
diffstat 5 files changed, 175 insertions(+), 160 deletions(-) [+]
line wrap: on
line diff
--- a/paper/Paging.tex	Sun Feb 09 19:13:32 2020 +0900
+++ b/paper/Paging.tex	Sun Feb 09 22:52:56 2020 +0900
@@ -15,18 +15,18 @@
 Paging を扱うことでブロック単位で管理することによりフラグメンテーションが解消でき、MMUが実メモリを管理することによってプログラム側で空いているメモリを探す必要がなくなる。
 
 
-図 \ref{fig:MemoryConstitution} で Xv6の仮想メモリと実メモリについて説明する。
-図のRWX は読み込み、書き込み、実行の権限を表している。
-
-
- \begin{figure}[ht]
- \begin{center}
-  \includegraphics[width=160mm]{./fig/MemoryConstitution}
- \end{center}
- \caption{On the left, xv6’s kernel address space. RWX refer to PTE read, write, and execute
-permissions. On the right, the RISC-V physical address space that xv6 expects to see.\cite{xv6}} 
- \label{fig:MemoryConstitution}
-\end{figure}
+% 図 \ref{fig:MemoryConstitution} で Xv6の仮想メモリと実メモリについて説明する。
+% 図のRWX は読み込み、書き込み、実行の権限を表している。
+% 
+% 
+%  \begin{figure}[ht]
+%  \begin{center}
+%   \includegraphics[width=160mm]{./fig/MemoryConstitution}
+%  \end{center}
+%  \caption{On the left, xv6’s kernel address space. RWX refer to PTE read, write, and execute
+% permissions. On the right, the RISC-V physical address space that xv6 expects to see.\cite{xv6}} 
+%  \label{fig:MemoryConstitution}
+% \end{figure}
 
 
 \section{CbCXv6 での Paging}
Binary file paper/master_paper.pdf has changed
Binary file paper/master_paper.synctex.gz has changed
--- a/paper/master_paper.tex	Sun Feb 09 19:13:32 2020 +0900
+++ b/paper/master_paper.tex	Sun Feb 09 22:52:56 2020 +0900
@@ -10,6 +10,7 @@
 \usepackage[deluxe, multi]{otf}
 
 
+
 %\input{dummy.tex} %% font
 
 \jtitle{CbCインターフェースによる CbCXv6 の書き換え}
--- a/slide/CbCXv6.md	Sun Feb 09 19:13:32 2020 +0900
+++ b/slide/CbCXv6.md	Sun Feb 09 22:52:56 2020 +0900
@@ -6,7 +6,7 @@
 
 # 概要
 - OS の信頼性を上げたい
-- CbCを使って xv6 を書き換える 
+- CbCを使って xv6 という OS を書き換える 
 - Paging の書き換えを行った
 - まだ実装中
 - 将来はコンテナやVMをメタ計算として実装できるはず
@@ -17,7 +17,7 @@
 - 仕様を満たすことを証明する
 - 証明しやすい形の記述を作る
 - CbCの goto で書く
-    - 状態遷移系に近い形で記述できる
+    - 状態遷移系に近い形で記述できる(証明しやすい)
     - 関数型の記述
 - CbCのinterface で書く
 - 記述のモジュール化
@@ -61,39 +61,33 @@
 ---
 
 # Data Gear の継続
+- Code Gear で定義されたデータ
 - goto の際に Data Gear も継続される
-
+ 
 ![](https://i.imgur.com/3E0DGWA.png)
 
 ---
 
-# インターフェース
-- 書き換えを防ぐために見える Data Gear に違いが生じる
-- -> Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入
-- インターフェースによる他のメリット
-    - 煩雑な記述の解消
-    - 機能の入れ替え
-    - Agda による証明
-
----
-
-
 # Meta Code Gear
 - 実際にはノーマルレベルの間にメタレベルの処理がある
-- Meta Level では Data Gear の見え方は変わる(Meta Data Gear)
-    - 書き換えやアクセスを防ぐため
 
 ![](https://i.imgur.com/vy0NxrG.png)
 
 ---
 
-# Geas OS
-- Xv6 をCbCで書き換える
+# Meta Data Gear
+- CbC では接続可能な Code Gear, Data Gear のリスト
+- Data Gear を確保するメモリ空間
+- ノーマルレベルでの書き換えやアクセスを防ぐために存在
+
+---
+
+# Xv6
 - MIT の講義用教材として作られたOS
-    - 企画課される前のCで書かれたUNIX V6 を書き換えた
+    - 規格化される前のCで書かれたUNIX V6 を書き換えた
     - 1万行程の軽量なOS
     - Linuxだと数千万行
-- Xv6 を参考に CbC で書き直すことで Gears OS を実装する
+- Xv6 をCbCで書き換える
 
 ---
 
@@ -101,25 +95,18 @@
 # Xv6の構成
 - systemcall
 - Scheduler
-- VM
+- Virtual Memory
 - file system
 - tty
 
 
----
-
-# Context
-- Meta Data Gear
-- ユーザープロセスに対応して1つのcontextがある
-- Contextには実行されるすべてのCode Gear が登録される
-- Data GearもContext上にある
 
 ---
 # カーネル空間
 - OS の中核となるプログラムで Meta Level に相当する
 - Xv6 ではカーネルとユーザープログラムは分離されている
 - ユーザープログラムはカーネルに直接アクセスできない。
-    - 書き換えやアクセスを防ぐため
+    - ユーザープログラムによる書き換えやアクセスを防ぐため
     - 呼び出す場合は system call
 
 ---
@@ -130,42 +117,63 @@
 - ユーザープログラムの中断
 - 処理がカーネルに切り替わる
 
-# CbCXv6 での Paging
-- OS の信頼性の1つであるメモリ管理部分
-- メモリ管理するpage table
+---
+
+# Paging
 - Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理
 - 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる
 
 ---
 
-# Pagingの図
-- 必要？
-![](https://i.imgur.com/ZNxOsNf.png)
+# Xv6の書き換え方針
+- メタレベルとノーマルレベルを記述できるOSを実装したい
+- 段階的に書き換えていきたい
+- Paging を書き換える理由
+    - OS の信頼性を保証する上で重要なメモリ管理部分
 
+- __code で書き直していく
 
 ---
-# CbC インターフェース
-- インターフェースは Data Gear に対しての操作を行う Code Gear
+
+# CbCインターフェース
+- ノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入
+- インターフェースによる他のメリット
+    - 煩雑な記述の解消
+    - 実装の入れ替え
+
 - 実装は別で定義し、呼び出す
-- インターフェースによって機能を置き換えることができる
+- インターフェースによって実装を置き換えることができる
+
+---
+
+# CbCインターフェース
+- Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する **Meta Data Gear**
+
+- インターフェース実装と定義の図入れる
 
 ---
 
 # インターフェースの定義
-- Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する **Meta Data Gear**
-
----
+- Xv6 の Virtual Memory の API 部分のインターフェース
 
-# インターフェースのソースコード
-- vm.c をインターフェースで書き換えた vm.h のコードの説明をしていく
+``` 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(...));
 
+```
 
 ---
 
 
-# 実装名の定義
-- typedef struct の直後に実装名(vm)を書く
-
+# インターフェースの命名
+- typedef struct の直後にインターフェース名(vm)を書く
+- Data Gear にマッピングされる
 
 ``` c
 typedef struct vm<Type,Impl> {
@@ -173,14 +181,11 @@
 
 ---
 
-# init_vmm
 
-
-# Code Gear の定義
-- Code Gear は __Code CodeGear名(引数); で記述する
-- 第1引数の Impl* vm が Code Gear の型になる
-- 初期化された Data Gear が それぞれの Code Gear の引数として扱われる
-- 例)定義された uinit が kpt_freerange の Code Gear の第1引数と対応している 
+# インターフェースの Code Gear
+- Code Gear は __code CodeGear名(引数); で記述する
+    - 引数が Data Gear に相当する
+- 第1引数の Impl* vm がインターフェースの実装の型になる
 
 
 ``` c
@@ -197,39 +202,59 @@
 
 ---
 
-
 # next(...)
-- __code next(...) は条件分岐によって複数の継続先が設定される
+- __code next(...) は次の Code Gear の継続先
 - それぞれの Code Gear の引数の1つに設定する
 ``` c
     __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...));
-....
+//....
     __code next(...);
 } vm;
 ```
+``` c
+__code exit(){
+//....
+}
+
+goto vm->kpt_freerange(vm, low, hi, exit);
+```
 
 ---
 
-# インターフェースの実装
-- インターフェースの実装は別ファイルで定義する(vm_impl.cbc)
-- ヘッダーファイルの呼び出しは #include ではなく #interface で呼び出す
+# Interface の実装の型
+- 実装側のヘッダーファイルも vm_impl と同じように用意する
 
 ``` c
-#include "../../context.h"
-#interface "vm.h"
-
+typedef struct vm_impl<Impl, Isa> impl vm{
+...
+    __code loaduvm_ptesize_check(Type* vm_impl, uint i, pte_t* pte, uint sz,
+__code next(...));
 ```
 
 
 ---
 
-# create_impl
+# インターフェースの実装
+- 実装は型と実装をそれぞれ別ファイルで定義する(vm_impl.h と vm_impl.cbc)
+- 実装するインターフェースは #interface で宣言する
+
+``` c
+#interface "vm.h"
+```
+
+---
+
+# 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 の番号を紐付けている
 
 ``` c
-
 vm* createvm_impl(struct Context* cbc_context) {
     struct vm* vm  = new vm();
 ....
@@ -237,7 +262,12 @@
     vm->init_vmm = C_init_vmmvm_impl;
     vm->kpt_freerange = C_kpt_freerangevm_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;
@@ -248,11 +278,48 @@
 
 --- 
 
-# private
-- CbC は信頼性を保証するためにそれぞれの Code Gear を細かくする必要があるので、for文やif文がある場合はさらに実装を分ける
--  Code Gear は基本的にインターフェースで指定された Code Gear 内からのみ継続さ れるため、Java の private メソッドのように扱われる。
+# インターフェース実装内の 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(...));
+}
+```
+
+``` c
+vm* createvm_impl(struct Context* cbc_context) {
+...
+    struct vm_impl* vm_impl = new vm_impl();
+...
+    vm_impl->loaduvm_ptesize_check = C_loaduvm_ptesize_checkvm_impl;
+....
+    vm->loaduvm = C_loaduvmvm_impl;
+....
+}
+```
+---
+
+# loaduvmの CbCによる書き換え
+- loaduvmは何でなぜ書き換えてるのか
+- vm.cのloaduvmの処理をCbC で書き換える
 
 ``` c
 int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz)
@@ -286,24 +353,10 @@
 }
 ```
 
----
-
-# goto private
-- vm と同じ create_impl 内で vm_impl を定義し、private で実装する Code Gear を定義する
-- loaduvmvm_impl で goto によって private に遷移する
+- loaduvm_impl がインターフェースから呼ばれる実装
 
 
 ``` c
-vm* createvm_impl(struct Context* cbc_context) {
-...
-    struct vm_impl* vm_impl = new vm_impl();
-...
-    vm_impl->loaduvm_ptesize_check = C_loaduvm_ptesize_checkvm_impl;
-....
-    vm->loaduvm = C_loaduvmvm_impl;
-....
-}
-
 __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;
@@ -315,42 +368,29 @@
     goto loaduvm_ptesize_checkvm_impl(vm, next(...));
 }
 ```
----
-
-# private のヘッダー
-- private 側のヘッダーファイルも 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(int ret, ...));
-```
-
----
-
-# private の記述
+- loaduvm_impl から private な Code Gear が呼ばれる
 
 ``` c
 #interface "vm_impl.h"
 
-__code loaduvm_ptesize_checkvm_impl(struct vm_impl* vm_impl, __code next(int ret, ...)) {
+__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(ret, ...));
+    goto loaduvm_loopvm_impl(vm_impl, next(...));
 }
 ```
 
+
 - vm.cではここから for だが CbC は if文の中と外にgoto を用意して実装する
 
 ![](https://i.imgur.com/ByA7GVJ.png)
 
 ```c
-__code loaduvm_loopvm_impl(struct vm_impl* vm_impl, __code next(int ret, ...)) {
+__code loaduvm_loopvm_impl(struct vm_impl* vm_impl, __code next(...)) {
     uint i = vm_impl->i;
     uint sz = vm_impl->sz;
 
@@ -358,11 +398,11 @@
         goto loaduvm_check_pgdir(vm_impl, next(ret, ...));
     }
 
-    goto loaduvm_exit(vm_impl, next(ret, ...));
+    goto loaduvm_exit(vm_impl, next(...));
 }
 
 
-__code loaduvm_check_pgdir(struct vm_impl* vm_impl, __code next(int ret, ...)) {
+__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;
@@ -379,17 +419,10 @@
     vm_impl->addr = addr;
     vm_impl->pa = pa;
 
-    goto loaduvm_check_PTE_SZ(vm_impl, next(ret, ...));
+    goto loaduvm_check_PTE_SZ(vm_impl, next(...));
 }
 
 __code loaduvm_check_PTE_SZ(struct vm_impl* vm_impl, __code next(int ret, ...)) {
-    uint sz = vm_impl->sz;
-    uint i = vm_impl->i;
-    uint n = vm_impl->n;
-    struct inode* ip = vm_impl->ip;
-    uint pa = vm_impl->pa;
-    uint offset = vm_impl->offset;
-
     if (sz - i < PTE_SZ) {
         n = sz - i;
     } else {
@@ -412,7 +445,7 @@
 }
 ```
 
-
+---
 
 ``` c
 
@@ -447,49 +480,27 @@
 }
 ```
 
+---
 
-# インターフェースの呼び出し
-- 定義したインターフェースの呼び出しについて説明する
+# stub 
+- goto meta はstub を呼び込んでいる
+- 説明
+
+---
+
+# C を CbC に部分的に書き直す手法
 - CbC の場合 goto による 遷移を行うので、関数呼び出しのように goto 以降のコードを実行できない
 - 例) goto すると戻ってこれないため それ以降が実行されなくなる。
 
-``` c
-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?");
-    }
-
-    goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
-    p->sz = PTE_SZ;
-
-    // craft the trapframe as if
-    memset(p->tf, 0, sizeof(*p->tf));
-~                                          
-```
-
-# 呼び出しの解決
+# CbC から C への遷移
 - 最初の命令は next で戻ってこれるので、dummy の関数を用意してそこで実行する
 
 ``` c
-void dummy(struct proc *p, char _binary_initcode_start[], char _binary_initcode_size[])
-{ 
+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);
-    goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
-
-}
-
-
-
-__ncode cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz){//:skip
 
     struct vm* vm = createvm_impl(cbc_context);
     // goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret);
@@ -501,7 +512,6 @@
     goto meta(cbc_context, vm->init_inituvm);
 }
 
-
 void userinit(void)
 {
     struct proc* p;
@@ -516,7 +526,11 @@
         panic("userinit: out of memory?");
     }
 
-    dummy(p, _binary_initcode_start, _binary_initcode_size);                     
+    cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
+
 ```
 
+---
 
+# まとめ
+