Mercurial > hg > Papers > 2024 > matac-master
view marp-slide/slide.md @ 76:13969295f118
...
| author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 14 Feb 2024 11:38:01 +0900 |
| parents | c6d41c973c8a |
| children | 5847cf59e9b3 |
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で構成される - indexやi-nodeの木 - DataGearを保持するQueueのリスト - ディスク上とメモリ上のデータ構造を統一する --- ## ファイルシステムの信頼性 - 電源断時にデータが残るpersistency - データを書き込めたかどうかを判定するatomic write - ノード喪失時にデータを保護する多重性 - 複数のコピーを調停するコミット機構 --- ## メモリ管理や多重性の機能がない <!-- それぞれが何のためにあるのか説明する感じでやると良い --> メモリ管理 - メモリ割り当てと保護、メモリリーク防止に必要 - 例：アロケーション、GC(ガベージコレクション) 多重性 - 単一障害点の排除、可用性の保証、災害復旧に必要 - 例：レプリケーション、バックアップ --- ## メモリ管理や多重性の機能の要件 <!-- 照明のしやすさの維持が唐突な感じ 動作の正しさがわかりやすい実装で証明しやすく --> - 信頼性を上げたい - 証明のしやすい実装 - データの持続性 - 持続性のあるストレージにちゃんとコピーする - 適切なタイミングでコピーを行う - 非破壊RedBlackTreeのメモリ管理 - 非破壊RedBlackTreeは履歴を全て持つ - 過去の履歴分のメモリを解放する必要がある --- ## GearsOSのGC CopyingGCのような仕組み - 新しいContextのメモリに新規にコピーする - 古いContextをそのまま全部解放する  --- ## GearsOSの レプリケーション - 複数のストレージに同時に木をコピーする - そのうちの一部は持続的なストレージにする - システム起動時には必要な分をメモリにコピーする トランザクションも考慮する  --- ## RedBlackTreeの トランザクション - トランザクションはのルートの置き換え - 複数の書き込みポイント - 最新の情報が欲しい場合は書き込み停止処理が必要  --- ## copyRedBlackTreeの実装をした - GCやレプリケーションの機能のために木のコピーが必要 - RedBlackTreeのコピーが出来るAPIを実装した --- ## Tree InterfaceのAPIとして実装 ```c typedef struct Tree<> { union Data* tree; struct Node* node; __code put(Impl* tree, Type* node, __code next(...)); __code get(Impl* tree, Type* node, __code next(...)); __code remove(Impl* tree, Type* node, __code next(...)); __code copy(Impl* tree, __code next(...)); __code next(...); } Tree; ``` - `goto tree->copy(next);`という形で使用できる --- ## コピーの アルゴリズム - left方向へ深さ優先探索を行う - 2つのStackを使用する - nodeStackは元の木を辿る - toStackは新しい木を操作 - 大まかにleftDown, rightDown, upの3ステップ  --- ## アロケーション部分 - leftDown、rightDownで新しい木のノードをアロケートする - newキーワードでアロケートしている ```c struct Node* newNode = new Node(); struct Node* data = (Node*)(stack->data); newNode->key = tree->current->left->key; newNode->value = (union Data*)new Integer(); ((Integer*)newNode->value)->value = ((Integer*)tree->current->left->value)->value; newNode->color = tree->current->left->color; if(data) { data->left = newNode; } ``` --- ## ALLOCATEマクロ - newキーワードによってビルド時に挿入されるマクロ - Contextが持つヒープ領域にDataGearサイズの領域を確保する - リニアアロケートする ```c #define ALLOCATE(context, t) ({ \ context->heap = __builtin_align_up(context->heap + sizeof(Meta) , sizeof(void *)) - sizeof(Meta); \ Meta* meta = (Meta*)context->heap;\ context->heap += sizeof(Meta);\ union Data* data = context->heap; \ context->heap += sizeof(t); \ meta->type = D_##t; \ meta->size = sizeof(t); \ meta->len = 1;\ meta->data = data; \ *context->metaData = meta; \ context->metaData++; \ data; }) ``` --- ## swap - コピー完了後に木を切り替える - CopyingGCのFrom To切り替えを想定 - 同一Context上での動作になっている  --- ## 実行方法 --- ## 評価 - 非破壊RedBlackTreeの増大抑制できる - コピーで木の持続性を確保できる 課題点 - 同一Contextへコピーしている - Stack使っているので余計なメモリを消費する - Stackも非破壊であるという問題がある - 証明しやすさを優先しているから - 非破壊である意味があまりない - コピーの正しさ --- ## 今後の研究方針 - 別Contextコピー - GearsAgdaでの記述 - Stack領域の圧縮 - Stackの再利用？ - GC，レプリケーションの実装 - 多重性以外の機能 --- ## まとめ - copyRedBlackTreeを実装した - それにより多重性を確保できるようになった - 多重性はシステムの信頼性を向上させる - 非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった