% sigos のやつ
\chapter{プログラミング言語の検証}
\label{chapter:intro}
現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。
実際に kernel 検証を行った例\cite{Klein:2010:SFV:1743546.1743574} \cite{Nelson:2017:HPV:3132747.3132748}
では C で記述された Kernel に対して、検証用の別の言語で書かれた等価な kernel を用いて OS の検証を行っている。
また、別のアプローチとして ATS2\cite{ats2} や Rust\cite{rust} などの低レベル記述向けの言語を
実装に用いる手法が存在している。

証明支援向けのプログラミング言語としては Agda\cite{agda}、 Coq\cite{coq} などが存在しているが、
これらの言語自体は実行速度が期待できるものではない。

そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{kaito-lola} (CbC) という言語を開発している。

CbC では、処理の単位を CodeGear、 データの単位を DataGear としている。
CodeGear は値を入力として受け取り出力を行う処理の単位であり、 CodeGear の出力を 次の GodeGear に接続してプログラミングを行う。 CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。
このメタ計算部分で検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。

本研究では Agda 上で CodeGear、DataGear という単位を用いてプログラムを記述し、
メタ計算部分で Hoare Logic を元にした検証を行った。


%現代の OS では拡張性と信頼性を両立させることが要求されている。
%時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。
%しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。
%これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
% 証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。
% 型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610}
% 従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。
% また SPIN などのモデル検査を OS の検証に用いた例もである。
% 本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。