\chapter{結論}
本論文では Gears OS のプロトタイプの設計と実装、メタ計算である Context と stub の生成を行う Perl スクリプトの記述を行った。
さらに Raspberry Pi 上での Gears OS 実装の考察、xv6 の機能の一部を CbC で書き換えを行った。

Code Gear 、Data Gear を処理とデータの単位として用いて Gears OS を設計した。
Code Gear、Data Gear にはメタ計算を記述するための Meta Code Gear、Meta Data Gear が存在する。
メタ計算を Meta Code Gear、によって行うことでメタ計算を階層化して行うことができる。
Code Gear は関数より細かく分割されてるためメタ計算を柔軟に記述できる。
Gears OS は Code Gear と Input/Output Data Gear の組を Task とし、並列実行を行う。

Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。
Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。
Interface は複数の実装をもち、Meta Data Gear として定義される。
従来の関数呼び出しでは引数をスタック上に構成し、関数の実装アドレスを Call するが、
Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、操作に対応する Code Gear に goto する。

Context は使用する Code Gear、Data Gear をすべて格納している Meta Data Gear である。
通常の計算から Context を直接扱うことはセキュリティ上好ましくない。
このため Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear である stub Code Gear を定義した。
stub Code Gear は Code Gear 毎に記述され、Code Gear 間の遷移の前に挿入される。

これらのメタ計算の記述は煩雑であるため Perl スクリプトによる自動生成を行なった。
これにより Gears OS のコードの煩雑さは改善され、ユーザーレベルではメタを意識する必要がなくなった。

ハードウェア上での Gears OS の実装を実現させるために Raspberry Pi 上での実装を考察した。
比較的シンプルな OS である xv6 を CbC に書き換えることにした。

xv6 を CbC で書き換えることによって、実行可能な CbC プログラムで記述された OS がそのまま、
状態遷移モデルによるモデル検査、Agda による定理証明が可能となる。 

今後の課題は、
現在は xv6 のシステムコールの一部のみの書き換えと、設計のみしか行っていないので、カーネル全ての書き換えと、
Gears OS の TaskManager の置き換えを行い、Gears OS の機能を xv6 に組み込む必要がある。
また、xv6-rpi は QEMU のみの動作でしか確認してないため、実機上での動作を行う必要がある。