title: GearsOSにおけるinodeを用いたFile systemの実装 author: 又吉 雄斗 profile: 並列信頼研 ## inodeを用いたgearsDirectoryの実装 - アプリケーションの信頼性を保証するために,アプリケーションが動作するOSの信頼性を高める必要がある - 信頼性確保の方法として定理証明やモデル検査がある - 当研究室では,信頼性の保証を目的としたGearsOSを開発している - GearsOSで未実装の機能であるファイルシステムの実装を目指す - 今回はUnix likeにディレクトリシステムを実装した - GearsOSへUnixのFile systemの仕組みを取り入れるアプローチをとる - GearsOSのディレクトリシステムであるgearsDirectoryについて説明する ## Continuation based C - Cの下位言語である - プログラムはCodeGearと呼ばれる処理の単位で記述する - データはDataGearと呼ばれる単位を用いる - ノーマルレベルとメタレベルの処理を切り分けることが容易に可能である - function callの継続の代わりにgotoによる継続を用いる - 呼び出し履歴を持たないことから軽量継続と呼ぶ  
## GearsOS - 当研究室にて,信頼性と拡張性の両立を目的として開発している - CbCで記述されている - Gearという概念があり,実行の単位をCodeGear,データの単位をDataGearと呼ぶ - ノーマルレベルとメタレベルの処理を切り分けることが容易にできる ## GearsOS ### CodeGearとmetaCodeGearの関係 - ノーマルレベルとメタレベルの存在 - CodeGearがDataGearを受け取り,処理後にDataGearを次のCodeGearに渡すという動作をしているように見える - 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し,それらの計算はMetaCodeGearで行われる
## GearsOS ### Context - GearsOS上全てのCodeGear,DataGearの参照を持つ - OS上の処理の実行単位 - Gearの概念ではMetaDataGearに当たる - ノーマルレベルから直接参照されず,必ずMetaDataGearとしてMetaCodeGearから参照される ## GearsOS ### CodeGear遷移の流れ
## UnixのFile system UnixのFile systemはBTreeを用いたinodeで構成されており,xv6もその仕組みを用いている ### xv6 - MITで教育用の目的で開発されたOS - Unixの基本的な構造を持つ - 当研究室ではxv6のCbCでの書き換え,分析を行なっている - File systemではinodeの仕組みが用いられている ### inode - ファイルの属性情報が書かれたデータである - 識別番号としてinode numberを持つ - inodeはファイルシステム始動時にinode領域をディスク上に確保する ## GearsFileSystemにおけるdirectoryの構成 - 2つのRedBlackTreeを用いる 1. filenameとinode numberのペアを持つindex tree 1. inode numberとinodeのポインタのペアを持つinode tree - カレントディレクトリはgearsDirectory-\>currentDirectoryに保存される
## Unix Like な interface ### mkdir ```c __code mkdir(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) { struct FTree* newDirectory = createFileSystemTree(context, gearsDirectory->currentDirectory); Node* inode = new Node(); inode->key = gearsDirectory->INodeNumber; inode->value = newDirectory; struct FTree* cDirectory = new FTree(); cDirectory = gearsDirectory->iNodeTree; goto cDirectory->put(inode, mkdir2); } __code mkdir2(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) { Node* dir = new Node(); dir->key = name->value; Integer* iNum = new Integer(); iNum->value = gearsDirectory->INodeNumber; dir->value = iNum; gearsDirectory->INodeNumber = gearsDirectory->INodeNumber + 1; struct FTree* cDirectory = new FTree(); cDirectory = gearsDirectory->currentDirectory; goto cDirectory->put(dir, next(...)); } ``` ## Unix Like な interface ### mkdir
## GearsDirectoryにおける非破壊編集ツリー - GearsOSにおける永続データは非破壊的な編集を行う木構造を用いて保存する - ディレクトリシステム自体にバックアップの機能を搭載することが可能と考える
## gearsDirectoryまとめ - gearsDirectoryの実装について説明した - RedBlackTreeを用いてinodeの仕組みを構築し,ls,cd,mkdirを作成するなどして,Unix Likeに構築することが出来た - RedBlackTreeのシンプルなinterfaceにより比較的容易に実装を行うことができた - 形式手法とファイルシステムの機能の両面で信頼性の向上が図れると考える ## GearsFileSystemの今後 ### gearsDirectory path - gearsDirectoryにはpathの機能が実装されていない - full path指定のlsなどが実装できない状態である - FileSystemTreeを拡張し,ノードをたどりpathを生成する様な機能を実装する必要がある ### gearsDirectory filename - 現状はgearsDirectoryのfilenameはIntegerの構造で管理されている - filenameは一般的に文字列型であるためIntegerから文字列型に変更する必要がある