Mercurial > hg > Papers > 2023 > matac-sigos
view marp-slide/slide.md @ 29:587197c3aa09
transaction
author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 12 May 2023 16:32:47 +0900 |
parents | 30fc12d776f1 |
children | ce4af0b4df9d |
line wrap: on
line source
--- marp: true theme: cr paginate: true --- # GearsOSのファイルシステムとDB <!-- スピーカーノート --> 琉球大学 理工学研究科 知能情報プログラム 河野研究室 ### 又吉 雄斗, 佐野 巧曜, 河野 真治 --- ## 研究目的 - アプリケーションの信頼性を保証するために, アプリケーションが動作するOSの信頼性を高める必要がある - 信頼性確保の方法として定理証明やモデル検査がある - 当研究室では,信頼性の保証を目的としたGearsOSを開発している - 証明や検証を容易に行えるよう,ファイルシステムのシンプルな実装を考えたい --- ## RedBlackTreeを用いたFSの構築 - GearsOSへファイルシステムとDBを実装するにあたり,RedBlackTreeを用いる - DBはファイルシステムと本質的に同じ役割を持っているため 同じRedBlackTreeで表現することが可能であると考える - よって,今回はGearsOSにおけるファイルシステムとDBをRedBlackTreeで実装するための設計を行う --- ## 信頼性の保証を目的としたOS ### 3種類のGears OS - GearsAgda(Agda) - 形式手法による信頼性の向上 - GearsOS(CbC) - ユーザーレベルタスクマネージメント - CbC x.v6 ← 今回の実装対象 - スタンドアロンOS --- ## Gears OS(CbC x.v6) - 当研究室にて,信頼性と拡張性の両立を目的として開発している - CbCで記述されている - Gearという概念があり,実行の単位をCodeGear,データの単位をDataGearと呼ぶ - ノーマルレベルとメタレベルの処理を切り分けることが容易にできる --- ## CodeGearとmetaCodeGearの関係 ### ノーマルレベルとメタレベルの存在 - CodeGearがDataGearを受け取り,処理後にDataGearを次のCodeGearに渡すという動作をしているように見える - 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し,それらの計算はMetaCodeGearで行われる --- ## CodeGearとmetaCodeGearの関係 ![w:1100](figs/meta_cg_dg.svg) --- ## Context - GearsOS上全てのCodeGear,DataGearの参照を持つ - OS上の処理の実行単位 - Gearの概念ではMetaDataGearに当たる - ノーマルレベルから直接参照されず,必ずMetaDataGearとしてMetaCodeGearから参照される --- ## CodeGear遷移の流れ ![w:1100](figs/context.svg) --- ## 非破壊的なRedBlackTree - GearsOSにおける永続データは非破壊的な編集を行うRedBlackTreeを用いて保存する - ディレクトリシステム自体にバックアップの機能を搭載することが可能と考える --- ## 非破壊的なRedBlackTree ![w:1100](figs/nondestructive_tree_modification.png) --- ## ディスク上とメモリ上のデータ構造 - ディスク上とメモリ上でデータの構造は,RedBlackTreeに統一する - ブロックアクセス数の観点ではRedBlackTreeはB-Treeに劣る - しかしながら,SSDはランダムアクセスによってデータにアクセスするため,RedBlackTreeでなくB-Treeを用いる利点は少ないと考える. - よって,ディスク上とメモリ上のデータ構造をRedBlackTreeに統一することが考えられる. - そうすることによって,ディスク上とメモリ上のデータのやりとりは単純なコピーで実装できる. <!-- --- ## データのロールバックとバックアップ DBの重要な機能の一つにロールバックがある. 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の木のルートに入れ替えることで書き込みを行う ![bg right:45% 65%](figs/transaction.svg) --- ## トランザクション ### readする場合 - readはデータに変更を加えないため,複数同時に同じノードを読み込むことが可能である - しかし,常に最新の情報を読み込めるとは限らない - 最新の情報が欲しい場合は書き込みを一旦止めるような処理が必要になる <!-- --- ## ファイルシステムにおけるスキーマ 従来のRDBのようなスキーマが存在すると, 個別にバックアップなどを取らない限り スキーマの変更以前にロールバックすることができない. しかしながら,実際運用する上でスキーマを変更することは多々ある. これは,データの信頼性を低下させると考える. また,DB上のデータ構造とプログラム上で扱うデータ構造に差が生まれる インピーダンスミスマッチが発生し,DBのデータをプログラムが扱う際に その差を埋めるような変換を必要とする場合が生まれる. 一方で,スキーマがあることによってデータに対して高度な操作を行うことができ, また,インデックスを容易に作成することができるといったメリットがある. よって,スキーマフルなDBとスキーマレスなDBはそれぞれメリットデメリットがあり, 状況によって使い分けるのが良いと考える. 今回は,非構造化データ内であれば構造化データを扱うことが可能であることと, 信頼性を保証したいという点から, スキーマレスなDBとしてのファイルシステムを考える. しかしながら,トランザクションの仕組みを作る上でRedBlackTreeに対し, キーを設定することから完全なスキーマレスとは言えない構成となる. GearsOSのデータは全てDataGearで表される. よって,GearsOSにおけるファイルシステムはDataGearの集合となる. スキーマレスとはキーがない状態のことといえるが, DataGearはキーが設定されていないため,その集合自体にスキーマは無い. そのことから,GearsOSにおけるスキーマとはDataGear上のキーの構成であることがわかる. なお,今回のRedBlackTreeによる構成の場合,キーはRedBlackTreeを指す. DataGearはKernelのContextからプロセスのContextを経由して全て繋がっている. よって,KernelのContext上にキーを用いたDataGearの参照を書き込む. --> --- ## 権限の表現 - ファイルの権限はファイルシステムの重要な機能の一つである - 今回のRedBlackTreeによる構成の場合,木のルートの所持者を設定することがファイルに対して権限を設定することにあたる - ルートに対してアクセスする権限がなければ,読み書きができないといった実装になると考える --- ## 今後の課題 - データクエリ言語 - 時系列データ - スタンドアロンDB