Mercurial > hg > Papers > 2024 > matac-master
view marp-slide/slide.md @ 73:c4b013299ff6
outline(slide & poster)
| author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 13 Feb 2024 20:25:58 +0900 |
| parents | b2a541a2c178 |
| children | 8c087f2ae631 |
line wrap: on
line source
--- marp: true theme: cr paginate: true --- <!-- 全体の流れ - 目的 - 基礎概念 - 問題提起 -> 解決 の繰り返し - 評価 --> # GearsOSのファイルシステムにおける GCとレプリケーション <!-- スピーカーノート --> 琉球大学 理工学研究科 工学専攻 知能情報プログラム 河野研究室 又吉 雄斗 --- <!-- 目的 --> ## システム全体の信頼性を上げたい - システムの構成要素全体の信頼性を上げる必要がある - アプリケーション - OS - ファイルシステム - DB - メモリとSSD - 分散ノード - ネットワーク --- ## Gears OSを使って実現する - CodeGear - 処理の単位 - DataGear - データの単位 - metaGear - データの整合性 - 資源管理 --- ## 信頼性を上げる方法 - 証明 - GearsAgdaを使ってinvariantを証明する - テスト - モデル検査 - システムの構成要素全体にこれらの方法を適用したい - 既存システムの信頼性における問題点の解決 --- <!-- ここからGears OSの基礎概念だと明示する --> ## Continuation based C - Cの下位言語である - 処理の単位 CodeGear - データの単位 DataGear - ノーマルレベルとメタレベルの切り分け - gotoによる軽量継続 --- ## CodeGearとmetaCodeGearの関係 - ノーマルレベルとメタレベルの存在  --- ## Context - Gears OS上全てのCodeGear，DataGearの参照を持つ - OS上の処理の実行単位 - プロセスに相当 - Gearの概念ではmetaDataGearに当たる - ノーマルレベルから直接参照されない - metaCodeGearから参照される --- ## 3種類のGears OS - GearsAgda(Agda) - 形式手法による信頼性の向上 - CbC x.v6 - スタンドアロンOS - Gears OS(CbC) ← 今回の実装対象 - ユーザーレベルタスクマネージメント --- ## GearsAgdaとGearsOSの対応 - GearsOSのCodeGearと直接対応している - GearsAgdaでRedBlackTreeの証明が進められている - find完了、insert証明中 - GearsOSの構造はRedBlackTreeが多くを占める GearsAgdaでRedBlackTreeが証明できれば、GearsOSの大部分を証明したことになる --- ## CodeGear遷移の流れ  --- ## 非破壊RedBlackTree  --- <!-- ここまでがGears OSの基礎概念だと明示する --> ## GearsFilesystem - GearsOSで書かれたファイルシステム - i-nodeによるディレクトリシステム - 分散ファイルシステムの通信機能 - 非破壊RedBlackTreeで構成される - ディスク上とメモリ上のデータ構造を統一する --- ## ファイルシステムの信頼性 - 電源断時にデータが残るpersistency - データを書き込めたかどうかを判定するatomic write - ノード喪失時にデータを保護する多重性 - 複数のコピーを調停するコミット機構 --- ## メモリ管理や多重性の機能がない メモリ管理 - GC(ガベージコレクション) 多重性 - レプリケーション - バックアップ --- ## メモリ管理や多重性の機能の要件 - データの持続性 - 証明のしやすさの維持 - データを破壊しない - 非破壊RedBlackTreeの増大抑制 - 非破壊RedBlackTreeは履歴を全て持つ - そのままにすると増大し、メモリを圧迫する --- ## GearsOSにおけるGC CopyingGCを採用する --- ## GearsOSにおけるレプリケーション 単純に木をコピーする --- ## copyRedBlackTreeの実装をした - RedBlackTreeのコピーを行う - GCやレプリケーションの機能のために木のコピーが必要 --- ## copyRedBlackTreeによって出来ること 多重性やメモリ管理に関する機能を追加できる GC(defragmentation) レプリケーション バックアップ --- ## Tree InterfaceのAPIとして実装 --- ## コピーのアルゴリズム詳細  --- ## アロケーション部分  --- ## swap  --- ## 実行方法 --- ## 評価 非破壊RedBlackTreeの増大抑制できる コピーするだけなので木が持続的 課題点 同一Contextへコピーしている コピーの正しさ --- ## 今後の研究方針 別Contextコピー GC，レプリケーションの実装 多重性以外の機能 --- ## まとめ copyRedBlackTreeを実装した それにより多重性を確保できるようになった 多重性はシステムの信頼性を向上させる 非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった