--- a/Gears OSの CodeGear Management.mm	Fri Apr 14 20:27:47 2023 +0900
+++ b/Gears OSの CodeGear Management.mm	Sat Apr 15 15:44:19 2023 +0900
@@ -96,6 +96,21 @@
 </node>
 <node TEXT="common in entire system" ID="ID_426293677" CREATED="1681371740626" MODIFIED="1681371760745"/>
 </node>
+<node TEXT="contents" POSITION="right" ID="ID_989875089" CREATED="1681471011911" MODIFIED="1681471016579">
+<node TEXT="Gears OS" ID="ID_1278063385" CREATED="1681471017088" MODIFIED="1681471022469"/>
+<node TEXT="Normal and Meta computation" ID="ID_881246923" CREATED="1681471023261" MODIFIED="1681471045403"/>
+<node TEXT="scheduling" ID="ID_36667967" CREATED="1681471046057" MODIFIED="1681471050843"/>
+<node TEXT="code table" ID="ID_29473159" CREATED="1681471051798" MODIFIED="1681471430033"/>
+<node TEXT="current implementation" ID="ID_1213592591" CREATED="1681471433871" MODIFIED="1681471443636"/>
+<node TEXT="dynamic loading" ID="ID_916954792" CREATED="1681471447252" MODIFIED="1681471451408"/>
+<node TEXT="UEFI implmentation" ID="ID_1655678668" CREATED="1681471455326" MODIFIED="1681471463651"/>
+<node TEXT="x.v6 implementation" ID="ID_457759694" CREATED="1681471469965" MODIFIED="1681471476106"/>
+<node TEXT="linking" ID="ID_1703694915" CREATED="1681471488739" MODIFIED="1681471493773">
+<node TEXT="correntness" ID="ID_123924946" CREATED="1681471497421" MODIFIED="1681471503194"/>
+<node TEXT="model checking level" ID="ID_1372172844" CREATED="1681471503683" MODIFIED="1681471513294"/>
+</node>
+<node TEXT="conculusion" ID="ID_44556806" CREATED="1681471530163" MODIFIED="1681471535066"/>
+</node>
 <node TEXT="Operating system should control&#xa; all the code" POSITION="left" ID="ID_472841100" CREATED="1681371764698" MODIFIED="1681371800835">
 <node TEXT="code is in db" ID="ID_1555760462" CREATED="1681371803618" MODIFIED="1681371848202"/>
 <node TEXT="managed" ID="ID_1344558154" CREATED="1681371849579" MODIFIED="1681371852479"/>

--- a/code-mangement.ind	Fri Apr 14 20:27:47 2023 +0900
+++ b/code-mangement.ind	Sat Apr 15 15:44:19 2023 +0900
@@ -2,10 +2,93 @@
 
 -author: 河野真治
 
---Gears OS
+--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