Mercurial > hg > Papers > 2023 > nana-sigos

comparison code-mangement.ind @ 6:c6bea5a028fd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 17 Apr 2023 18:28:26 +0900
parents c0d369375b21
children 36b34f6e906a
comparison
equal deleted inserted replaced
5:890dcb9acc8b 6:c6bea5a028fd
1 -title: Gears OSの CodeGear Management 1 -title: Gears OSの CodeGear Management
2 2
3 -author: 河野真治 3 -author: 仲吉菜々子 and 河野真治
4
5 --abstract:
6
7 GearsOSではすべてのプログラムはKernelやdriverを含めて CodeGear
8 で書かれている。これらは、CodeGear のSystem DBに格納される
9 べきである。Microwre OS9でもmoduleという形でメモリに展開さ
10 れていた。CodeGearの集合で一つのアプリやサービスが作られる。
11 このCodeGearnの組み合わせを指定する仕組みが必要である。また、
12 CodeGear を実行時にloadする機構を作ることにより、現在、clnag
13 のlinkerで行っている作業抜きでGearsOSを構成できる。これによ
14 り、GearsOSのbuildを簡単にすることができる。高速化が必要な
15 場合は、複数のCodeGearをまとめて最適化して、一つのCodeGearn
16 にする。しかし、実行時のメタ計算がが必要な場合は、それよう
17 のhookを用意する必要がある。これの仕組みについて考察する。
18
19 --abstract-e:
20
21 In GearsOS, all programs, including kernels and drivers, are
22 written in CodeGear. These should be stored in the System DB
23 of CodeGear. In Microwre OS9, they were deployed in memory
24 as modules. An application or service is created using a set
25 of CodeGear. A mechanism is needed to specify the combination
26 of CodeGear. Additionally, by creating a mechanism to load
27 CodeGear at runtime, GearsOS can be built without the work
28 currently done by the clnag linker. This simplifies the process
29 of building GearsOS. When optimization is necessary, multiple
30 CodeGear can be combined and optimized to create a single CodeGear.
31 However, if runtime metacalculation is necessary, a hook must
32 be provided for it.
4 33
5 --Gears OSによる信頼できるサービス 34 --Gears OSによる信頼できるサービス
6 35
7 サービスやアプリケーションの信頼性は、OSとユーザプログラムのように分離することはできない。 36 サービスやアプリケーションの信頼性は、OSとユーザプログラムのように分離することはできない。
8 プログラムの正しさは基本的にはコードの正しさであり、今のOSのようにコードの管理をユーザ空間の 37 プログラムの正しさは基本的にはコードの正しさであり、今のOSのようにコードの管理をユーザ空間の
9 問題として放り出す方法には限界がある。 38 問題として放り出す方法には限界がある。
10 39
11 Gears OSでは実行単位として codeGear、データ単位として dataGear を使う。さらに、これらは 40 Gears OSでは実行単位として codeGear、データ単位として dataGear を使う。さらに、これらは
12 Monad のようにメタ codeGeearやメタdataGearを持っている。 41 Monad のようにメタ codeGeearやメタdataGearを持っている。
13 42
14 Gears OSでの検証は、Agdaを使った GearsAgdaを用いる。これらの実行と並列実行は、 43 Gears OSでの検証は、Agda\cite{Agda,AgdaWiki}を使った GearsAgdaを用いる。これらの実行と並列実行は、
15 GearsAgdaに対して定義される。当然、すべてのGearsAgdaのcodeGearは、Gears OSに 44 GearsAgdaに対して定義される。当然、すべてのGearsAgdaのcodeGearは、Gears OSに
16 登録されることになる。 45 登録されることになる。
17 46
47 OSでの証明よる検証はいろいろ行なわれているが、Haskellに近い形式に変換することが多い
48 \cite{Klein:2014:CFV:2584468.2560537,Chen:2015:UCH:2815400.2815402,Yang:2010:SLI:1806596.1806610}。
49 Gears OSでは、GearsAgda で直接に記述できる点が新しい。
50
18 この論文では、Gears OSのcodeGearの管理方法について考察する。 51 この論文では、Gears OSのcodeGearの管理方法について考察する。
19 52
20 --Normal and Meta computation 53 --Normal and Meta computation
21 54
22 Gears OSの基本は、CbC (Continuation based C)であり、input interfaceとoutput interfaceを有限な処理で 55 Gears OSの基本は、CbC (Continuation based C)\cite{cbc-github}であり、input interfaceとoutput interfaceを有限な処理で
23 結ぶものになっている。これは、コンパイラの基本ブロックに大体相当する。これはさらに、GearsAgdaの 56 結ぶものになっている。これは、コンパイラの基本ブロックに大体相当する。これはさらに、GearsAgdaの
24 Agdaで記述された invariant あるいは、表示的意味論と直結している。 57 Agdaで記述された invariant あるいは、表示的意味論と直結している。
25 58
26 CbCの記述は以下のようなものである。 59 CbCの記述は以下のようなものである。
27 60
36 この単位で行われ定義される。ハードウェアでの並行実行、割り込み処理などは、それにそって 69 この単位で行われ定義される。ハードウェアでの並行実行、割り込み処理などは、それにそって
37 実装される必要がある。これらは、GearsAgdaでは、外部環境へのアクセスがある。この場合は 70 実装される必要がある。これらは、GearsAgdaでは、外部環境へのアクセスがある。この場合は
38 時刻に対するアクセスである。 71 時刻に対するアクセスである。
39 72
40 OS側からみると、これは詳細のない単なるコードに見える。実行の詳細、つまり、実行に関係する 73 OS側からみると、これは詳細のない単なるコードに見える。実行の詳細、つまり、実行に関係する
41 すべての dataGear 、すべてのcodeGearは、プロセスに相当する Context metaDataGearに格納される。 74 すべての dataGear 、すべてのcodeGearは、プロセスに相当する Context metaDataGear(図\ref{Gears OS})に格納される。
42 75
43 つまり、OSからみた codeGearの実行は、 76 つまり、OSからみた codeGearの実行は、
44 77
45 　　Contextから詳細を取り出すmeta codeGearの番号から、codeGearを選ぶ 78 meta codeGearの番号から、codeGearを選ぶ
46 　　それを実行し、continuation としてshcedulerを指定する 79 　　それを実行し、continuation としてshcedulerを指定する
47 　　これを CPU worker 毎に実行する 80 　　これを CPU worker 毎に実行する
48 81
49 ということになる。CPU worker毎に Contextは一つなので、Contextはsingle threadで実行される。 82 ということになる。CPU worker毎に Contextは一つなので、Contextはsingle threadで実行される。
50 これにより、並行実行の単位はcodeGearとなる。 83 これにより、並行実行の単位はcodeGearとなる。
68 meta が書き換えられている場合は、ここで Context switchが起きることになる。 101 meta が書き換えられている場合は、ここで Context switchが起きることになる。
69 102
70 このContext switchでメモリ空間の切り替えが必要かどうかは application に依存する。 103 このContext switchでメモリ空間の切り替えが必要かどうかは application に依存する。
71 もし、codeGearの実行の正しさが証明されているなら、メモリ空間を切り替える必然性はない。 104 もし、codeGearの実行の正しさが証明されているなら、メモリ空間を切り替える必然性はない。
72 実際、Kernel 内や Realtime Monitor では切り替えない方が普通である。 105 実際、Kernel 内や Realtime Monitor では切り替えない方が普通である。
106
107 <center><img src="fig/gears_structure.pdf" alt="Gears OS"></center>
73 108
74 --証明付きのコード 109 --証明付きのコード
75 110
76 GearsAgdaで記述されていれば、codeGearやdataGearは証明を持つ。これらは単なる型なので実行時には 111 GearsAgdaで記述されていれば、codeGearやdataGearは証明を持つ。これらは単なる型なので実行時には
77 実態を持たない。ただし、それを実行時にチェックすることもできる。assertなどと同じ扱いである。 112 実態を持たない。ただし、それを実行時にチェックすることもできる。assertなどと同じ扱いである。
113 自分自身の codeGear の再帰呼び出しで行うと、codeGearの実行が有界な時間に閉じなくなる。 148 自分自身の codeGear の再帰呼び出しで行うと、codeGearの実行が有界な時間に閉じなくなる。
114 なので、loop は軽量継続を用いて、一旦、外にでることになる。これは、この段階でmeta level的に処理が 149 なので、loop は軽量継続を用いて、一旦、外にでることになる。これは、この段階でmeta level的に処理が
115 割り込まれることも意味している。 150 割り込まれることも意味している。
116 151
117 GearsAgda で処理された項は、ContextのdataGearに格納される。また、GearsAgdaのcodeGearは、 152 GearsAgda で処理された項は、ContextのdataGearに格納される。また、GearsAgdaのcodeGearは、
118 Contextのcode tableに格納される。どちらも、メモリ的には番号で管理されることになる。 153 Contextのcode table(図\ref{code table})に格納される。どちらも、メモリ的には番号で管理されることになる。
119 GearsAgda の Context は、その意味で、プロセスのメモリ空間そのものを抽象化したものになっている。 154 GearsAgda の Context は、その意味で、プロセスのメモリ空間そのものを抽象化したものになっている。
120 155
121 156
122 つまり、CbCのcodeGearと GearsAgdaは、normal level ではポインタを使わないのだが、 157 つまり、CbCのcodeGearと GearsAgdaは、normal level ではポインタを使わないのだが、
123 その意味は、CbCと GearsAgda で若干異なる。CbCでの実装は、GearsAgdaでの実装の持つ 158 その意味は、CbCと GearsAgda で若干異なる。CbCでの実装は、GearsAgdaでの実装の持つ
124 性質を保存する必要がある。 159 性質を保存する必要がある。
160
161 <center><img src="fig/codetable.pdf" alt="code table"></center>
125 162
126 --Contextを通した dataGearとcodeGearの連携 163 --Contextを通した dataGearとcodeGearの連携
127 164
128 Gears OSでは、Context はCの構造体であり、一つのContextで使用するdataGearとcodeGearは、そこに格納される。 165 Gears OSでは、Context はCの構造体であり、一つのContextで使用するdataGearとcodeGearは、そこに格納される。
129 複数のContextから、dataGearもcodeGearも共有されることがある。その排他制御は、Gears OSのmeta codeGearに 166 複数のContextから、dataGearもcodeGearも共有されることがある。その排他制御は、Gears OSのmeta codeGearに
152 dataGearもContextから参照される pool に確保される。これの管理は meta dataGear (Gears OSのkernel) 189 dataGearもContextから参照される pool に確保される。これの管理は meta dataGear (Gears OSのkernel)
153 が行う。GearsAgda は、この部分はAgdaが管理するので meta的な管理は行われない。しかし、 190 が行う。GearsAgda は、この部分はAgdaが管理するので meta的な管理は行われない。しかし、
154 Context を用いた並行実行の場合は、Context上での管理の問題が生じる。 191 Context を用いた並行実行の場合は、Context上での管理の問題が生じる。
155 192
156 193
194 --code table
195
196 contextの初期化の中で、code table に実際の codeGear stub へのポインタが初期化される。
197
198 context->code[C_add] = add_stub;
199 context->code[C_checkAndSetAtomicReference]
200 = checkAndSetAtomicReference_stub;
201 context->code[C_clearSingleLinkedQueue] = clearSingleLinkedQueue_stub;
202 context->code[C_clearSynchronizedQueue] = clearSynchronizedQueue_stub;
203 context->code[C_code1] = code1_stub;
204 context->code[C_createTask1] = createTask1_stub;
205 context->code[C_createTask2] = createTask2_stub;
206 context->code[C_decrementTaskCountTaskManagerImpl]
207 = decrementTaskCountTaskManagerImpl_stub;
208 context->code[C_exit_code] = exit_code_stub;
209 context->code[C_getTaskCPUWorker] = getTaskCPUWorker_stub;
210 context->code[C_incrementTaskCountTaskManagerImpl]
211 = incrementTaskCountTaskManagerImpl_stub;
212
213 interfaceの初期化の中で、この番号が interfaceを表す dataGearに格納される。
214
215 Tree* createRedBlackTree(struct Context* context) {
216 struct Tree* tree = &ALLOCATE(context, Tree)->Tree;
217 struct RedBlackTree* redBlackTree
218 = &ALLOCATE(context, RedBlackTree)->RedBlackTree;
219 tree->tree = (union Data*)redBlackTree;
220 redBlackTree->root = NULL;
221 redBlackTree->nodeStack = createSingleLinkedStack(context);
222 tree->put = C_putRedBlackTree;
223 tree->get = C_getRedBlackTree;
224 tree->remove = C_removeRedBlackTree;
225 return tree;
226 }
227
228 この辺の構造は、GearsAgda 側では簡素化されている。実際、pointer を直接操作しないとかも、厳密に守る必要はなく、
229 GearsAgda と CbC での実装が平行していれば問題はない。
230
157 --codeGearのlinkage 231 --codeGearのlinkage
158 232
159 Gears OSのあらゆるコードは、codeGear DBのコードの組み合わせになる。しかし、そのためには、 233 Gears OSのあらゆるコードは、codeGear DBのコードの組み合わせになる。しかし、そのためには、
160 Contextから詳細なデータを取り出して、実行し、次のcodeGearを呼び出す時にContextの正しい場所にdataGearを格納する 234 Contextから詳細なデータを取り出して、実行し、次のcodeGearを呼び出す時にContextの正しい場所にdataGearを格納する
161 必要がある。これは codeGear 全体に対して必要になる。 235 必要がある。これは codeGear 全体に対して必要になる。
162 236
163 現状では、これは stubとしてコンパイル時に生成される。 237 現状では、これは stubとしてコンパイル時に生成される。
164 238
165 __code checkAndSetAtomicReference(struct AtomicReference* atomic, union Data** ptr, union Data* oldData, union Data* newData, __code next(...), __code fail(...)) { 239 __code checkAndSetAtomicReference(struct AtomicReference* atomic,
240 union Data** ptr, union Data* oldData, union Data* newData, __code next(...),
241 __code fail(...)) {
166 if (__sync_bool_compare_and_swap(ptr, oldData, newData)) { 242 if (__sync_bool_compare_and_swap(ptr, oldData, newData)) {
167 goto next(...); 243 goto next(...);
168 } 244 }
169 goto fail(...); 245 goto fail(...);
170 } 246 }
180 enum Code next; 256 enum Code next;
181 enum Code fail; 257 enum Code fail;
182 } Atomic; 258 } Atomic;
183 259
184 __code checkAndSetAtomicReference_stub(struct Context* context) { 260 __code checkAndSetAtomicReference_stub(struct Context* context) {
185 AtomicReference* atomic = (AtomicReference*)GearImpl(context, Atomic, atomic); 261 AtomicReference* atomic = (AtomicReference*)
262 GearImpl(context, Atomic, atomic);
186 Data** ptr = Gearef(context, Atomic)->ptr; 263 Data** ptr = Gearef(context, Atomic)->ptr;
187 Data* oldData = Gearef(context, Atomic)->oldData; 264 Data* oldData = Gearef(context, Atomic)->oldData;
188 Data* newData = Gearef(context, Atomic)->newData; 265 Data* newData = Gearef(context, Atomic)->newData;
189 enum Code next = Gearef(context, Atomic)->next; 266 enum Code next = Gearef(context, Atomic)->next;
190 enum Code fail = Gearef(context, Atomic)->fail; 267 enum Code fail = Gearef(context, Atomic)->fail;
191 goto checkAndSetAtomicReference(context, atomic, ptr, oldData, newData, next, fail); 268 goto checkAndSetAtomicReference(context, atomic,
269 ptr, oldData, newData, next, fail);
192 } 270 }
193 271
194 これらは単一のGears OS内で整合する必要がある。実際には、これらは、stubが参照する Context内のoffsetにすぎない。 272 これらは単一のGears OS内で整合する必要がある。実際には、これらは、stubが参照する Context内のoffsetにすぎない。
195 Atomic は dataGear の巨大な Union になっている。これは、GearsAgda でも状況は同じで、巨大な Sum type になっている。 273 Atomic は dataGear の巨大な Union になっている。これは、GearsAgda でも状況は同じで、巨大な Sum type になっている。
196 274
219 297
220 codeGear単位で正直に分割コンパイルすると最適化の余地がない。しかし、その場合でもJITなどは可能である。 298 codeGear単位で正直に分割コンパイルすると最適化の余地がない。しかし、その場合でもJITなどは可能である。
221 299
222 --boot codeGear 300 --boot codeGear
223 301
224 今の実装では、UEFIから Gears OSが読み出される。Gears OS自体は、x.v6\cite{}と同じで、ファイルシステムを 302 今の実装では、UEFIから Gears OSが読み出される。Gears OS自体は、x.v6\cite{xv6rpi}と同じで、ファイルシステムを
225 含む一体の binary になっている。 303 含む一体の binary になっている。
226 304
227 codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。 305 codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。
228 306
229 307