# CbCインターフェースによる CbCXv6 の書き換え
- 並列信頼研
- 桃原 優

---

# 概要
- OS の信頼性を上げたい
- CbCという言語を使って xv6 という OS を書き換える 
- Paging の書き換えを行った
- 実装中だが、将来はコンテナやVMを実装できるはず

---

# OS の信頼性を上げたい
- OS自体が複雑で検証が困難。
    - バグの原因に
- OSの仕様を定義してそれを満たすことを証明する
- 証明しやすい形の記述を作る
- CbCの goto で書く
    - 状態遷移系に近い形で記述できる(証明しやすい)
    - 関数型の記述
    - 入力に対しての出力を検証する
- 記述のモジュール化
    - CbCのインターフェースで書く
    - 煩雑な記述の解消
    - 入力の切り替えによる機能の入れ替え

---

# ノーマルレベルとメタレベル
- ノーマルレベル
    - CbCで記述される部分
- メタレベル
    - Paging などのメモリやCPU自体の操作
    - (ノーマルレベルの)プログラムの正しさの証明
    - cmake で生成している

---

# Continuation based C
- 状態遷移ベースで記述できる言語(以下CbC)
- cmake で CbC からメタレベルの記述を生成する
- Code Gear
    - 基本的な処理の単位
    - goto 文で遷移する
- Data Gear 
    - Code Gear からアクセスできるデータの単位
    - 引数など
- Meta Code Gear
    - Code Gear の間に挟まれるメタレベルの処理
- Meta Data Gear
    - Code Gearの間の接続などの情報
    - Context(後ほど説明)

---

# ノーマルレベル

---
# Code Gear による継続
- Code Gear の処理の間を goto によって遷移していく
- __code CodeGear名 で定義
![](https://i.imgur.com/etfQund.png)


---

# Data Gear の継続
- Code Gear からアクセスできるデータ
- input Data Gear と Output Data Gear で証明する
 
![](https://i.imgur.com/3E0DGWA.png)

---
# メタレベル

---

# Meta Code Gear
- メタレベルで見ると Code Gear の間にメタレベルの処理が挟まっている
- cmake で __code CodeGear名_stub が生成される
![](https://i.imgur.com/vy0NxrG.png)

---

# Meta Data Gear
- ノーマルレベルでの書き換えやアクセスを防ぐために存在
- CbC の 接続可能な Code Gear, Data Gear のリスト
- Data Gear を確保するメモリ空間
- Context

---

# Context
- Meta Data Gear
- Contextには全てのData Gear と Code Gear が登録されている
- Xv6ではユーザープロセスに対応して1つのcontextが存在する
- 将来的なVMやコンテナの実装はContextの切り替えるによる実装を目指している
![](https://i.imgur.com/GLIew1x.png)

---

# Xv6
- MIT の講義用教材として作られたOS
    - 規格化される前のCで書かれたUNIX V6 を書き換えた
    - 1万行程の軽量なOS
    - Linuxだと数千万行
- Xv6 をCbCで書き換える

---

# Xv6の構成
- system call
    - カーネル空間の処理の呼び出し
- VM(仮想メモリ)
    - Paging
- File System
    - I/O, Read, Write
- Scheduler など

---

# カーネル空間
- OS の中核となるプログラムで Meta Level に相当する
- Xv6 ではカーネルとユーザープログラムは分離されている
- ユーザープログラムはカーネルに直接アクセスできない。
    - ユーザープログラムによる書き換えやアクセスを防ぐため
    - 呼び出す場合は system call

---

# Paging
- Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理
- 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる

---

# Xv6の書き換え方針
- メタレベルからノーマルレベルを保証するOSを作りたい
- 段階的に書き換えていきたい
- Paging を書き換える理由
    - OS の信頼性を保証する上で重要なメモリ管理部分

- __code で書き直していく

---

# インターフェースの導入
- ノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入
- インターフェースによるメリット
    - 煩雑な記述の解消
    - 入力の切り替えによる実装の入れ替え
- 実装は別で定義し、呼び出す
    - 後ほど説明

---

# CbCインターフェース
- Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する **Meta Data Gear**
- インターフェースを定義してそこから呼び出す

---

# インターフェースの定義
- Xv6 の Virtual Memory の API 部分のインターフェース
- 以下のコードについて説明していく

``` 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(...));

```

---


# インターフェースの命名(1行目)
- typedef struct の直後にインターフェース名(vm)を書く

``` c
typedef struct vm<Type,Impl> {
```

---


# インターフェースの Code Gear(2行目~)
- vm で使う Code Gear を登録する
- Code Gear は __code CodeGear名(引数); で記述する
    - 引数が Data Gear に相当する
- 第1引数の Impl* vm がインターフェースの実装の型になる


``` 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(...));

```

---

# next(...)
- __code next(...) は次の Code Gear の継続先
- それぞれの Code Gear の引数の1つに設定する
``` c
    __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...));
//....
    __code next(...);
} vm;
```
- 例) goto vm->kpt_freerange の引数に exit を設定すると Code Gear である exit に遷移する
``` c
__code exit(){
//....
}

goto vm->kpt_freerange(vm, low, hi, exit);
```

---

# Interface の実装の型
- 実装側のヘッダーファイルも 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(...));
```


---

# インターフェースの実装
- 実装は型と実装をそれぞれ別ファイルで定義する(vm_impl.h と vm_impl.cbc)
- 実装するインターフェースは #interface で宣言する

``` c
#interface "vm.h"
```

---

# 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;
```


- 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;

    goto next(...);
}
```

--- 

# インターフェース実装内の CbC
- for文やif文がある場合はさらに実装を分ける
    - 状態遷移ベースで記述したい
- インターフェースは外から呼び出されるAPI
- それに対してインターフェースの実装の Code Gearから明示的に呼び出される Code Gearは、Java の private メソッドのように扱われる。
- 実際に vm.c の loaduvm の実装を分けた記述を説明する

---

![](https://i.imgur.com/Cj87Pxu.png)

---
# 実装内の明示的な遷移の処理
- **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(...));
}
```

- 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;
....
    vm->loaduvm = C_loaduvmvm_impl;
....
}
```
---

# loaduvmの CbCによる書き換え
- loaduvmは
    - swapから呼び出す
    - kernelの中をloopしてreadiに入る
    - 入った場合は待ちになる
    - user proc側が待ちになる

- 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;
}
```

