# アプリケーションの信頼性
アプリケーションの信頼性を向上させるためには、 土台となるOS自体の信頼性が高く保証されていなければならない。
OSそのものも巨大なプログラムであるため、テストコードを用いた方法で信頼性を確保する事が可能である。
しかし並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。
テスト以外の方法でOSの信頼性を高めたい。

そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、定理証明支援系Agda\cite{agda}を利用した証明ベースでの信頼性の確保などの手法が考えられる。\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}
形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。\cite{hyperKernel}
OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。
実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。

OS上のアプリケーションには本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理がある。
前者をノーマルレベルの計算と呼び、後者をメタ計算と呼ぶ。
OSはメタ計算を担当していると言える。
実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが
検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。
ノーマルレベル上でのバグを例えばモデル検査のようなメタ計算によって発見し信頼性を向上させたい。

ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
CbCは基本`goto`で`CodeGaar`というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と
呼ばれる隠れた状態を持たない。このため、計算のための情報は`CodeGear`の入力にすべてそろっている。
そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。
メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。
CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
CbCは`GCC`\cite{gcc}\cite{weko_82695_1}あるいは`LLVM`\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。

現在小さなunixであるxv6 kernelをCbCを用いて書き換えている。
書き換えの為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。


# Continuation Based C

Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。
CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。
この継続はSchemeなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。
またCbCではこの軽量継続を用いて\texttt{for}文などのループ文を実装する。これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。
実際、Agda よる関数型のCbCの記述も用意されている\cite{}。
実際のOSやアプリケーションを記述する場合には
GCC及びLLVM/clang上のCbC実装を用いる。

CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。
各CodeGearはDataGearと呼ばれるデータの単位で入力を受け取り、 その結果を別のDataGearに書き込む。
入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。
CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。
これらの関係図を図\ref{fig:cgdg}に示す。

![lab:fig:cgdg, cap:CodeGearと入出力の関係図](fig/cgdg.pdf)

CbCを利用したシステムコールのディスパッチ部分をCode \ref{src:cbc_example}に示す。
この例題では特定のシステムコールの場合、 CbCで実装された処理に`goto`文をつかって継続する。
例題ではCodeGearへのアドレスが配列`cbccodes`に格納されている。
引数として渡している`cbc_ret`は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。
実際に`cbc_ret`に継続が行われるのは、 `read`などのシステムコールの一連の処理の継続が終わったタイミングである。

``` lab:src:cbc_example, cap:CbCを利用したシステムコールのディスパッチ
void syscall(void)
{
    int num;
    int ret;

    if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
        proc->cbc_arg.cbc_console_arg.num = num;
        goto (cbccodes[num])(cbc_ret);
    }
```

Code\ref{src:cbc_example}の状態遷移図を図\ref{fig:dispatch}に示す。
図中の`cbc_read`などは、 `read`システムコールを実装しているCodeGearの集合である。

![lab:fig:dispatch, cap:CbCを利用したシステムコールディスパッチの状態遷移](fig/syscall_dispatch.pdf)

CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す`void`型などの関数を経由することで呼び出しが可能となる。

この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。
これはGCCでは内部コードを生成、 LLVM/clangでは`setjmp`と`longjmp`を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。
したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。

# CbCを用いたOSの実装

軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。\cite{gears}
現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。

GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。
また、 対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。
MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、 現在はPerlスクリプトによってGearsOSのビルド時に生成される。
CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。

![lab:meta-cg-dg, cap:CodeGearとMetaCodeGear](./fig/meta-cg-dg.pdf)

通常のコード中では入力のDataGearを受け取りCodeGearを実行、 結果をDataGearに書き込んだ上で別のCodeGearに継続する様に見える。
この流れを図\ref{meta-cg-dg}の上段に示す。
しかし実際はCodeGearの実行の前後に実行されるMetaCodeGearや入出力のDataGearをMetaDataGearから取り出すなどのメタ計算が加わる。
これは図\ref{meta-cg-dg}の下段に対応する。

