Mercurial > hg > Papers > 2024 > matac-master
comparison marp-slide/slide.md @ 77:5847cf59e9b3
...
author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 14 Feb 2024 13:49:06 +0900 |
parents | 13969295f118 |
children | 4ab8a9a8389a |
comparison
equal
deleted
inserted
replaced
76:13969295f118 | 77:5847cf59e9b3 |
---|---|
81 | 81 |
82 --- | 82 --- |
83 | 83 |
84 ## Context | 84 ## Context |
85 | 85 |
86 - Gears OS上全てのCodeGear,DataGearの参照を持つ | 86 - Gears OS上全てのCodeGear、DataGearの参照を持つ |
87 - OS上の処理の実行単位 | 87 - OS上の処理の実行単位 |
88 - プロセスに相当 | 88 - プロセスに相当 |
89 - Gearの概念ではmetaDataGearに当たる | 89 - Gearの概念ではmetaDataGearに当たる |
90 - ノーマルレベルから直接参照されない | 90 - ノーマルレベルから直接参照されない |
91 - metaCodeGearから参照される | 91 - metaCodeGearから参照される |
92 | |
93 --- | |
94 | |
95 ## CodeGear遷移の流れ | |
96 | |
97 ![w:1100](figs/context.svg) | |
92 | 98 |
93 --- | 99 --- |
94 | 100 |
95 ## 3種類のGears OS | 101 ## 3種類のGears OS |
96 | 102 |
109 - GearsAgdaでRedBlackTreeの証明が進められている | 115 - GearsAgdaでRedBlackTreeの証明が進められている |
110 - find完了、insert証明中 | 116 - find完了、insert証明中 |
111 - GearsOSのファイルシステムの構造はRedBlackTreeが多くを占める | 117 - GearsOSのファイルシステムの構造はRedBlackTreeが多くを占める |
112 | 118 |
113 GearsAgdaでRedBlackTreeが証明できれば、GearsOSのファイルシステムの大部分を証明したことになる | 119 GearsAgdaでRedBlackTreeが証明できれば、GearsOSのファイルシステムの大部分を証明したことになる |
114 | |
115 --- | |
116 | |
117 ## CodeGear遷移の流れ | |
118 | |
119 ![w:1100](figs/context.svg) | |
120 | 120 |
121 --- | 121 --- |
122 | 122 |
123 ## 非破壊RedBlackTree | 123 ## 非破壊RedBlackTree |
124 | 124 |
181 | 181 |
182 --- | 182 --- |
183 | 183 |
184 ## GearsOSのGC | 184 ## GearsOSのGC |
185 | 185 |
186 CopyingGCのような仕組み | 186 - CopyingGCのような仕組み |
187 | |
188 - 新しいContextのメモリに新規にコピーする | 187 - 新しいContextのメモリに新規にコピーする |
189 - 古いContextをそのまま全部解放する | 188 - 古いContextをそのまま全部解放する |
190 | 189 |
191 ![bg right:52% 95%](figs/copy_context.svg) | 190 ![bg right:52% 85%](figs/copy_context.svg) |
192 | 191 |
193 --- | 192 --- |
194 | 193 |
195 ## GearsOSの レプリケーション | 194 ## GearsOSの レプリケーション |
196 | 195 |
197 - 複数のストレージに同時に木をコピーする | 196 - 複数のストレージに同時に木をコピーする |
198 - そのうちの一部は持続的なストレージにする | 197 - そのうちの一部は持続的なストレージにする |
199 - システム起動時には必要な分をメモリにコピーする | 198 - システム起動時には必要な分をメモリにコピーする |
200 | 199 - トランザクションも考慮する |
201 トランザクションも考慮する | 200 |
202 | 201 ![bg right:48% 85%](figs/copy_context.svg) |
203 ![bg right:48% 95%](figs/copy_context.svg) | |
204 | 202 |
205 --- | 203 --- |
206 | 204 |
207 ## RedBlackTreeの トランザクション | 205 ## RedBlackTreeの トランザクション |
208 | 206 |
209 - トランザクションはのルートの置き換え | 207 - トランザクションはルートの置き換え |
210 - 複数の書き込みポイント | 208 - 複数の書き込みポイント |
211 - 最新の情報が欲しい場合は書き込み停止処理が必要 | 209 - 最新の情報が欲しい場合は書き込み停止処理が必要 |
212 | 210 |
213 ![bg right:45% 65%](figs/transaction.svg) | 211 ![bg right:45% 65%](figs/transaction.svg) |
214 | 212 |
243 | 241 |
244 - left方向へ深さ優先探索を行う | 242 - left方向へ深さ優先探索を行う |
245 - 2つのStackを使用する | 243 - 2つのStackを使用する |
246 - nodeStackは元の木を辿る | 244 - nodeStackは元の木を辿る |
247 - toStackは新しい木を操作 | 245 - toStackは新しい木を操作 |
248 - 大まかにleftDown, rightDown, upの3ステップ | 246 - 大まかにleftDown, rightDown, upの3つの動作 |
249 | 247 |
250 ![bg right:45% 65%](figs/copy_algo4.svg) | 248 ![bg right:45% 65%](figs/copy_algo4.svg) |
251 | 249 |
252 --- | 250 --- |
253 | 251 |
301 - 同一Context上での動作になっている | 299 - 同一Context上での動作になっている |
302 | 300 |
303 ![bg right:50% 90%](figs/swap.svg) | 301 ![bg right:50% 90%](figs/swap.svg) |
304 | 302 |
305 --- | 303 --- |
306 | 304 <!-- |
307 ## 実行方法 | 305 ## 実行方法 |
308 | 306 |
309 --- | 307 --- --> |
310 | 308 |
311 ## 評価 | 309 ## 評価 |
312 | 310 |
313 - 非破壊RedBlackTreeの増大抑制できる | 311 - 非破壊RedBlackTreeの増大抑制できる |
314 - コピーで木の持続性を確保できる | 312 - コピーで木の持続性を確保できる |
327 ## 今後の研究方針 | 325 ## 今後の研究方針 |
328 | 326 |
329 - 別Contextコピー | 327 - 別Contextコピー |
330 - GearsAgdaでの記述 | 328 - GearsAgdaでの記述 |
331 - Stack領域の圧縮 | 329 - Stack領域の圧縮 |
332 - Stackの再利用? | 330 - Stackの再利用 |
333 - GC,レプリケーションの実装 | 331 - GC、レプリケーションの実装 |
334 - 多重性以外の機能 | 332 - 多重性やメモリ管理以外の機能の実装 |
335 | 333 |
336 --- | 334 --- |
337 | 335 |
338 ## まとめ | 336 ## まとめ |
339 | 337 |