Mercurial > hg > Papers > 2023 > matac-sigos
view marp-slide/slide.md @ 40:2e2ddc184572
...
| author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 13 May 2023 16:03:48 +0900 |
| parents | a246b64a1b2d |
| children | efea60e8455a |
line wrap: on
line source
--- marp: true theme: cr paginate: true --- # Gears OSのファイルシステムとDB <!-- スピーカーノート --> 琉球大学 理工学研究科 知能情報プログラム 河野研究室 又吉 雄斗, 佐野 巧曜, 河野 真治 --- ## システム全体の信頼性を上げたい - システムの構成要素全体の信頼性を上げる必要がある - アプリケーション - OS - ファイルシステム - DB - メモリとSSD - 分散ノード - ネットワーク --- ## Gears OSを使って実現する - CodeGear - 処理の単位 - DataGear - データの単位 - metaGear - データの整合性 - 資源管理 --- ## 信頼性を上げる方法 - 証明 - GearsAgdaを使ってinvariantを証明する - テスト - モデル検査 - システムの構成要素全体にこれらの方法を適用したい --- ## FSとDBの要素をRBTreeに対応させる - ファイルシステムとDBをRedBlackTreeで統一する - RedBlackTreeはinvariantで証明する --- ## Continuation based C - Cの下位言語である - 処理の単位 CodeGear - データの単位 DataGear - ノーマルレベルとメタレベルの切り分け - gotoによる軽量継続 --- ## CodeGearとmetaCodeGearの関係 - ノーマルレベルとメタレベルの存在  --- ## Context - Gears OS上全てのCodeGear，DataGearの参照を持つ - OS上の処理の実行単位 - プロセスに相当 - Gearの概念ではmetaDataGearに当たる - ノーマルレベルから直接参照されない - metaCodeGearから参照される --- ## 3種類のGears OS - GearsAgda(Agda) - 形式手法による信頼性の向上 - Gears OS(CbC) - ユーザーレベルタスクマネージメント - CbC x.v6 ← 今回の実装対象 - スタンドアロンOS --- ## CodeGear遷移の流れ  --- ## ファイルシステムとDB - 両方ともRedBlackTreeで実装する - 本質的な役割は一緒 - 信頼性の向上 - 証明のしやすさ - 非破壊Tree - データの持続性 --- ## 非破壊的なRedBlackTree  --- ## RedBlackTreeはDBのテーブル - テーブルのキーがRedBlackTreeのkey - トランザクションはテーブルのルートの置き換え - 複数の書き込みポイント  --- ## データの持続性 - オンメモリーなRedBlackTree - SSD上のコピー - ログ的にコピーしていく - Copying GC --- ## スキーマ - DBの各テーブルのレコードの型定義 - Contextに登録されているDataGearの型 - キーを用いたDataGearの参照 --- ## インピーダンスミスマッチ - プログラムで使用するデータ構造 - queue - stack - DBにはリストやキューは入らない - 第一正規系でないから - データ構造を持続的にしたい - なのでファイルシステムが必要 --- ## RedBlackTreeベースのファイルシステム - i-node番号をkeyにする - inodeにはDGのリストが入る - 持続性 - オンメモリーなRedBlackTree - SSD上のコピー - ログ的にコピーしていく --- ## バックアップとロールバック - ロールバックの必要性 - トランザクションの失敗 - システムクラッシュ - SSDのログからロールバックする - Copying GCによるバックアップ - ルートノードがデータのバージョン --- ## 構成要素 - すべてRedBlackTreeで構成されている - 検証はRedBlackTreeだけで良い - invariantで証明する - RedBlackTreeによる権限の表現 - metaDGで行う - ContextからアクセスできるRedBlackTreeがある --- ## 信頼性の保証 - RedBlackTreeの変更の正しさ - トランザクションの正しさ - アクセス権限の正しさ - SSDへのコピーの正しさ - ポータビリティ - 異なる計算機アーキテクチャ - 異なるエンコード - 異なる分散ノード - 正しくスキーマに対応しているかどうか - 違反しても良い --- ## 今後の課題 - データクエリ言語 - SQL - SQLより良いものが欲しい - ファイルシステムとDBの両方で使える - 時系列データ - データ圧縮 - スタンドアロンなDB - ポータビリティ <!-- - CodeGearがDataGearを受け取り，処理後にDataGearを次のCodeGearに渡すという動作をしているように見える - 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し，それらの計算はMetaCodeGearで行われる --> <!-- ## RedBlackTreeを用いたFSの構築 - Gears OSへファイルシステムを実装するにあたり，RedBlackTreeを用いる - DBはファイルシステムと本質的に同じ役割を持っているため，同じRedBlackTreeでDBも表現することが可能であると考える ### Gears OSにおけるDBの機能を持ち合わせたファイルシステムの設計を</br>信頼性の向上と， RedBlackTreeのみのシンプルな構造を基軸として考える --- ## 非破壊的な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 -->