遷移先のCodeGearとMetaCodeGearの紐付けや、 計算に必要なDataGearを保存や管理を行うMetaDataGearとして`context`がある。
contextは処理に必要なCodeGearの番号とMetaCodeGearの対応表や、 DataGearの格納場所を持つ。
計算に必要なデータ構造と処理を持つデータ構造であることから、 contextは従来のOSのプロセスに相当するものと言える。
cotnextと各データ構造の関わりを図\ref{fig:context_ref}に示す。
![lab:fig:context_ref, cap:Contextと各データの関係図](fig/Context_ref.pdf)

コード上では別のCodeGearに直接遷移している様に見えるが、 実際はcontext内の遷移先のCodeGearに対応するスロットから、対応するMetaCodeGearに遷移する。
MetaCodeGear中で、次に実行するCodeGearで必要なDataGearをcontextから取り出し、 実際の計算が行われる。


# xv6 kernel

xv6とはマサチューセッツ工科大学でv6 OS\cite{lions1996lions}を元に開発された教育用のUNIX OSである。\cite{xv6}
xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
Raspberry Pi\cite{rpi}上での動作を目的としたARMアーキテクチャのバージョンも存在する。\cite{xv6rpi}
本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。

xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。
またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。

本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。
xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。

本論文ではxv6の継続の分析をシステムコール部分とファイルシステム、 仮想メモリなどのOSの根幹部分でそれぞれ行った。


# xv6のシステムコールの継続の分析と書き換え
xv6の処理を継続を中心とした記述で書き換えを行う。
この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。

まずxv6の`read` システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 \cite{weko_195888_1}
分析結果をCbCのCodeGearに変換し、 状態遷移図におこしたものを図\ref{fig:cbc_readsyscall}に示す。

![lab:fig:cbc_readsyscall, cap:readシステムコールの状態遷移](fig/readsyscall.pdf)

CbCで書き換えた`read`システムコールは、 xv6の`read`システムコールのディスパッチ部分から、 `cbc_read`CodeGearに`goto`文で軽量継続される。
継続後はreadする対象によって`cbc_readi`や、 `cbc_consoleread`などに状態が変化していく。
各CodeGearの遷移時にはDataGearがやり取りされる。
DataGearはxv6のプロセス構造体に埋め込まれたcontextを経由してCodeGearに渡される。

この実装の利点として、 CodeGearの命名と状態が対応しており、 状態遷移図などに落としても自然言語で説明が可能となる点が挙げられる。
しかし実際には`cbc_readi`の状態はさらに複数のCodeGearに分離しており、 実際に`read`システムコールを実装するCodeGearの数は図の状態より多い。
この事から、 複数のCodeGearを1つにまとめた上で見た状態と、 各CodeGearそれぞれの状態の2種類の状態があるといえる。

複数のCodeGearをまとめた状態は、 抽象化したAPIの操作時におけるアルゴリズム上の問題が無いかの確認として使用出来る。
対して各CodeGearそれぞれはモデル検査や、 特定の関数の中の処理が適しているかどうかの検査として見ることが出来ると考えられる。

この事からGearsOSでは、 各CodeGearのモジュール化の仕組みであるInterface機能を導入している。
Interfaceの導入によってCodeGearを定義することで状態数を増やしても、 抽象化されたAPIを利用することで細部の状態まで意識する必要が無くなった。
xv6の処理をCbCで書き換える際には、 対象の継続のAPIをまず決定しモジュール化を図る必要がある。

# xv6のシステムコール以外の継続の分析
xv6はシステムコール以外に、 ファイルシステムの操作やページテーブルの管理などの処理も存在している。
これらはOSの立ち上げ時やシステムコールの中で、ファイルシステムの操作に対応した関数や構造体などのAPIを通して操作される。
システムコールの一連の流れに着目するのではなく、 特定の対象のAPIに着目して継続の分析を検討した。

xv6のファイルシステムに関する関数などのAPIは主に`fs.c`中に記述されている。
APIの内部をCodeGearに分割をすると、 APIを呼び出す時点でAPI細部の継続を考慮する必要がある。
細部の継続を隠蔽するために、 抽象的に複数のCodeGearをまとめる機能であるInterfaceを導入したい。
Code\ref{src:fs_interface}に示す様に、 `fs.c`中に定義されているAPIを抜き出し、 CbCのInterfaceとして定義した。
`__code`から始まるCodeGearの名前が、 それぞれ抽象化されたCodeGearの集合の最初の継続となる。


