title: 継続を用いたxv6 kernelの書き換え
author: Takahiro Sakamoto, Yu Tobaru, Shinji Kono

profile: 琉球大学工学部情報工学科並列信頼研

## 研究目的
* 現代の OS では拡張性と信頼性を両立させることが要求されている
* 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である
* ノーマルレベルの計算とメタレベルの計算を切り離して記述するために Code Gear と Data Gear という単位を用いている
* Gears OS は Continuation based C(CbC) によってアプリケーションと OS そのものを記述する
* 本研究では、CbC を用いた Gears OS の実装の前段階として xv6 での実装を目標とする

## メタ計算とは
* プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理やスレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する
* これらの計算をメタ計算と呼ぶ
* メタ計算はノーマルレベルの計算から切り離して記述したい
* そのためには処理を細かく分割する必要があるが、関数やクラスなどの単位は容易に分割できない
* そこで当研究室ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を提案している

## Continuatuin based C
* Continuation based C (CbC) はこの Code Gear 処理の単位としてプログラミング言語として開発している。
* Code Gear は 関数呼び出し時の環境を使わずに次の Code Gear へと goto 文によって遷移する
* この goto 文による遷移を軽量継続と呼ぶ。
* 継続を用いることによって状態遷移ベースでのプログラミングが可能である
* CbC は C と互換性のある言語なので、C の関数も呼び出すことができる

## CbC のコード例
* CbC では Code Gear は *__code* Code Gear 名 (引数) の形で記述される
* Code Gear は戻り値を持たないので、関数とは異なり return 文は存在しない
* goto の後に Code Gear 名と引数を並べて、次の Code Gear の遷移を記述する

## CbC のコード例
* この goto の行き先を継続と呼び、このときの a+b が次の Code Gear への出力となる

```
__code cg0(int a, int b){
  goto cg1(a+b);
}

__code cg1(int c){
  goto cg2(c);
}
```

## CbC の継続
* Code Gear の継続を表す図である
* Code Gear 間の遷移は goto によって行われる
<!--* アセンブラレベルで見ると call ではなく jmp となっている-->

<div style="text-align: center;">
　<img src="./images/cbc_goto.svg" alt="normalCodeGear" width="600">
</div>

## Gears におけるメタ計算
* Gears OS ではメタ計算を Meta Code Gear、Meta Data Gear で表現する
* Meta Code Gear はノーマルレベルの Code Gear の直後に遷移され、メタ計算を実行する
* Meta Code Gear で OS の機能であるメモリ管理やスレッド管理を行う

<div style="text-align: center;">
　<img src="./images/meta_Code_Gear.svg" alt="normalCodeGear" width="600">
</div>

## Meta Gear
* Gears OS では、Meta Code Gear は通常の Code Gear の直前、直後に挿入され、メタ計算を実行する
* 通常の計算からはメタ計算は見ることができない
<div style="text-align: center;">
　<img src="./images/meta_gear2.svg" alt="MetaGear" width="600">
</div>


<!--## Context
* Gears OS では Context と呼ばれる、使用されるすべての Code Gear、Data Gear を持つ Meta Data Gear を持っている
* Gears OS は必要な Code Gear、Data Gear を参照したい場合、この Context を通す必要がある
* Context は Meta Data Gear であるため、Meta Code Gear を介してアクセスする
-->

## Interface
* Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される
* Interface は使用される Data Gear の定義と、それに対する Code Gear の集合である
* Interface の操作に対応する Code Gear の引数は Interface に定義されている Data Gear を通して行われる

## xv6-rpi の CbC 対応
* オリジナルの xv6 は x86 アーキテクチャで実装されたものだが、xv6-rpi は Raspberry Pi 用に実装されたものである
* xv6-rpi を CbC で書き換えるために、GCC 上で実装した CbC コンパイラを ARM 向けに build し xv6-rpi をコンパイルした
* これにより、xv6-rpi を CbC で書き換える ことができるようになった

## xv6 の CbC への書き換え
* xv6 は UNIX V6 を x86 向けに再実装した OS である
* プロセスや仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなどの基本的な Unix の構造を持つ
* CbC は Code Gear 間の遷移が goto による継続で行われるため、状態遷移ベースでのプログラミングに適している
* CbC で xv6 を書き換えることにより、状態遷移モデルによるモデル検査が可能となることを期待する

## xv6 の書き換えの方針
* xv6 を CbC で書き換え、Gears OS の機能と置き換えることで Gears OS に OS の基本構造を持たせたい
* このためには xv6 をモジュール化することで、xv6 の機能を明らかにする必要がある
* xv6 の Interface を定義し、Gears OS の機能をこれに合わせることによって実現したい

## CbC によるシステムコールの書き換え
* CbC は C と互換性のある言語であるため、元のソースコードから大きく崩すことなく必要な機能のみを CbC へと書き換えることが可能である
* ここでは実際にシステムコールを CbC で書き換えることによって、状態遷移ベースで書き換えるには何が必要か示すことにした
* 今回は read システムコールの CbC 書き換えを行なった

