-title: Gears OSの CodeGear Management

-author: 仲吉菜々子 and 河野真治 

--abstract:

GearsOSではすべてのプログラムはKernelやdriverを含めて CodeGear
で書かれている。これらは、CodeGear のSystem DBに格納される
べきである。Microwre OS9でもmoduleという形でメモリに展開さ
れていた。CodeGearの集合で一つのアプリやサービスが作られる。
このCodeGearnの組み合わせを指定する仕組みが必要である。また、
CodeGear を実行時にloadする機構を作ることにより、現在、clnag
のlinkerで行っている作業抜きでGearsOSを構成できる。これによ
り、GearsOSのbuildを簡単にすることができる。高速化が必要な
場合は、複数のCodeGearをまとめて最適化して、一つのCodeGearn
にする。しかし、実行時のメタ計算がが必要な場合は、それよう
のhookを用意する必要がある。これの仕組みについて考察する。

--abstract-e:

In GearsOS, all programs, including kernels and drivers, are
written in CodeGear. These should be stored in the System DB
of CodeGear. In Microwre OS9, they were deployed in memory 
as modules. An application or service is created using a set
of CodeGear. A mechanism is needed to specify the combination
of CodeGear. Additionally, by creating a mechanism to load 
CodeGear at runtime, GearsOS can be built without the work 
currently done by the clnag linker. This simplifies the process
of building GearsOS. When optimization is necessary, multiple
CodeGear can be combined and optimized to create a single CodeGear.
However, if runtime metacalculation is necessary, a hook must
be provided for it. 

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

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

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

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

OSでの証明よる検証はいろいろ行なわれているが、Haskellに近い形式に変換することが多い
\cite{Klein:2014:CFV:2584468.2560537,Chen:2015:UCH:2815400.2815402,Yang:2010:SLI:1806596.1806610}。
Gears OSでは、GearsAgda で直接に記述できる点が新しい。

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

--Normal and Meta computation

Gears OSの基本は、CbC (Continuation based C)\cite{cbc-github}であり、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(図\ref{Gears OS})に格納される。

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

    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 では切り替えない方が普通である。

<center><img src="fig/gears_structure.pdf" alt="Gears OS"></center>

--証明付きのコード

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

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

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

現状では、証明はAgdaで記述されたデータ構造でしかない。それをcodeGear DBに入れても利用する方法は
ないがいくつかの利用法は考えられる。

  証明とcodeGearの一致を確認する
  型整合に使う
  codeの認証に使う

この大域のcodeGear DBは、kernelを含めたすべてのcodeGearに対するもので全部で共有される。つまり、
あらゆるversionを含む共有ライブラリとなる。これは全世界でuniqueなDBとしても良い。

--CbCのcodeGear と GearsAgdaの違い

CbCのcodeGearとdataGearは、普通のCの関数と構造体であり、その意味で不思議なところはない。しかし、
normal levelではpointerが出てこないのが望ましい。なぜなら、メモリ配置は meta levelの問題で
プログラムの正しさとは直接関係しないからである。つまり、normal levelでの構造体は List や 木
など以外の再帰的構造でも直接的なポインタ操作は行わない。meta levelでは、メモリの直接操作
例えば mallocやfree、あるいは共有データの扱いなどをポインタを通して行う。

meta levelでのポインタ操作は、データ構造に対する操作であり、そのlevelに閉じる限り、
プログラムの正しさはポインタの実装に依存しない。その意味で、meta codeGear も単なる
noraml level のcodeGear に過ぎない。meta codeGearの証明あるいは、実装をさらにmeta level
で行うこともできる。

GearsAgda では、すべてはAgdaの構造体で表現される。これらは変数と項であり、基本的に複製可能
な項である。その意味で、ポインタを持たないと言ってよい。Listや木の実装を配列と番号で行う
ことはまったく実用的ではないので、普通に再帰的なデータ構造を使ってよい。ただし、それを
自分自身の codeGear の再帰呼び出しで行うと、codeGearの実行が有界な時間に閉じなくなる。
なので、loop は軽量継続を用いて、一旦、外にでることになる。これは、この段階でmeta level的に処理が
割り込まれることも意味している。

