\chapter{OS の拡張性と信頼性の両立}

さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。
OS の信頼性を保証する事自体が難しいが、
時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。
OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分であり、
テストしきれない部分が残ってしまう。
これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
モデル検査は無限の状態ではなくても巨大な状態を調べることになり、
状態を有限に制限したり状態を抽象化したりする方法が用いられている。
(図\ref{fig:verification})
\begin{figure}[ht]
 \begin{center}
  \includegraphics[width=70mm]{./fig/verification.pdf}
 \end{center}
 \caption{証明とモデル検査によるOSの検証}
 \label{fig:verification}
\end{figure}

証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。
%さまざまなものって何？
検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。
つまり信頼性と拡張性を両立させることが重要である。

コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。
%操作的意味論って何？
プログラミング言語で記述される部分をノーマルレベルの計算と呼ぶ。
実際にコードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。
これをメタレベルの計算という。
この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。
ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。

ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。
CbC は関数呼出時の暗黙の環境(Environment)を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。
これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。
これらを用いて、検証された Gears OS を構築したい。
図\ref{fig:MetaGear}。
検証には定理証明支援系である Agda を用いる。
Gears OS の記述はそのまま Agda に落ちる。
CbC で記述することによって検証された OS を実装することができる。

また、Gears の記述をモジュール化するために Interface を導入した。
さらに並列処理の記述用にpar goto 構文を導入する。
これらの機能は Agda 上で継続を用いた関数型プログラムに対応するようになっている。
\begin{figure}[ht]
 \begin{center}
  \includegraphics[width=70mm]{./fig/MetaGear.pdf}
 \end{center}
 \caption{Gearsのメタ計算}
 \label{fig:MetaGear}
\end{figure}

本論文では Interface と par goto の実装を行なった。
%実際の修正は考えてない