``` lab:src:fs_interface, cap:ファイルシステム操作のAPIの一部
typedef struct fs<Type,Impl> {
    __code readsb(Impl* fs, uint dev, struct superblock* sb, __code next(...));
    __code iinit(Impl* fs, __code next(...));
    __code ialloc(Impl* fs, uint dev, short type, __code next(...));
    __code iupdate(Impl* fs, struct inode* ip, __code next(...));
    __code idup(Impl* fs, struct inode* ip, __code next(...));
    __code ilock(Impl* fs, struct inode* ip, __code next(...));
    __code iunlock(Impl* fs, struct inode* ip, __code next(...));
    __code iput(Impl* fs, struct inode* ip, __code next(...));
....
} fs;
```

Code\ref{src:fs_interface}内の `readsb`などは`fs.c`内で定義されているCの関数名と対応している。
このCの関数を更に継続ごと分割するために、 関数内のif文などの分岐を持たない基本単位であるBasic Blockに着目した。

CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。
したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearへ変換することが可能となる。
実際にBasicBlock単位で切り分ける前の処理と、切り分けたあとの処理の一部を示す。
例としてinodeのアロケーションを行うAPIでる`ialloc`の元のコードをCode\ref{src:ialloc_origin}に示す。

``` lab:src:ialloc_origin, cap:iallocの元のソースコード
struct inode* ialloc (uint dev, short type)
{
    readsb(dev, &sb);
    for (inum = 1; inum < sb.ninodes; inum++) {
        bp = bread(dev, IBLOCK(inum));
        dip = (struct dinode*) bp->data + inum % IPB;

        if (dip->type == 0) {  // a free inode
            memset(dip, 0, sizeof(*dip));
            ...
            return iget(dev, inum);
        }
        brelse(bp);
    }
    panic("ialloc: no inodes");
}
```

 `ialloc`はループ条件である `inum < sb.ninodes`が成立しなかった場合は`panic`へと状態が遷移する。
 この`for`文での状態遷移をCodeGearに変換したものをCode\ref{src:allocinode_loopcheck}に示す。


``` lab:src:allocinode_loopcheck, cap:ループ条件を確認するCodeGear
__code allocinode_loopcheck(struct fs_impl* fs_impl, uint inum, uint dev, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(...)){
    if( inum < sb->ninodes){
        goto allocinode_loop(fs_impl, inum, dev, type, sb, bp, dip, next(...));
    }
    char* msg = "failed allocinode...";
    struct Err* err = createKernelError(&proc->cbc_context);
    goto err->panic(msg);
}
```

Code\ref{src:allocinode_loopcheck}ではループ条件の成立を`if`文で確認し、ループ処理に移行する場合は `allocinode_loop`へ遷移する。
`goto`文の中の引数の1つ`next(...)` は、 APIとして呼び出した`ialloc`の次の継続のCodeGearに対して、 `context`などの環境を渡す構文である。
ループ条件が満たされなかった場合は、 コンテキストから`panic`に関するCodeGearの集合を取り出し、 集合中の`panic` CodeGearへと遷移する。
オリジナルの処理では、 ループ中に`dip->type == 0`が満たされた場合は関数から`return`文により関数から復帰する。
CodeGearではCode\ref{src:alloc_loop}内で、 状態が分けられる。
この先の継続は、　復帰用のCodeGearかループの先頭である`allocinode_loopcheck`に再帰的に遷移するかになる。

``` lab:src:alloc_loop, cap:ループ中に復帰するかどうかの確認をするCodeGear
__code allocinode_loop(struct fs_impl* fs_impl, uint inum, uint dev, short type, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(...)){
    bp = bread(dev, IBLOCK(inum));
    dip = (struct dinode*) bp->data + inum % IPB;
    if(dip->type = 0){
        goto allocinode_loopexit(fs_impl, inum, dev, sb, bp, dip, next(...));
    }

    brelse(bp);
    inum++;
    goto allocinode_loopcheck(fs_impl, inum, dev, type, sb, bp, dip, next(...));
}
```
 
