Mercurial > hg > Papers > 2023 > nana-sigos

comparison code-mangement.ind @ 2:42df4feebde2

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 Sat, 15 Apr 2023 16:30:15 +0900
parents 664ad87c2740
children c0d369375b21
comparison
equal deleted inserted replaced
1:664ad87c2740 2:42df4feebde2
82 82
83 codeはContextの表に登録されるが、システム全体のcodeは Database で管理される。その管理は 83 codeはContextの表に登録されるが、システム全体のcodeは Database で管理される。その管理は
84 ファイルシステム上でも良い。codeは証明が付属している場合もあるが、それは何らかの形で 84 ファイルシステム上でも良い。codeは証明が付属している場合もあるが、それは何らかの形で
85 codeGear Databseに格納される。 85 codeGear Databseに格納される。
86 86
87 現状では、証明はAgdaで記述されたデータ構造でしかない。それをcodeGear DBに入れても利用する方法は
88 ないがいくつかの利用法は考えられる。
87 89
90 証明とcodeGearの一致を確認する
91 型整合に使う
92 codeの認証に使う
88 93
94 この大域のcodeGear DBは、kernelを含めたすべてのcodeGearに対するもので全部で共有される。つまり、
95 あらゆるversionを含む共有ライブラリとなる。これは全世界でuniqueなDBとしても良い。
89 96
97 --codeGearのlinkage
90 98
99 Gears OSのあらゆるコードは、codeGear DBのコードの組み合わせになる。しかし、そのためには、
100 Contextから詳細なデータを取り出して、実行し、次のcodeGearを呼び出す時にContextの正しい場所にdataGearを格納する
101 必要がある。これは codeGear 全体に対して必要になる。
91 102
92 --並列実行 103 現状では、これは stubとしてコンパイル時に生成される。
93 104
94 --code table 105 __code checkAndSetAtomicReference(struct AtomicReference* atomic, union Data** ptr, union Data* oldData, union Data* newData, __code next(...), __code fail(...)) {
106 if (__sync_bool_compare_and_swap(ptr, oldData, newData)) {
107 goto next(...);
108 }
109 goto fail(...);
110 }
95 111
96 --dynamic loading 112 では、Context 上には以下の構造と、それを呼び出す stub がある。
97 113
98 --実装 114 struct Atomic {
115 union Data* atomic;
116 union Data** ptr;
117 union Data* oldData;
118 union Data* newData;
119 enum Code checkAndSet;
120 enum Code next;
121 enum Code fail;
122 } Atomic;
99 123
100 --linkの方法 124 __code checkAndSetAtomicReference_stub(struct Context* context) {
125 AtomicReference* atomic = (AtomicReference*)GearImpl(context, Atomic, atomic);
126 Data** ptr = Gearef(context, Atomic)->ptr;
127 Data* oldData = Gearef(context, Atomic)->oldData;
128 Data* newData = Gearef(context, Atomic)->newData;
129 enum Code next = Gearef(context, Atomic)->next;
130 enum Code fail = Gearef(context, Atomic)->fail;
131 goto checkAndSetAtomicReference(context, atomic, ptr, oldData, newData, next, fail);
132 }
133
134 これらは単一のGears OS内で整合する必要がある。実際には、これらは、stubが参照する Context内のoffsetにすぎない。
135 Atomic は dataGear の巨大な Union になっている。これは、GearsAgda でも状況は同じで、巨大な Sum type になっている。
136
137 このContext内での offsetと呼び出すcodeGearの番号が一致すれば、Kernel側で整合性の問題はない。
138
139 --static linkage
140
141 コンパイル時に codeGearの結合が明らかならば、それは一つのcodeGearとしてまとめてよい。Contextへの書き込みもさぼることが
142 可能になる。ただし、時分割実行される場合は、codeGearの切れ目で分割するのと同じ実行が要求される。
143 つまり、割り込み処理などで途中で実行が中断するならば、それはその単位まで実行してから、Contextを切り替える必要がある。
144
145 これを実現する手法はflagを参照する方法や、コードを書き換える方法あるいは、polingを埋め込むなどの方法が考えられる。
146 整合性が不要であれば途中で止めても問題ないが、その場合は register などの状態を従来のOSのように保持する必要がある。
147
148 codeGear単位で正直に分割コンパイルすると最適化の余地がない。しかし、その場合でもJITなどは可能である。
149
150 --boot codeGear
151
152 今の実装では、UEFIから Gears OSが読み出される。Gears OS自体は、x.v6\cite{}と同じで、ファイルシステムを
153 含む一体の binary になっている。
154
155 codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。
101 156
102 --まとめ 157 --まとめ