\chapter{GearsOSにおけるデバッグ}

OSはCPUの割り当てやスケジュール、記憶容量へのアクセスなどアプリケーションが動作する上で土台となる重要なソフトウェアである。
そのためOSの信頼性は高く保証されている必要がある。
信頼性を保証する方法として形式検証が挙げられる。
形式検証には定理証明とモデル検査があり、定理証明はAgda\cite{agda}などの定理証明支援系を用いて数学的にプログラムの信頼性を保証する。
モデル検査はプログラムが特定の状態から遷移しうる全ての状態を数え上げ、
仕様を満たしているかどうかを検査することでプログラムの信頼性を保証する。

本研究室では定理証明やモデル検査を用いて信頼性の保証を行うGearsOSの開発を行っている。
GearsOSはContinuation Based C(CbC)を用いて記述したOSで、CbCは本研究室で開発している言語で、CodeGearというプログラム単位で記述・遷移するC言語の下位言語である。
CodeGear間の遷移は通常の関数呼び出しではなく、goto文によって行われるため、呼び出し元へ戻らない。
そのためプログラムの記述をそのまま状態遷移として落とし込むことができ、これにより定理証明やモデル検査が可能である。

GearsOSは定理証明やモデル検査により信頼性の保証を行っているが、
これらの定理証明やモデル検査自体を自分がどう証明したのかを確かめたり、GearsOS上の例題のデバッグしたいということがある。
現状このような場合にはGDB\cite{gdb}やLLDB\cite{lldb}などの既存のデバッガを用いて変数の値の確認や、
スタックトレースによる関数呼び出しの確認を行うことでデバッグを行っている。
しかし、GearsOSは変数の格納方法が複雑なため煩雑な記述を行わなければならない特性や、
スタックを持たないためにスタックトレースが使えないなどの特性を持つ。これらの特性によりプログラムの遷移の流れや、
変数の値の変化など既存デバッガを用いたデバッグが難しいという問題がある。

本研究ではGearsOS特化のデバッガを開発することでエラー・バグの発見および修正のコストを下げるとともにさらなるGearsOSの信頼性の向上を目指す。