## syscall関数
* syscall 関数 はシステムコールを呼び出す関数である
```
void syscall(void)
{
    int num;
    int ret;
    num = proc->tf->r0;
    if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
        proc->cbc_arg.cbc_console_arg.num = num;
        goto (cbccodes[num])(cbc_ret);
    }
    if((num > 0) && (num <= NELEM(syscalls)) && syscalls[num]) {
        ret = syscalls[num]();
        if (num != SYS_exec) {
            proc->tf->r0 = ret;
        }
    } else {
        cprintf("%d %s: unknown sys call %d\n", proc->pid, proc->name, num);
        proc->tf->r0 = -1;
    }
}
```

## sys\_read 関数
* 読み込むファイルの情報とアドレスを取り出し、fileread に渡している
```
int sys_read(void)
{   
    struct file *f;
    int n;
    char *p;

    if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
        return -1;
    }

    return fileread(f, p, n);
}
```

## cbc\_read
```
__code cbc_read(__code (*next)(int ret)){
    struct file *f;
    int n;
    char *p;

    if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
        goto next(-1);
    }
    goto cbc_fileread(f, p, n, next);
}
```

## fileread
* file の状態を確認し、対応した関数へ移行する
```
int fileread (struct file *f, char *addr, int n)
{
    int r;

    if (f->readable == 0) {
        return -1;
    }

    if (f->type == FD_PIPE) {
        return piperead(f->pipe, addr, n);
    }

    if (f->type == FD_INODE) {
        ilock(f->ip);

        if ((r = readi(f->ip, addr, f->off, n)) > 0) {
            f->off += r;
        }

        iunlock(f->ip);

        return r;
    }

    panic("fileread");
}
```

## cbc\_fileread
```
__code cbc_fileread1 (int r)
{   
    struct file *f = proc->cbc_arg.cbc_console_arg.f;
    __code (*next)(int ret) = cbc_ret;
    if (r > 0)
        f->off += r;
    iunlock(f->ip);
    goto next(r);
}

__code cbc_fileread (struct file *f, char *addr, int n, __code (*next)(int ret))
{
    if (f->readable == 0) {
        goto next(-1);
    }

    if (f->type == FD_PIPE) {
        //goto cbc_piperead(f->pipe, addr, n, next);
        goto next(-1);
    }

    if (f->type == FD_INODE) {
        ilock(f->ip);
        proc->cbc_arg.cbc_console_arg.f = f;
        goto cbc_readi(f->ip, addr, f->off, n, cbc_fileread1);
    }

    goto cbc_panic("fileread");
}
```

## readi
* readi はファイルシステム上か特殊なデバイスを制御するかどうかで分岐する
* ここでは consoleread へ向かう処理を確認する
```
int readi (struct inode *ip, char *dst, uint off, uint n)
{
    uint tot, m;
    struct buf *bp;

    if (ip->type == T_DEV) {
        if (ip->major < 0 || ip->major >= NDEV || !devsw[ip->major].read) {
            return -1;
        }

        return devsw[ip->major].read(ip, dst, n);
    }
...
```

## cbc\_readi
```
__code cbc_readi (struct inode *ip, char *dst, uint off, uint n, __code (*next)(int ret))
{   
    uint tot, m;
    struct buf *bp;

    if (ip->type == T_DEV) {
        if (ip->major < 0 || ip->major >= NDEV || !cbc_devsw[ip->major].read) {
            goto next(-1);
        }

        goto cbc_devsw[ip->major].read(ip, dst, n, next);
    }
...
```

## consoleread
* console への入力を読み込み、待っている間スリープする
```
int consoleread (struct inode *ip, char *dst, int n)
{
    uint target;
    int c;
    iunlock(ip);
    target = n;
    acquire(&input.lock);

    while (n > 0) {
        while (input.r == input.w) {
            if (proc->killed) {
                release(&input.lock);
                ilock(ip);
                return -1;
            }
            sleep(&input.r, &input.lock);
        }
        c = input.buf[input.r++ % INPUT_BUF];
        if (c == C('D')) {  // EOF
            if (n < target) {
                input.r--;
            }
            break;
        }
        *dst++ = c;
        --n;
        if (c == '\n') {
            break;
        }
    }
    release(&input.lock);
    ilock(ip);
    return target - n;
}
```

## cbc\_consoleread

```
__code cbc_consoleread (struct inode *ip, char *dst, int n, __code(*next)(int ret))
{   
    uint target;

    iunlock(ip);

    target = n;
    acquire(&input.lock);

    if (n > 0) {
        proc->cbc_arg.cbc_console_arg.n = n;
        proc->cbc_arg.cbc_console_arg.target = target;
        proc->cbc_arg.cbc_console_arg.dst = dst;
        proc->cbc_arg.cbc_console_arg.ip = ip;
        proc->cbc_arg.cbc_console_arg.next = next;
        goto cbc_consoleread2();
    }
    goto cbc_consoleread1();
}
```

