Mercurial > hg > Papers > 2023 > matac-sigos
view marp-slide/slide.md @ 38:162915cd51be
kono advice
| author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 May 2023 19:17:03 +0900 |
| parents | 9935613ddc4a |
| children | a246b64a1b2d |
line wrap: on
line source
--- marp: true theme: cr paginate: true --- # Gears OSのファイルシステムとDB <!-- スピーカーノート --> 琉球大学 理工学研究科 知能情報プログラム 河野研究室 ### 又吉 雄斗, 佐野 巧曜, 河野 真治 --- ## システム全体の信頼性を上げたい - システムの構成要素全体の信頼性を上げる必要がある - アプリケーション - OS - ファイルシステム - DB - メモリとSSD - 分散ノード - ネットワーク --- ## Gears OSを使って実現する - CodeGear - DataGear - metaGear --- ## 信頼性を上げる方法 - 証明 - GearsAgdaを使ってinvariantを証明する - テスト - - モデル検査 --- ## Gears OS <!-- - アプリケーションの信頼性を保証するために， アプリケーションが動作するOSの信頼性を高める必要がある - 信頼性確保の方法として定理証明やモデル検査がある - 当研究室では，信頼性の保証を目的としたGears OSを開発している - 証明や検証を容易に行えるよう，ファイルシステムのシンプルな実装を考えたい --> --- ## RedBlackTreeを用いたFSの構築 - Gears OSへファイルシステムを実装するにあたり，RedBlackTreeを用いる - DBはファイルシステムと本質的に同じ役割を持っているため，同じRedBlackTreeでDBも表現することが可能であると考える ### Gears OSにおけるDBの機能を持ち合わせたファイルシステムの設計を</br>信頼性の向上と， RedBlackTreeのみのシンプルな構造を基軸として考える --- ## 信頼性の保証を目的としたOS ### 3種類のGears OS - GearsAgda(Agda) - 形式手法による信頼性の向上 - Gears OS(CbC) - ユーザーレベルタスクマネージメント - CbC x.v6 ← 今回の実装対象 - スタンドアロンOS --- ## Gears OS(CbC x.v6) - 当研究室にて，信頼性と拡張性の両立を目的として開発している - CbCで記述されている - Gearという概念があり，実行の単位をCodeGear，データの単位をDataGearと呼ぶ - ノーマルレベルとメタレベルの処理を切り分けることが容易にできる --- ## CodeGearとmetaCodeGearの関係 ### ノーマルレベルとメタレベルの存在 - CodeGearがDataGearを受け取り，処理後にDataGearを次のCodeGearに渡すという動作をしているように見える - 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し，それらの計算はMetaCodeGearで行われる --- ## CodeGearとmetaCodeGearの関係  --- ## Context - Gears OS上全てのCodeGear，DataGearの参照を持つ - OS上の処理の実行単位 - Gearの概念ではMetaDataGearに当たる - ノーマルレベルから直接参照されず，必ずMetaDataGearとしてMetaCodeGearから参照される --- ## CodeGear遷移の流れ  --- ## 非破壊的なRedBlackTree - Gears OSにおける永続データは非破壊的な編集を行うRedBlackTreeを用いて保存する - ディレクトリシステム自体にバックアップの機能を搭載することが可能と考える --- ## 非破壊的なRedBlackTree  --- ## ディスク上とメモリ上のデータ構造 - ディスク上とメモリ上でデータの構造は，RedBlackTreeに統一する - ブロックアクセス数の観点ではRedBlackTreeはB-Treeに劣る - しかしながら，SSDはランダムアクセスによってデータにアクセスするため，RedBlackTreeでなくB-Treeを用いる利点は少ないと考える - データ構造を統一することで，ディスク上とメモリ上のデータのやりとりは単純なコピーで実装できる --- ## データのロールバックとバックアップ - RDBのロールバックは，コミットするまではトランザクションの開始時点に戻ることができる機能を持つ - ロールバックはコミットが完了するとそれ以前の状態に戻すことはできないが，データのバックアップをとっておくことで復元を行う - このような，ロールバックとバックアップの仕組みをファイルシステムに実装したい --- ## データのロールバックとバックアップ - RedBlackTreeのルートノードがデータのバージョンの役割を果たしていることを利用する - 非破壊的なTree編集はアップデートのたびに，ルートノードを増やす - つまり，ルートノードはアップデートのログと言えその時点のデータのバージョンを表していると考えることができる - よって，ロールバックを行いたい場合は参照を過去のルートノードに切り替える --- ## データのロールバックとバックアップ - ルートノードはデータのアップデート時に増えるため，データが際限なく増加していく問題がある - この問題はCopyingGCを行うことによって解決する - まず，RedBlackTreeを丸ごとコピーして最新のルートを残して他のルートは削除する - その後，コピーしたものはバックアップないしログとしてディスクに書き込む - データの増加によるリソースの枯渇を防ぎ，かつデータのログ付きバックアップを作成することで信頼性の向上が期待できる --- ## トランザクション - トランザクションはDBの重要な機能の一つである - データの競合を防ぎ信頼性を向上させるために，トランザクションの仕組みを考える必要がある - ファイルシステムは全てRedBlackTreeで実装するため，RedBlackTreeのノードに対するトランザクションを考える - トランザクションをwriteとreadに分けて考える --- ## トランザクション ### writeする場合 - トランザクションはRedBlackTreeのルートの置き換えと対応する - writeするために，まずルートを生やし書き込みが終わった後ルートを置き換える - ルートの置き換えは競合的なので，複数プロセスから同時に書き込みを行っても1つしか成功しない - 単一のRedBlackTreeに複数の書き込みポイントを作り，並行実行可能にする必要がある --- ## トランザクション ### 複数の書き込みポイント - RedBlackTreeに複数の書き込みポイントを作るために，キーごとのルートを作成する - ノードはそれぞれがキーとRedBlackTreeを持つ状態になる - writeする際は，そのキーのルートを置き換える --- ## トランザクション - Aの木はファイルシステム全体を表すRedBlackTreeである - ノードNのデータに対して書き込みすることを考える - キーがaであるBの木のルートからロックしCの木を作成して，Bの木からCの木のルートに入れ替えることで書き込みを行う  --- ## トランザクション ### readする場合 - readはデータに変更を加えないため，複数同時に同じノードを読み込むことが可能である - しかし，常に最新の情報を読み込めるとは限らない - 最新の情報が欲しい場合は書き込みを一旦止めるような処理が必要になる --- ## ファイルシステムにおけるスキーマ - Gears OSのデータは全てDataGearで表されるため，Gears OSにおけるファイルシステムはDataGearの集合となる - Gears OSにおけるスキーマとはDataGear上のキーの構成であることがわかる - 今回のRedBlackTreeによる構成の場合，キーはRedBlackTreeを指す - KernelのContext上にキーを用いたDataGearの参照を書き込む --- ## 権限の表現 - ファイルの権限はファイルシステムの重要な機能の一つである - 今回のRedBlackTreeによる構成の場合，木のルートの所持者を設定することがファイルに対して権限を設定することにあたる - ルートに対してアクセスする権限がなければ，読み書きができないといった実装になると考える --- ## 今後の課題・展望 - データクエリ言語 - 時系列データ - スタンドアロンDB