Mercurial > hg > Papers > 2024 > matac-master
view marp-slide/slide.md @ 80:e81688943a04
...
| author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 15 Feb 2024 12:28:59 +0900 |
| parents | 810987627f3c |
| children | 4052b8572f02 |
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から参照される --- ## CodeGear遷移の流れ  --- ## GearsOSのプログラミングと通常のプログラミングの違い - 実行するプログラムをCodeGearという単位に分割する - CodeGearの引数とContextにプログラムの状態が全部入っている - 通常のプログラムでは関数呼び出しのStackやループの状況が隠されている - CodeGear単位の切り替え点でモデル検査や証明が行える - 状態の明示化は証明を行う際には必ず行う必要がある --- ## 基本的なデータ構造の処理をGearsOSに書き換える必要性 - 既存のプログラムをそのままCodeGearに書き換えることは可能 - しかし、CodeGear、DataGearともに複雑になる - なぜかというと、既存のプログラムは人間向けの読みやすさが優先だから - 重要なのは信頼性なので、モデル検査のしやすさ兼証明のしやすさを優先する - 基本的なデータ構造を証明優先に書き換える必要がある - これらは既存のプログラムと異なるプログラミングスタイルになる --- ## 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のファイルシステムの大部分を証明したことになる --- ## 非破壊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も非破壊であるという問題がある - 証明しやすさを優先しているから - 非破壊である意味があまりない - コピーの正しさ --- ## GearsOSでの記述に変換する際の問題点 - ループ文がない - gotoのループで表現する必要がある - 処理が細切れになって全体の把握が難しい - stackをpop、pushするたびにgotoするなどが原因 - ここのフローに入ると何回popされるかなどがわかり辛い - 事前にどのようなCodeGearが必要かわかりにくい - デバッグが難しい - Call Stackがないため処理の流れが掴めない - printでどのCodeGearを通ってきたかを把握する --- ## 今後の研究方針 - Stack領域の圧縮と再利用 - 別Contextコピー - これによりGCとレプリケーションが可能になる - モデル検査で並行実行下で正しく動くことを調べる - メモリアロケーションを含めたモデル検査を行う - GearsAgdaで記述して証明する - 並列実行下で正しく動くか - メモリが正しく開放されているかどうか --- ## まとめ - copyRedBlackTreeをGearsOSで実装した - それにより多重性を確保できるようになった - 多重性はシステムの信頼性を向上させる - 非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった