# 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`で宣言を行う。

CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。
例題ではCodeGearとして`factorial`を宣言している。
`factorial`はCodeGearの引数として`struct F`型の変数`arg`を受け取り、`arg`のメンバー変数によって`factorial`の再帰呼び出しを行う。
`arg`の様なCodeGearの引数のことを`DataGear`と呼ぶ。
CodeGearの呼び出しは`goto`文によって行われる。


``` src:cbc_example, 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);
    }
}
```

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では、 CodeGearとDataGearを元にプログラミングを行う。
遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。
Contextそのものは、 DataGearの実行に必要なMetaDataGearである。
プログラマがプログラミングする上では別のCodeGearに直接遷移している様に見えるが、 実際はMetaCodeGearを一度経由してからCodeGearに遷移する。

# 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のファイルシステムの一部の分析

xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。
この中に出てくる関数に着目し、 この関数をさらにCodeGearに変換していくことで状態遷移単位での記述を試みた。

まず関数内でif文などの分岐を持たない基本単位であるBasic Blockに着目した。
CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。
したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearへ変換することで状態遷移系への変換を行った。