# HG changeset patch
# User tobaru
# Date 1581155982 -32400
# Node ID 6d84ce92ff356ac2e2211c2f2b9404a522b32ad2
# Parent  ff1f2c66a84dd89b224db603656c79815a5d767e
.

diff -r ff1f2c66a84d -r 6d84ce92ff35 paper/GearsOS.tex
--- a/paper/GearsOS.tex	Sat Feb 08 17:22:55 2020 +0900
+++ b/paper/GearsOS.tex	Sat Feb 08 18:59:42 2020 +0900
@@ -57,7 +57,7 @@
 この問題を防ぐため、Context から必要な Data Gear のみをノーマルレベルの Code Gear に渡す処理を行なっている。
 
 
- Meta Code Gear は使用される全ての Code Gear ごとに記述する必要がある。しかし、全ての Code Gear に対して記述すると膨大な記述量になる。そのため、Interface を実装した code Gear の Meta Code Gear は Perl スクリプトで自動生成する。
+ Meta Code Gear は使用される全ての Code Gear ごとに記述する必要がある。しかし、全ての Code Gear に対して記述すると膨大な記述量になる。そのため、Interface を実装した Code Gear の Meta Code Gear は Perl スクリプトで自動生成する。
 
 
 Meta Code Gear はユーザーが記述することも可能である。そうすることでメタ計算を記述することができるようになったり、goto による継続先を変更することで Geas OS の機能を置き換えることができる。
diff -r ff1f2c66a84d -r 6d84ce92ff35 paper/fig/cbc_for_private.graffle
Binary file paper/fig/cbc_for_private.graffle has changed
diff -r ff1f2c66a84d -r 6d84ce92ff35 paper/fig/cbc_for_private.pdf
Binary file paper/fig/cbc_for_private.pdf has changed
diff -r ff1f2c66a84d -r 6d84ce92ff35 paper/src/fix_vm.h
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/fix_vm.h	Sat Feb 08 18:59:42 2020 +0900
@@ -0,0 +1,17 @@
+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(...));
+    __code clearpteu(Impl* vm, pde_t* pgdir, char* uva,  __code next(...));
+    __code copyuvm(Impl* vm, pde_t* pgdir, uint sz, __code next(...));
+    __code uva2ka(Impl* vm, pde_t* pgdir, char* uva, __code next(...));
+    __code copyout(Impl* vm, pde_t* pgdir, uint va, void* pp, uint len, __code next(...));
+    __code paging_int(Impl* vm, uint phy_low, uint phy_hi, __code next(...));
+    __code void_ret(Impl* vm);
+    __code next(...);
+} vm;
+
diff -r ff1f2c66a84d -r 6d84ce92ff35 slide/CbCXv6.md
--- a/slide/CbCXv6.md	Sat Feb 08 17:22:55 2020 +0900
+++ b/slide/CbCXv6.md	Sat Feb 08 18:59:42 2020 +0900
@@ -4,14 +4,12 @@
 
 ---
 
-# 目次
-1. **OS の信頼性の保証**
-2. CbC による Gears OS の開発
-3. Xv6
-4. CbCXv6 での Paging
-5. CbC インターフェース
-6. 評価
-7. まとめ　
+# 概要
+- OS の信頼性を保証したい
+- メタレベルを記述できる CbC で OS の開発
+- インターフェースの導入
+    - 煩雑な記述の解消
+    - Agdaによる証明のため
 
 ---
 
@@ -23,7 +21,7 @@
 
 ---
 
-# OS の信頼性の重要性
+# OS の検証
 
 - 全てのOSのコードに対して検証を行うのは困難
     - 複雑な機能が多い
@@ -36,7 +34,6 @@
 
 ---
 
-
 # メタレベルとノーマルレベル
 - ノーマルレベル
     - ユーザーがプログラミング言語によって記述する部分の処理 
@@ -75,6 +72,7 @@
 # Meta Code Gear
 - 実際にはノーマルレベルの間にメタレベルの処理がある
 - Meta Level では Data Gear の見え方は変わる(Meta Data Gear)
