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

数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
これに適した形として、 状態遷移モデルが挙げられる。
OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。
しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。
実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。

さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。
本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。
ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。
プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。

ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。

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



# Continuation Based C

Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。
CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに`jmp`命令で移動する継続が導入されている。
この継続はSchemeなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。
またCbCではこの軽量継続を用いた再帰呼び出しを利用することで`for`文などのループ文を廃し、 関数型プログラミングに近いスタイルでプログラミングが可能となる。
現在CbCはGCC及びLLVM/clang上にそれぞれ実装されている。


CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
CodeGearは通常のCの関数宣言の返り値の型の代わりに`__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}に示す。
例題ではCodeGearとして`factorial`を宣言している。
`factorial`はCodeGearの引数として`struct F`型の変数`arg`を受け取り、`arg`のメンバー変数によって`factorial`の再帰呼び出しを行う。
CodeGearの呼び出しは`goto`文によって行われる。
この例題を状態遷移図にしたものを図\ref{fig:factorial_cbc}に示す。
図中の四角がDataGear、 円がCodeGearに対応する。


``` lab:src:cbc_example, cap:CbCで階乗を求める例題
__code factorial(struct F arg) {
    if (arg.n<0) {
        exit(1);
    }
    if (arg.n==0) {
      goto arg.next(arg);
    } else {
      arg.r *= arg.n;
      arg.n--;
      goto factorial(arg);
    }
}
```

![lab:fig:factorial_cbc, cap:CbCで階乗を求める例題の状態遷移](fig/factorial_cbc.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の設計を行っている。
現在の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を元に開発された教育用のUNIX OSである。
xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。
本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。

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

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

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


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

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

![lab:fig:cbc_readsyscall, cap:readシステムコールの状態遷移](fig/readsyscall_state.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`中に記述されている。
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));
            // omission
            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`へ遷移する。
ループ条件が満たされなかった場合は、 コンテキストから`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)
{
// omission

    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));
// omission
}
```

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を管理する機能が必要であると考えられる。
contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。
他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。

現状はxv6の全ての機能をまだCbCを用いて再実装をしていない。
ファイルシステムや仮想メモリにまつわる処理などはAPI単位では再実装しているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。
そのためにOSそのものを状態遷移単位で完全に書き直す必要が存在し、 そのためには全ての処理に対して状態を定義していく必要がある。
xv6にはアセンブラで記述されている処理も複数存在するため、 CodeGrarの表現においてこのような処理の扱いも決定する必要がある。

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

またxv6にはユーザーコマンドも存在しているために、 ユーザーコマンド向けのCbCのAPIなども考慮したい。

# まとめ

本稿ではxv6を継続を用いた単位での再実装を検討し、 実際にいくつかの処理を再実装した。
現状はまだxv6の実装を利用した証明は行っていない。
今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。
それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。