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

コンピュータには CPU、ディスプレイ、キーボードやマウス、ハードディスクなど様々な機器が接続されている。
プログラムの処理を行うとき、これらの様々なデバイスのアクセスや資源管理は複雑で容易ではない。
異なるハードウェアを扱う際にはそれぞれに対応したプログラミングを行う必要がある。
OS とはこれらのデバイスの抽象化や資源管理を行う。

ユーザーは OS のおかげで異なるハードウェアの違いを意識することなくプログラミングをすることができる。
例えば同じプログラムで、異なる入力デバイスによる操作や、ディスプレイでの表示などは、
それぞれデバイスへのアクセスなどの複雑な処理を OS が隠すことによって可能となっている。

CPU、メモリ、ディスク、などの本来ユーザーが意識しなければならない資源も、OS が資源管理を行うことで意識することなくプログ
ラミングすることができる。

1950年代におけるコンピューターがプログラムを実行する際には専門のオペレータが存在し、
オペレーターがジョブの管理、コンパイラの選択などを行なっていた。
しかし後に、ジョブの自動実行、やコンパイラのロードを行うプログラムができた。これが OS の祖先である。
コンピュータには科学技術用のコンピューターと商用のコンピューターが開発されていたが、後に汎用コンピューターである System/360 が開発される。
その OS/360 は強力なソフトウェア互換を持っていた。
ソフトウェア互換により全てのソフトウェアが全てのマシンで動作するようになった。
その後、OS は、スプーリングやタイムシェアリングといった機能も導入されるようになった。
1970年代には UNIX が開発され、後に様々なバージョンが開発され、System V、BSD といった派生 OS なども開発され、現在に至る。\cite{os}

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

Meta Gear を入れかえることにより、ノーマルレベルの Gear をモデル検査することができるようにしたい。
ノーマルレベルでの Code Gear と Data Gear は継続を基本とした関数型プログラミング的な記述に対応する。
この記述を定理証明支援系である Agda を用いて直接に証明できるようにしたい。
Gears OS の記述はそのまま Agda に落ちる。
Code Gear、Data Gear を用いた言語である CbC で記述することによって検証された OS を実装することができる。

従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{moggi-monad}。これは Haskell では実行時の環境を記述する構文として使われている。
OS の研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。
Python や Haskell による記述をノーマルレベルとして
採用した OS の検証の研究もある\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}。
SMIT などのモデル検査を OS の検証に用いた例もある\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}。

本研究で用いる Meta Gear は制限された Monad に相当し、型つきアセンブラよりは大きな表現単位を提供する。
Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。
CbC はスタック上に隠された環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。
ただし、Gear のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。

Gears の記述をモジュール化するために Interface を導入した。
これらの機能は Agda \cite{agda} 上で継続を用いた関数型プログラムに対応するようになっている。\cite{agda-ryokka}
これにより Code Gear、Data Gear の Agda による証明が可能となるように Gears OS の構築を行った。 

\begin{figure}[ht]
 \begin{center}
  \includegraphics[width=130mm]{./fig/MetaGear.pdf}
 \end{center}
 \caption{Gearsのメタ計算}
 \label{fig:MetaGear}
\end{figure}

本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。
また、OS の信頼性を保証するため、xv6 \cite{xv6} の CbC による書き換えについて考察する。
xv6 は OS の基本的な機能を持っているにも関わらず、Linux などに比べてシンプルであり、
CbC に書き換えることによって状態遷移ベースのプログラミングが可能となり、
実行可能なプログラムがそのままモデル検査が可能で、Agda による証明が可能な OS となることを目的とする。