この継続の分析方法の利点として、 既存のコードのBasic Block単位でCodeGearに変換可能であるため機械的にCodeGearへの変更が可能となる。
既存の関数上のアルゴリズムや処理に殆ど変更がなく変更可能であるために、 CodeGearで細分化して表現することは容易となる。

現在は従来のxv6の関数呼び出しを元にしたAPIの中でCodeGearに分割している。
このために既存のAPI内の処理の細分化は可能とはなったが、 APIそのものをCodeGearを用いた継続に適した形には表現できていない。
APIの内部のCodeGearはあくまでBasic Block単位に基づいているために、 状態遷移図で表現した際に自然言語で表現できないCodeGearも存在してしまう。

さらに、 `for`ループをCodeGearに分割することを考えるとループ中にループのindexを利用している場合は、 そのindexも次の継続に渡さなければならない。
このためindexを使用していないCodeGearでも継続の引数としてindexを受け取り、 実際にindexを利用するCodeGearに伝搬させる必要がある。
これらの問題を解決する為には、 APIを分割したCodeGearそれぞれのDataGearに型を与え、 どの継続でDataGearの意味が変わるかを追求する必要がある。
APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した1つの巨大な構造体に隠蔽されている。
巨大な構造体で管理するのではなく、 構造体で次のCodeGearの状態に影響を与える要素を適宜組み合わせたDataGearを作る必要がある。


# CbCを用いた部分的なxv6の書き換え

CbCではCodeGear、 DataGearからなる単位を基本とし、 それぞれにメタなGearが付随する。
また実行に必要なCodeGearとDataGearをまとめたcontextというMetaDataGearが存在する。
この機能を元にxv6の書き換えを検討した。

xv6内でCbCの軽量継続に突入する際は、 元の処理関数に通常の方法では戻ってくることができず、部分的に書き換えていくのが困難である。
今回は呼び出し関数に戻れるスタックフレームを操作したい為に、 ダミーの`void`関数を用意した。
この関数内でCodeGearに`goto`文を用いて遷移することで、 CbCから帯域脱出した際に`void`関数の呼び出し元から処理を継続し、部分的にCbCに書き換えることが可能となった。
Code\ref{src:dumy_function_cbc}では、 `userinit`関数へ戻るために、 `cbc_init_vmm_dumy`を経由している。

``` lab:src:dumy_function_cbc, cap:部分的にCbCを適応する例
void cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz)
{
    struct vm* vm = createvm_impl(cbc_context);
    goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret);
}

void userinit(void)
{
...

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

    p->sz = PTE_SZ;
    memset(p->tf, 0, sizeof(*p->tf));
...
}
```

Code\ref{src:dumy_function_cbc}中で、 CodeGearへの遷移が行われる`goto vm->init_vmm()`の`vm->void_ret`は`init_vmm`の次の継続のCodeGear名である。
この`vm->void_ret`は`return`するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。


# xv6の今後の書き換え

xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。
グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。
グローバル変数を極力使わず継続を中心とした実装を行いたい。

contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。

現状はxv6の全ての機能をまだCbCを用いて書き換えていない。
ファイルシステムや仮想メモリにまつわる処理などはAPI単位では書き換えているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。
そのためにOSそのものを状態遷移単位で完全に書き直す必要が存在し、 そのためには全ての処理に対して状態を定義していく必要がある。

またOS上でDataGearとCodeGearの位置づけを明確に定義する必要も存在する。
DataGearの依存関係やCodeGearの並列実行など、 プロセスベースで実装していた処理をCodeGearなどで意味がある形式にする必要がある。

# まとめ

本稿ではxv6を継続を用いた単位での書き換えを検討し、 実際にいくつかの処理を書き換えた。
書き換えはシステムコールに着目しCodeGearへ分割する手法と、 BasicBlockごとにCodeGearへ分割する手法で行った。
現状はまだxv6の実装を利用した証明や、 xv6にモデル検査機能の実装を行いたい。
またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。