- loaduvm_impl がインターフェースから呼ばれる実装


``` 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(...));
}
```
- loaduvm_impl から private な Code Gear が呼ばれる

``` c
#interface "vm_impl.h"

__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(...));
}
```


- 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 を用意して実装する

![](https://i.imgur.com/ByA7GVJ.png)

```c
__code loaduvm_loopvm_impl(struct vm_impl* vm_impl, __code next(...)) {
    uint i = vm_impl->i;
    uint sz = vm_impl->sz;

    if (i < sz) {
        goto loaduvm_check_pgdir(vm_impl, next(ret, ...));
    }

    goto loaduvm_exit(vm_impl, next(...));
}


__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;
    char* addr = vm_impl->addr;
    uint pa = vm_impl->pa;

    if ((pte = walkpgdir(pgdir, addr + i, 0)) == 0) {
        // goto panic
    }
    pa = PTE_ADDR(*pte);

    vm_impl->pte = pte;
    vm_impl->pgdir = pgdir;
    vm_impl->addr = addr;
    vm_impl->pa = pa;

    goto loaduvm_check_PTE_SZ(vm_impl, next(...));
}

__code loaduvm_check_PTE_SZ(struct vm_impl* vm_impl, __code next(int ret, ...)) {
    if (sz - i < PTE_SZ) {
        n = sz - i;
    } else {
        n = PTE_SZ;
    }

    if (readi(ip, p2v(pa), offset + i, n) != n) {
        ret = -1;
        goto next(ret, ...);
    }

    vm_impl->n = n;

    goto loaduvm_loopvm_impl(vm_impl, next(ret, ...));
}

__code loaduvm_exit(struct vm_impl* vm_impl, __code next(int ret, ...)) {
    ret = 0;
    goto next(ret, ...);
}
```


---

# C を CbC に部分的に書き直す手法
- CbC の場合 goto による 遷移を行うので、関数呼び出しのように goto 以降のコードを実行できない
- 例) goto すると戻ってこれないため それ以降が実行されなくなる。

---

# CbC から C への遷移
- 最初の命令は next で戻ってこれるので、dummy の関数を用意してそこで実行する

``` c
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);

    struct vm* vm = createvm_impl(cbc_context);
    // goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret);
        Gearef(cbc_context, vm)->vm = (union Data*) vm;
        Gearef(cbc_context, vm)->pgdir = pgdir;
        Gearef(cbc_context, vm)->init = init;
        Gearef(cbc_context, vm)->sz = sz ;
        Gearef(cbc_context, vm)->next = C_vm_void_ret ;
    goto meta(cbc_context, vm->init_inituvm);
}

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?");
    }

    cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);

```

---

# まとめ
- OS 内部で CbC インターフェースを扱えるようになった
- CbC の書 き換えが完了すれば、継続の入力と出力を検査することで OS の信頼性を保証したり、インターフェースの実装の入れ替えが可能になる。
- Context による複数環境の入れ替えや同時実行を可能にすることで CbCXv6 に おいて コンテナと VM を実装ができると予想される。