Mercurial > hg > Papers > 2023 > nana-sigos

--- a/code-mangement.ind	Mon Apr 17 15:39:57 2023 +0900
+++ b/code-mangement.ind	Mon Apr 17 18:28:26 2023 +0900
@@ -1,6 +1,35 @@
 -title: Gears OSの CodeGear Management

--author: 河野真治
+-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による信頼できるサービス

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

-Gears OSでの検証は、Agdaを使った GearsAgdaを用いる。これらの実行と並列実行は、
+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)であり、input interfaceとoutput interfaceを有限な処理で
+Gears OSの基本は、CbC (Continuation based C)\cite{cbc-github}であり、input interfaceとoutput interfaceを有限な処理で
 結ぶものになっている。これは、コンパイラの基本ブロックに大体相当する。これはさらに、GearsAgdaの
 Agdaで記述された invariant あるいは、表示的意味論と直結している。

@@ -38,11 +71,11 @@
 時刻に対するアクセスである。

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

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

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

@@ -71,6 +104,8 @@
 もし、codeGearの実行の正しさが証明されているなら、メモリ空間を切り替える必然性はない。
 実際、Kernel 内や Realtime Monitor では切り替えない方が普通である。

+<center><img src="fig/gears_structure.pdf" alt="Gears OS"></center>
+
 --証明付きのコード

 GearsAgdaで記述されていれば、codeGearやdataGearは証明を持つ。これらは単なる型なので実行時には
@@ -115,7 +150,7 @@
 割り込まれることも意味している。

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


@@ -123,6 +158,8 @@
 その意味は、CbCと GearsAgda で若干異なる。CbCでの実装は、GearsAgdaでの実装の持つ
 性質を保存する必要がある。

+<center><img src="fig/codetable.pdf" alt="code table"></center>
+
 --Contextを通した dataGearとcodeGearの連携

 Gears OSでは、Context はCの構造体であり、一つのContextで使用するdataGearとcodeGearは、そこに格納される。
@@ -154,6 +191,43 @@
 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のコードの組み合わせになる。しかし、そのためには、
@@ -162,7 +236,9 @@

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

-    __code checkAndSetAtomicReference(struct AtomicReference* atomic, union Data** ptr, union Data* oldData, union Data* newData, __code next(...), __code fail(...)) {
+    __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(...);
         }
@@ -182,13 +258,15 @@
     } Atomic;

     __code checkAndSetAtomicReference_stub(struct Context* context) {
-            AtomicReference* atomic = (AtomicReference*)GearImpl(context, Atomic, atomic);
+            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);
+            goto checkAndSetAtomicReference(context, atomic,
+                ptr, oldData, newData, next, fail);
     }

 これらは単一のGears OS内で整合する必要がある。実際には、これらは、stubが参照する Context内のoffsetにすぎない。
@@ -221,7 +299,7 @@

 --boot codeGear

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

 codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。
--- a/main.tex	Mon Apr 17 15:39:57 2023 +0900
+++ b/main.tex	Mon Apr 17 18:28:26 2023 +0900
@@ -39,9 +39,9 @@

 % 和文著者名
 \author{
-{河野真治} \\
+{仲吉菜々子, 河野真治} \\
 琉球大学工学部\\
-{Shinji KONO} \\
+{Nakako Nakayoshi, Shinji KONO} \\
 Faculty of Engineering, University of the Ryukyus\\
 }