\chapter{OSとアプリケーションの信頼性}

コンピューター上では様々なアプリケーションが常時動作している。
動作しているアプリケーションは信頼性が保証されていてほしい。
信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。
アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。

アプリケーションは通常特定のプログラミング言語で実装されている。
このプログラミング言語自身の信頼性は高く保証される必要がある。
また、実際にアプリケーションを動作させるOSも高い信頼性が保証される必要がある。
OSはCPUやメモリなどの資源管理と、 ユーザーにシステムコールなどのAPIを提供することで抽象化を行っている。


OSの信頼性の保証もテストコードを用いて証明することも可能ではあるが、 アプリケーションと比較するとOSのコード量、 処理の量は膨大である。
またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。
テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。
実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。
非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。


テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。
形式手法の具体的な検証方法の中で、 証明を用いる方法とモデル検査を用いる方法がある。
証明を用いる方法ではAgdaやCoqなどの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
Curry-Howard同型対応則により、型と論理式の命題が対応する。
この型を導出するプログラムと実際の証明が対応する。
特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
証明そのものは記述した関数の内容の整合性を、定理証明支援系が検証する。
証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。
AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。
しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。
Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。
検証ができているソースコードそのものを使ってOSを動作させたい。


他の形式手法にモデル検査がある。
モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。
例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。
しかしOSの処理は膨大である。
すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。
状態を有限に制限したり抽象化を行う必要がある。


OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
範囲が限られているため、有限時間でモデル検査などで検証することが可能である。
この為にはOSの処理を状態遷移系で表現し、 証明しやすくする必要がある。


証明を行う対象の計算は、 その意味が大きく別けられる。
OSやプログラムの動作においては本来したい計算がまず存在する。
これはプログラマが通常プログラミングするものである。
それ以外にデータをメモリに保存するためにメモリのアロケーションをする処理や、メモリから値を持ってくる処理が入る。
メモリのほかにCPUの資源管理なども必要となる。
ユーザーレベルから見ると、データの読み込みなどは資源へのアクセスが必要であるため、システムコールを呼ぶ必要がある。
システムコール自体もメタ計算である。
ユーザーが本来やりたい計算以外に、資源管理などのこれら計算を行う上でやらなければならない計算が存在する。
前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。
ノーマルレベルの計算を確実に行う為には、メタレベルの計算が重要となる。


プログラムの整合性の検証はメタレベルの計算で行いたい。
ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。
またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。
この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。
メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。
この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。

プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。