%OS研究会のまま、要相談
\chapter*{要旨}
現代の OS では拡張性と信頼性を両立させることが要求されている。
信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。

Gears OS は Continuation based C (CbC) によってアプリケーションと OS そのものを記述する。
OS の下ではプログラムの記述は通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、
エラーハンドリング等の記述しなければならない処理が存在する。
これらの計算をメタ計算と呼ぶ。
メタ計算を通常の計算から切り離して記述するために、Code Gear、Data Gear という単位を提案している。
CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。

OS は時代とともに複雑さが増し、OS の信頼性を保証することは難しい。
そこで、基本的な OS の機能を揃えたシンプルな OS である xv6 を CbC で書き換え、OS の機能を保証する。

Code Gear は goto による継続で処理を表すことができる。
これにより、状態遷移による OS の記述が可能となり、複雑な OS のモデル検査を可能とする。
また、CbC は 定理証明支援系 Agda に置き換えることができるように構築されている。
これらを用いて OS の信頼性を保証したい。

CbC でシステムやアプリケーションを記述するためには、Code Gear と Data Gear を柔軟に再利用する必要がある。
このときに機能を接続するAPIと実装の分離が可能であることが望ましい。
Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。

本論文では、Interface を用いたモジュールシステムの説明と、
xv6 の CbC 書き換えについての考察を行う。

\chapter*{Abstract}
%英語論文
Contemporary OS is required to achieve both scalability and reliability.
We are designing Gears OS with the goal of guaranteeing reliability for normal level computation and realizing extensibility with meta level computation.

Gears OS describes applications and OS themselves with Continuation based C (CbC).
In addition to normal processing, the description of the program under the OS includes memory management, queuing of threads, management of the network,
There is a process that must be described such as error handling.
These computation are called meta computation.
In order to describe the meta computation separately from normal computation, we propose a unit called Code Gear, Data Gear.
CbC describes the program in units of Code Gear and Data Gear.

It is necessary to flexibly reuse Code Gear and Data Gear to describe systems and applications.
At this time it is desirable that it is possible to separate API and implementation connecting functions.
In order to guarantee the reliability of the Gears OS, it is necessary to provide a formatted module system.

In this paper, we describe the module system using Interface,
In order to enable meta computation and parallel execution on hardware,
We also consider the implementation of Gears OS on Raspberry Pi.

In order to meta computation on hardware and execute it in parallel, basic OS functions are aligned,
It is realized by replacing simple xv 6 with Gears OS.