-title: Gears OSの CodeGear Management

-author: 河野真治

--Gears OSによる信頼できるサービス

サービスやアプリケーションの信頼性は、OSとユーザプログラムのように分離することはできない。
プログラムの正しさは基本的にはコードの正しさであり、今のOSのようにコードの管理をユーザ空間の
問題として放り出す方法には限界がある。

Gears OSでは実行単位として codeGear、データ単位として dataGear を使う。さらに、これらは
Monad のようにメタ codeGeearやメタdataGearを持っている。

Gears OSでの検証は、Agdaを使った GearsAgdaを用いる。これらの実行と並列実行は、
GearsAgdaに対して定義される。当然、すべてのGearsAgdaのcodeGearは、Gears OSに
登録されることになる。

この論文では、Gears OSのcodeGearの管理方法について考察する。

--Normal and Meta computation

Gears OSの基本は、CbC (Continuation based C)であり、input interfaceとoutput interfaceを有限な処理で
結ぶものになっている。これは、コンパイラの基本ブロックに大体相当する。これはさらに、GearsAgdaの
Agdaで記述された invariant あるいは、表示的意味論と直結している。

CbCの記述は以下のようなものである。

    __code startTimer(struct TimerImpl* timer, __code next(...)) {
        struct timeval tv;
        gettimeofday(&tv, NULL);
        timer->time = tv.tv_sec + (double)tv.tv_usec*1e-6;
        goto next(...);
    }

nextが軽量継続を表している。このcodeGearの実行は論理的に割り込まれない。つまり、並行実行は
この単位で行われ定義される。ハードウェアでの並行実行、割り込み処理などは、それにそって
実装される必要がある。これらは、GearsAgdaでは、外部環境へのアクセスがある。この場合は
時刻に対するアクセスである。

OS側からみると、これは詳細のない単なるコードに見える。実行の詳細、つまり、実行に関係する
すべての dataGear 、すべてのcodeGearは、プロセスに相当する Context metaDataGearに格納される。

つまり、OSからみた codeGearの実行は、

　　Contextから詳細を取り出すmeta codeGearの番号から、codeGearを選ぶ
　　それを実行し、continuation としてshcedulerを指定する
　　これを CPU worker 毎に実行する

ということになる。CPU worker毎に Contextは一つなので、Contextはsingle threadで実行される。
これにより、並行実行の単位はcodeGearとなる。
ただし、Context関の共有データがある場合は意味的なずれがでる場合がある。それは、
Contextの実行をそうなるように実装することになる。

その実装の正しさは、実装を GearsAgdaで記述することより可能になるが、その実装が物理的に一致するかどうかの
保証はハードウェアの性質に依存する。

外界との対応もメタ計算になるが、それはGearsAgdaによるシミュレーションに対する正しさということになる。

scheduler から codeGearへの移行は、以下のmeta codeGear で実装される。

    __code meta(struct Context* context, enum Code next) {
        goto (context->code[next])(context);
    }


\verb+context->code[next]+が codeGearのtableの呼び出しになるが、
これは表がコンパイル時に確定し、直接の呼び出しでは、コンパイラが最適化するので、overhead とはならない。
meta が書き換えられている場合は、ここで Context switchが起きることになる。

このContext switchでメモリ空間の切り替えが必要かどうかは application に依存する。
もし、codeGearの実行の正しさが証明されているなら、メモリ空間を切り替える必然性はない。
実際、Kernel 内や Realtime Monitor では切り替えない方が普通である。

--証明付きのコード

GearsAgdaで記述されていれば、codeGearやdataGearは証明を持つ。これらは単なる型なので実行時には
実態を持たない。ただし、それを実行時にチェックすることもできる。assertなどと同じ扱いである。

GearsAgdaの証明に閉じていれば、その範囲内での信頼性がある。しかし、動的にcodeが読み込まれる場合は
そうはならない。その時には、証明しなおす、簡易あるいは詳細なモデル検査を実施するなどが可能だが、
それらが実用的とは限らない。

codeはContextの表に登録されるが、システム全体のcodeは Database で管理される。その管理は
ファイルシステム上でも良い。codeは証明が付属している場合もあるが、それは何らかの形で
codeGear Databseに格納される。






--並列実行

--code table

--dynamic loading

--実装

--linkの方法

--まとめ