## cbc\_consoleread
```
__code cbc_consoleread2 ()
{   
    struct inode *ip = proc->cbc_arg.cbc_console_arg.ip;
    __code(*next)(int ret) = proc->cbc_arg.cbc_console_arg.next;
    if (input.r == input.w) {
        if (proc->killed) {
            release(&input.lock);
            ilock(ip);
            goto next(-1);
        }
       goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2);
    }
    goto cbc_consoleread1();
}

__code cbc_consoleread1 ()
{   
    int cont = 1;
    int n = proc->cbc_arg.cbc_console_arg.n;
    int target = proc->cbc_arg.cbc_console_arg.target;
    char* dst = proc->cbc_arg.cbc_console_arg.dst;
    struct inode *ip = proc->cbc_arg.cbc_console_arg.ip;
    __code(*next)(int ret) = proc->cbc_arg.cbc_console_arg.next;

    int c = input.buf[input.r++ % INPUT_BUF];

    if (c == C('D')) {  // EOF
        if (n < target) {
            input.r--;
        }
        cont = 0;
    }

    *dst++ = c;
    --n;
    if (c == '\n') {
        cont = 0;
    }
    if (cont == 1) {
        if (n > 0) {
            proc->cbc_arg.cbc_console_arg.n = n;
            proc->cbc_arg.cbc_console_arg.target = target;
            proc->cbc_arg.cbc_console_arg.dst = dst;
            proc->cbc_arg.cbc_console_arg.ip = ip;
            proc->cbc_arg.cbc_console_arg.next = next;
            goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2);
        }
    }
    release(&input.lock);
    ilock(ip);
    goto next(target - n);
}
```
## sleep
* プロセスをスリープ状態にしてスケジューラーへ引き渡す
```
void sleep(void *chan, struct spinlock *lk)
{
    if(proc == 0) {
        panic("sleep");
    }

    if(lk == 0) {
        panic("sleep without lk");
    }

    if(lk != &ptable.lock){  //DOC: sleeplock0
        acquire(&ptable.lock);  //DOC: sleeplock1
        release(lk);
    }

    proc->chan = chan;
    proc->state = SLEEPING;
    sched();

    proc->chan = 0;

    if(lk != &ptable.lock){  //DOC: sleeplock2
        release(&ptable.lock);
        acquire(lk);
    }
}
```

## cbc\_sleep
```
__code cbc_sleep1()
{   
    struct spinlock *lk = proc->lk;
    proc->chan = 0;

    if(lk != &ptable.lock){  //DOC: sleeplock2
        release(&ptable.lock);
        acquire(lk);
    }
    goto proc->cbc_next();
}

__code cbc_sleep(void *chan, struct spinlock *lk, __code(*next1)())
{   
    if(proc == 0) {
        panic("sleep");
    }

    if(lk == 0) {
        panic("sleep without lk");
    }

    if(lk != &ptable.lock){  //DOC: sleeplock0
        acquire(&ptable.lock);  //DOC: sleeplock1
        release(lk);
    }
    proc->chan = chan;
    proc->state = SLEEPING;
    proc->lk = lk;
    proc->cbc_next = next1;

    goto cbc_sched(cbc_sleep1);
}
```

## sched
* レジスタの値を切り替えて、スケジューラーへと戻る
* 再開時は swtch の下から再開する
```
void sched(void)
{   
    int intena;

    if(!holding(&ptable.lock)) {
        panic("sched ptable.lock");
    }

    if(cpu->ncli != 1) {
        panic("sched locks");
    }

    if(proc->state == RUNNING) {
        panic("sched running");
    }

    if(int_enabled ()) {
        panic("sched interruptible");
    }

    intena = cpu->intena;
    swtch(&proc->context, cpu->scheduler);
    cpu->intena = intena;
}
```

## cbc\_sched
```
__code cbc_sched(__code(*next)())
{   
    int intena;

    if(!holding(&ptable.lock)) {
        panic("sched ptable.lock");
    }

    if(cpu->ncli != 1) {
        panic("sched locks");
    }

    if(proc->state == RUNNING) {
        panic("sched running");
    }

    if(int_enabled ()) {
        panic("sched interruptible");
    }

    intena = cpu->intena;
    swtch(&proc->context, cpu->scheduler);
    cpu->intena = intena;

    goto next();
}
```
<!-- コメントアウトのやり方-->
## まとめと今後の方針
* 現在は xv6 のシステムコールの一部のみの書き換えと、設計のみしか行っていないのでカーネル全ての書き換えをおこなう
* Gears OS にはメタ計算を実装する context は par goto の機能がある
* これらの機能を xv6 に組み込む方法について考察する必要がある
* xv6-rpi は QEMU のみの動作でしか確認してないため、実機上での動作が可能なように実装する必要がある