\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のすべての処理を検査するのは難しい。


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


OSを状態遷移系で実装する場合、通常のC言語では状態ごとに分離するのは困難である。
関数呼び出しを利用して状態を切り分けても、 関数呼び出し時に伴うスタックフレームの操作などでパフォーマンスにも問題がある。
この問題を解決するには、 C言語よりも細かく記述できる言語で実装する必要がある。