--- 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);
+
 ```
 
+---
 
+# まとめ
+