並列信頼研
桃原優

# 概要

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名で定義

# Data Gear の継続

Code Gear からアクセスできるデータ
input Data Gear と Output Data Gear で証明する

# メタレベル

# Meta Code Gear

メタレベルで見ると Code Gear の間にメタレベルの処理が挟まっている
cmake で __code CodeGear名_stub が生成される

# Meta Data Gear

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

# Context

Meta Data Gear
Contextには全てのData Gear と Code Gear が登録されている
ユーザープロセスに対応して1つのcontextが存在する
将来的なVMやコンテナの実装はContextの切り替えるによる実装を目指している
Code Gear は Context 内の Data Gear の関数ポインタを持っていてそこにアクセスする
stub Code Gear でOutput Data Gear のポインタを参照してそこに書き出す

# 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 部分のインターフェース
以下のコードについて説明していく

1
2
3
4
5
6
7
8


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)を書く

1

typedef struct vm<Type,Impl> {

# インターフェースの Code Gear(2行目~)

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

1
2
3
4
5
6
7
8


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つに設定する

1
2
3
4


    __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...));
//....
    __code next(...);
} vm;

例) goto vm->kpt_freerange の引数に exit を設定すると Code Gear である exit に遷移する

1
2
3
4
5


__code exit(){
//....
}

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

# Interface の実装の型

実装側のヘッダーファイルも vm_impl と同じように用意する

1
2
3
4


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 で宣言する

1

#interface "vm.h"

# vmインターフェースの実装の初期化

定義が終わったのでインターフェースを使用したい
メモリ上にインターフェースの置き場所と実装を確保
- struct vm* vm = new vm();
インターフェースと実装の紐付け
- vm->void_ret = C_vm_void_ret;
  - Code Gear の enum の設定
  - インターフェースのAPIと enum の番号を紐付けている

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


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 と対応する

1
2
3
4
5
6


__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 の実装を分けた記述を説明する

# 実装内の明示的な遷移の処理

vm と同じ create_impl 内で vm_impl を定義し、private で実装する Code Gear を定義する
loaduvmvm_impl で goto によって private に遷移する

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


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 で書き換える

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29


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 がインターフェースから呼ばれる実装

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


__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 が呼ばれる

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


#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 で書き直す

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30



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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53


__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 の関数を用意してそこで実行する

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29


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 を実装ができると予想される。

CbCインターフェースによる CbCXv6 の書き換え

CbCインターフェースによる CbCXv6 の書き換え

# 概要

# OS の信頼性を上げたい

# ノーマルレベルとメタレベル

# Continuation based C

# ノーマルレベル

# Code Gear による継続

# Data Gear の継続

# メタレベル

# Meta Code Gear

# Meta Data Gear

# Context

# Xv6

# Xv6の構成

# カーネル空間

# Paging

# Xv6の書き換え方針

# インターフェースの導入

# CbCインターフェース

# インターフェースの定義

# インターフェースの命名(1行目)

# インターフェースの Code Gear(2行目~)

# next(…)

# Interface の実装の型

# インターフェースの実装

# vmインターフェースの実装の初期化

# インターフェース実装内の CbC

# 実装内の明示的な遷移の処理

# loaduvmの CbCによる書き換え

# C を CbC に部分的に書き直す手法

# CbC から C への遷移

# まとめ