Mercurial > hg > Papers > 2020 > tobaru-master

diff slide/CbCXv6.md @ 21:6d84ce92ff35
.
author: tobaru
date: Sat, 08 Feb 2020 18:59:42 +0900
parents: 98cee2f6c919
children: 49d691a92b41
--- 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);                     
+```
 
-```
+
author	tobaru
date	Sat, 08 Feb 2020 18:59:42 +0900
parents	98cee2f6c919
children	49d691a92b41