\chapter{評価}

本研究では、Gears OS のモジュール化、メタレベルの計算の自動生成、
xv6 の CbC 書き換えの考察と、システムコールの書き換えを行なった。

これらの実装についての評価を行う。

\section{Gears OS のモジュール化}
Gears OS の モジュール化について評価を行う。
モジュール化されていない以前の Gears OS ではソースコード \ref{prevgear} 4行目のように、
Code Gear 直接指定しなければならなかった。
Interface を用いた ソースコード \ref{intergear} ではここを stack$->$push のように抽象化することができる。

また、Gears OS では、ある Data Gear を Code Gear が扱う場合、
Code Gear に対応する Data Gear を Context が持つ Data Gear のリストから取り出す必要があるが、
ソースコード \ref{prevgear} 12、13行目のように Context に引数格納用として型ごとに確保された Data Gear を、
複数の Code Gear で使いまわしてしまう問題があった。
これも Interface を用いることで、Interface 用に実装で用いる Data Gear を持てるようになり、
ソースコード \ref{intergear} 12、13行目のように使うことができるようになった。

\begin{lstlisting}[frame=lrbt,label=prevgear,caption={\footnotesize Interface を用いない Gears}]
__code cg1 (struct Context* context, struct Element* element) {
    struct Node* node1 = new Node();
    element->data = (union Data*)node1;
    goto meta(context, pushSingleLinkedStack)
}

__code pushSingleLinkedStack(struct Context* context, struct SingleLinkedStack* stack, struct Element *element) {
    ...
}

__code pushSingleLinkedStack_stub(struct Context* context){
    SingleLinkedStack* stack = &context->data[SingleLinkedStack]->SingleLinkedStack;
    Element *element = &context->data[Element]->element;
    goto pushSingleLinkedStack(context, stack, data);
}

\end{lstlisting}

\begin{lstlisting}[frame=lrbt,label=intergear,caption={\footnotesize Interface を用いた Gears}]
__code cg1 (struct Context* context, struct Stack* stack) {
    struct Node* node1 = new Node();
    goto stack->push((union Data*)node1,cg2);
}

__code pushSingleLinkedStack(struct Context* context, struct SingleLinkedStack* stack, union Data* data, __code next(...)) {
    ...
}

__code pushSingleLinkedStack_stub(struct Context* context){
    SingleLinkedStack* stack = (SingleLinkedStack*)context->data[D_Stack]->Stack.stack->Stack.stack;
    Data* data = &context->data[D_Stack]->Stack->data;
    enum Code next = &context->data[D_Stack]->Stack->next;
    goto pushSingleLinkedStack(context, stack, data, next);
}

\end{lstlisting}

\section{Code Gear の変換と Meta Gear の自動生成}

CbC はノーマルレベルとメタレベルという異なる階層を持つ言語である。
メタレベルのコードの変換と生成は本来コンパイラで行うべきものだが、
Code Gear の変換や Meta Gear の生成の考察や評価のため、
現在は Perl スクリプトにより、コンパイル時に生成、変換を行なっている。

Code Gear の引数は、ノーマルレベルと、メタレベルによって意味が異なる。
ノーマルレベルでは引数はそのまま次の Code Gear へと渡す引数の集合だが、
メタレベルでは Context から参照して取り出す Data Gear を表す。
この意味のズレを調整するのが stub Code Gear である。

stub Code Gear は、Code Gear 間の継続の間に挟まれる。
この stub Code Gear へ継続するための ノーマルレベルの Code Gear の変換作業を行うことは、
ノーマルレベルとメタレベルでのズレを調整するために必要な作業である。

また、stub Code Gear は Code Gear 毎に挿入されるため、               
これが自動生成されることによってソースコードの記述量が大幅に減少した。

\section{xv6 の CbC 書き換えのための環境構築}
xv6-rpi の CbC 書き換えを行うために、ARM 用のクロスコンパイラを build する必要があった。
しかし、LLVM 上で実装した CbC では上手くいかなかったため、GCC 上で実装した CbC を用いることにした。
GCC 上で実装した CbC は更新が止まっていたため、現在の GCC へのアップデート作業を行なった。

これにより、GCC 上で実装された CbC が、最新の環境で動作するようになり、
ARM 用のクロスコンパイラの build も可能となった。

\section{xv6 の CbC 書き換え}

CbC は Code Gear 間の遷移は goto による継続で行われるため、
状態遷移ベースでのプログラムに適している。
xv6 を CbC で書き換えることにより、実行可能な OS のプログラムを状態遷移モデルに落とし込むことができる。
これにより状態遷移系のモデル検査が可能となる。

xv6 のシステムコールを CbC によって書き換えることで、
元の C のソースコードからの大きな変更をすることなしに、
図 \ref{fig:state} のように状態遷移ベースの実行可能なプログラムへと落とし込むことができた。

また、CbC は C 言語との互換があるため、システムコールのみ CbC へと書き換えるといったことも可能であるため、
信頼性を保証したい機能のみを CbC で記述することもできる。

さらに、CbC は Agda に変換できるように設計されているため CbC で記述された実行可能なプログラムが、
そのまま Agda による定理証明が可能となる。

これらのため、CbC で記述された実行可能な OS そのものがモデル検査と定理証明が可能となり、
OS の信頼性が保証できる。