GearsAgda で処理された項は、ContextのdataGearに格納される。また、GearsAgdaのcodeGearは、
Contextのcode table(図\ref{code table})に格納される。どちらも、メモリ的には番号で管理されることになる。
GearsAgda の Context は、その意味で、プロセスのメモリ空間そのものを抽象化したものになっている。


つまり、CbCのcodeGearと GearsAgdaは、normal level ではポインタを使わないのだが、
その意味は、CbCと GearsAgda で若干異なる。CbCでの実装は、GearsAgdaでの実装の持つ
性質を保存する必要がある。

<center><img src="fig/codetable.pdf" alt="code table"></center>

--Contextを通した dataGearとcodeGearの連携

Gears OSでは、Context はCの構造体であり、一つのContextで使用するdataGearとcodeGearは、そこに格納される。
複数のContextから、dataGearもcodeGearも共有されることがある。その排他制御は、Gears OSのmeta codeGearに
よって行われる。

Gears OSは、interfaceという構造体でオブジェクト表現していて、これらには、メソッドを格納する配列がある。
この配列の添字を他のinterfaceが使用する。なので、interface間の呼び出しは、interfaceを表すdataGearと
そのメソッドの番号で決定される。

引数は、interface毎に Contextに決まった場所が確保される。これは、通常ではstack上に場所を確保する。
しかし、CbCでは関数呼び出しはstackを使わないので、このようにする必要がある。これは、もちろん、
マルチスレッドな実行では破壊されるおそれがあるが、Contextはシングルスレッドで実行することになっている
ので問題ない。

Contextの切り替えは、codeGearの境目で行われるので、Contextと実行しているcodeGearのcode tableの番号で
状態が決定する。つまり、Gears OSでは、Task Switchにはレジスタは関係しない。割り込みなどは、codeGearの
境界と独立に起きるが、それをmeta codeGearが境界で Context switchが起きたのと同じようにすることを
保証する。これは一種の遅延処理となる。もちろん、影響がないなら、割り込み中にmetaな処理を行ってもよい。
これは、本来はCPUなどのハードウェアでサポートされるべきかもしれない。

dataGearは、metaな情報として、dataGearの構造定義を番号として持っている。これを使うことにより
任意のdataGearの表示を正しく行うことができる。この情報を取り扱うことは meta level からでしか
許されないが、CbC的には特に制限はない。

引数として呼び出される dataGearは、Context上に前もって確保されているが、実行時にallocateされる
dataGearもContextから参照される pool に確保される。これの管理は meta dataGear (Gears OSのkernel)
が行う。GearsAgda は、この部分はAgdaが管理するので meta的な管理は行われない。しかし、
Context を用いた並行実行の場合は、Context上での管理の問題が生じる。


--code table

contextの初期化の中で、code table に実際の codeGear stub へのポインタが初期化される。

    context->code[C_add]    = add_stub;
    context->code[C_checkAndSetAtomicReference]    
       = checkAndSetAtomicReference_stub;
    context->code[C_clearSingleLinkedQueue]    = clearSingleLinkedQueue_stub;
    context->code[C_clearSynchronizedQueue]    = clearSynchronizedQueue_stub;
    context->code[C_code1]    = code1_stub;
    context->code[C_createTask1]    = createTask1_stub;
    context->code[C_createTask2]    = createTask2_stub;
    context->code[C_decrementTaskCountTaskManagerImpl]    
        = decrementTaskCountTaskManagerImpl_stub;
    context->code[C_exit_code]    = exit_code_stub;
    context->code[C_getTaskCPUWorker]    = getTaskCPUWorker_stub;
    context->code[C_incrementTaskCountTaskManagerImpl]    
        = incrementTaskCountTaskManagerImpl_stub;

interfaceの初期化の中で、この番号が interfaceを表す dataGearに格納される。

    Tree* createRedBlackTree(struct Context* context) {
        struct Tree* tree = &ALLOCATE(context, Tree)->Tree;
        struct RedBlackTree* redBlackTree 
           = &ALLOCATE(context, RedBlackTree)->RedBlackTree;
        tree->tree = (union Data*)redBlackTree;
        redBlackTree->root = NULL;
        redBlackTree->nodeStack = createSingleLinkedStack(context);
        tree->put = C_putRedBlackTree;
        tree->get = C_getRedBlackTree;
        tree->remove = C_removeRedBlackTree;
        return tree;
    }