+    - 書き換えやアクセスを防ぐため
 
 ![](https://i.imgur.com/vy0NxrG.png)
 
@@ -90,11 +88,11 @@
 - モデル検査
     - 定理証明支援系である Agda を用いる。
 - Agda
-    - Haure Logic という検証手法を扱える。
+    - Hoare Logic という検証手法を扱える。
 
 ---
 
-# Haure Logic
+# Hoare Logic
 - 検証手法
     - 事前条件を使ってある関数を実行して事後条件を満たすことを確認する
 - CbCと相性がいい
@@ -118,46 +116,26 @@
 # インターフェース
 - 書き換えを防ぐために見える Data Gear に違いが生じる
 - -> Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入
-- 機能の入れ替えによる他のメリット
+- インターフェースによる他のメリット
     - 煩雑な記述の解消
     - 機能の入れ替え
     - Agda による証明
 
-
----
-
-# 目次
-1. OS の信頼性の保証
-2. **CbC による Gears OS の開発**
-3. Xv6
-4. CbCXv6 での Paging
-5. CbC インターフェース
-6. 評価
-7. まとめ　
-
 ---
 
 # CbC による Gears OS の開発
-- a
-
-
 
 ---
 
-
 # Context
-- a 
-
----
-
-# 目次
-1. OS の信頼性の保証
-2. CbC による Gears OS の開発
-3. **Xv6**
-4. CbCXv6 での Paging
-5. CbC インターフェース
-6. 評価
-7. まとめ　
+- Meta Data Gear
+    - Code Gear
+    - Data Gear のリスト
+    - Data Gear を確保するメモリ空間
+- スレッドやプロセスに対応
+- ノーマルレベルに必要な処理のみ Code Gear に渡す
+- Meta Code Gear は Perlスクリプトで自動生成
+- 継続先を変えることで機能を置き換えることも可能
 
 ---
 
@@ -204,29 +182,12 @@
 
 ---
 
-# system call 
-- ソースコード載せる
-
----
-
 # Xv6-rpi
 - Xv6 は　Arm のバイナリを出力するので様々なハードウェアで動かすことができる
     - Raspberry Pi
     - 携帯電話
-- 実際にRaspberry Pi で動かすために xv6-rpi を用意して動作しているかコンソールで確認中
-    - CbCxv6 とは別
-
-
----
-
-# 目次
-1. OS の信頼性の保証
-2. CbC による Gears OS の開発
-3. Xv6
-4. **CbCXv6 での Paging**
-5. CbC インターフェース
-6. 評価
-7. まとめ　
+- 実際にRaspberry Pi で動かすために xv6-rpi を用意して動作しているか確認中
+    - CbCxv6 とは別のプロジェクト
 
 ---
 
@@ -252,6 +213,8 @@
 
 # Pagingの図
 - 必要？
+![](https://i.imgur.com/ZNxOsNf.png)
+
 
 ---
 
@@ -276,17 +239,6 @@
 
 ---
 
-# 目次
-1. OS の信頼性の保証
-2. CbC による Gears OS の開発
-3. Xv6
-4. CbCXv6 での Paging
-5. **CbC インターフェース**
-6. 評価
-7. まとめ　
-
----
-
 # CbC インターフェースの導入
 - 継続の記述が煩雑になる
     - Code Gear がどの Data Gear の番号に対応するか指定する必要がある
@@ -325,21 +277,6 @@
 
 ---
 
-# Data Gear の定義
-- 2行目から19行目で引数の Data Gear を定義している
-
-
-``` c
-typedef struct vm<Type,Impl> {
-    union Data* vm;
-    uint low;
-    uint hi;
-    struct proc* p;
-....
-```
-
----
-
 # Code Gear の定義
 - Code Gear は __Code CodeGear名(引数); で記述する
 - 第1引数の Impl* vm が Code Gear の型になる
@@ -348,6 +285,7 @@
 
 
 ``` 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(...));
@@ -356,8 +294,6 @@
     __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(...));
 
-....
-
 ```
 
 ---
@@ -496,7 +432,6 @@
 
 # private の記述
 
-
 ``` c
 #interface "vm_impl.h"
 
@@ -682,7 +617,7 @@
         panic("userinit: out of memory?");
     }
 
-    dummy(p, _binary_initcode_start, _binary_initcode_size);
-~                                                            
+    dummy(p, _binary_initcode_start, _binary_initcode_size);                     
+```
 
-```
+