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