この辺の構造は、GearsAgda  側では簡素化されている。実際、pointer を直接操作しないとかも、厳密に守る必要はなく、
GearsAgda と CbC での実装が平行していれば問題はない。

--codeGearのlinkage

Gears OSのあらゆるコードは、codeGear DBのコードの組み合わせになる。しかし、そのためには、
Contextから詳細なデータを取り出して、実行し、次のcodeGearを呼び出す時にContextの正しい場所にdataGearを格納する
必要がある。これは codeGear 全体に対して必要になる。

現状では、これは stubとしてコンパイル時に生成される。

    __code checkAndSetAtomicReference(struct AtomicReference* atomic, 
       union Data** ptr, union Data* oldData, union Data* newData, __code next(...), 
       __code fail(...)) {
        if (__sync_bool_compare_and_swap(ptr, oldData, newData)) {
            goto next(...);
        }
        goto fail(...);
    }

では、Context 上には以下の構造と、それを呼び出す stub がある。

    struct Atomic {
        union Data* atomic;
        union Data** ptr;
        union Data* oldData;
        union Data* newData;
        enum Code checkAndSet;
        enum Code next;
        enum Code fail;
    } Atomic;

    __code checkAndSetAtomicReference_stub(struct Context* context) {
            AtomicReference* atomic = (AtomicReference*)
               GearImpl(context, Atomic, atomic);
            Data** ptr = Gearef(context, Atomic)->ptr;
            Data* oldData = Gearef(context, Atomic)->oldData;
            Data* newData = Gearef(context, Atomic)->newData;
            enum Code next = Gearef(context, Atomic)->next;
            enum Code fail = Gearef(context, Atomic)->fail;
            goto checkAndSetAtomicReference(context, atomic, 
                ptr, oldData, newData, next, fail);
    }

これらは単一のGears OS内で整合する必要がある。実際には、これらは、stubが参照する Context内のoffsetにすぎない。
Atomic は dataGear の巨大な Union になっている。これは、GearsAgda でも状況は同じで、巨大な Sum type になっている。

このContext内での offsetと呼び出すcodeGearの番号が一致すれば、Kernel側で整合性の問題はない。

--codeGearのコンパイル方法

現在の Gears OSのcodeGearは、interfaceを含む記述を .cbc に書き、それを CbC に変換している。
この時に、meta codeGear として stub そして、meta dataGearとして Context の定義が生成される。

Context の定義は Application 毎に異なっているが、全部をそろえることも可能である。この変換は
Perl script で記述されていて、煩雑になっている。これを codeGear / interface 単位で .o と
meta dataGearにできれば、全体の構成と、interfaceのコンパイルが簡単になると期待される。

ただし、この場合は、Context の中での引数領域のoffset管理、code tableの初期化、code間の
遷移を扱う codeGearの番号の指定の書き換えなどが必要となる。

--static linkage

コンパイル時に codeGearの結合が明らかならば、それは一つのcodeGearとしてまとめてよい。Contextへの書き込みもさぼることが
可能になる。ただし、時分割実行される場合は、codeGearの切れ目で分割するのと同じ実行が要求される。
つまり、割り込み処理などで途中で実行が中断するならば、それはその単位まで実行してから、Contextを切り替える必要がある。

これを実現する手法はflagを参照する方法や、コードを書き換える方法あるいは、polingを埋め込むなどの方法が考えられる。
整合性が不要であれば途中で止めても問題ないが、その場合は register などの状態を従来のOSのように保持する必要がある。

codeGear単位で正直に分割コンパイルすると最適化の余地がない。しかし、その場合でもJITなどは可能である。

--boot codeGear

今の実装では、UEFIから Gears OSが読み出される。Gears OS自体は、x.v6\cite{xv6rpi}と同じで、ファイルシステムを
含む一体の binary になっている。

codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。


--まとめ

Gears OS と GearsAgda における codeGear の管理方法について考察した。将来的には GearsAgda で記述された
証明付きinterfaceのコードを CbC に変換し、それを Gears OSで正しさを確認しながら組み合わせて、meta計算の
変更を可能にしながら実行するシステムを作りたい。