title: GearsOSにおける<br />inodeを用いたファイルシステムの構築
author: Matayoshi Yuto, Sano Yoshiaki, Shinji Kono,
profile: 琉球大学 


<!-- ここでは大きな目的を述べる -->

## 研究目的

- アプリケーションの信頼性を保証するために，アプリケーションが動作するOSの信頼性を高める必要がある
- 信頼性確保の方法として定理証明やモデル検査がある
- 当研究室では，信頼性の保証を目的としたGearsOSを開発している
- GearsOSで未実装の機能であるファイルシステムの実装を目指す

<!-- ここでは今回やったことの概要を述べる -->

## inodeを用いたgearsDirectoryの実装

- <span style="color: red; ">今回はUnixのinode仕組みを参考にディレクトリシステムを実装した</span>
- GearsOSのディレクトリシステムであるgearsDirectoryについて
  - 基礎概念
    - CbC
    - GearsOS
  - 実装


<!-- ここから基礎概念 -->

## 信頼性の保証を目的としたOS

- GearsAgda(Agda)
  - 形式手法による信頼性の向上
- GearsOS(CbC) <- 今回ディレクトリシステムの実装を行なった
  - ユーザーレベルタスクマネージメント
- x.v6(CbC)
  - スタンドアロンOS

## Continuation based C

- Cの下位言語である
- プログラムはCodeGearと呼ばれる処理の単位で記述する
- データはDataGearと呼ばれる単位を用いる
- ノーマルレベルとメタレベルの処理を切り分けることが容易に可能である
- function callの継続の代わりにgotoによる継続を用いる
  - 呼び出し履歴を持たないことから軽量継続と呼ぶ

&emsp;

<div style="text-align: center;">
  <img src="figs/cgdg.svg" width="1000">
</div>

## GearsOS(CbC)

- 当研究室にて，信頼性と拡張性の両立を目的として開発している
- CbCで記述されている
- Gearという概念があり，実行の単位をCodeGear，データの単位をDataGearと呼ぶ
- ノーマルレベルとメタレベルの処理を切り分けることが容易にできる

## GearsOS(CbC)

### CodeGearとmetaCodeGearの関係

- ノーマルレベルとメタレベルの存在
  - CodeGearがDataGearを受け取り，処理後にDataGearを次のCodeGearに渡すという動作をしているように見える
  - 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し，それらの計算はMetaCodeGearで行われる

<div style="text-align: center;">
  <img src="../paper/figs/meta_cg_dg.svg" width="1200">
</div>

## GearsOS(CbC)

### Context

- GearsOS上全てのCodeGear，DataGearの参照を持つ
- OS上の処理の実行単位
- Gearの概念ではMetaDataGearに当たる
- ノーマルレベルから直接参照されず，必ずMetaDataGearとしてMetaCodeGearから参照される

<!--
### Contextの種類

- OS全体のContextを管理するKernel Context
- ユーザープログラムごとに存在するUser Context
- CPUやGPUごとに存在するCPU Context

-->

## GearsOS(CbC)

### CodeGear遷移の流れ

<div style="text-align: center;">
  <img src="figs/context.svg" width="1200">
</div>

## Unixのinode

- UnixのファイルシステムはメタデータにBTreeで構成されたinodeを用いる

### inode

- ファイルの属性情報が書かれたデータである
- 識別番号としてinode numberを持つ
- inodeはファイルシステム始動時にinode領域をディスク上に確保する

<!-- ここまで基礎概念 -->

<!-- 実装したものの説明 -->

## GearsFileSystemにおけるdirectoryの構成

- 2つのRedBlackTreeを用いる
1. filenameとinode numberのペアを持つindex tree
1. inode numberとinodeのポインタのペアを持つinode tree
- カレントディレクトリはgearsDirectory-\>currentDirectoryに保存される

<div style="text-align: center;">
  <img src="figs/inode.svg" width="1000">
</div>

## 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

<div style="text-align: center;">
  <img src="figs/mkdir.svg" width="1100">
</div>

<!--
## Unix Like な interface

### ls

```c
__code ls(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) {
    Node* dir = new Node();
    dir->key = name->value;
    struct FTree* cDirectory = new FTree();
    cDirectory = gearsDirectory->currentDirectory;
    goto cDirectory->get(dir, ls2);
}

__code ls2(struct GearsDirectoryImpl* gearsDirectory, struct Node* node, __code next(...)) {
    printf("%d\n", node->key);
    goto next(...);
}
```

## Unix Like な interface

### ls

<div style="text-align: center;">
  <img src="figs/ls.svg" width="1000">
</div>

## Unix Like な interface

### cd

```c
__code cd2Child(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) {
    struct FTree* cDirectory = new FTree();
    cDirectory = gearsDirectory->currentDirectory;
    struct Node* node = new Node();
    node->key = name->value;
    goto cDirectory->get(node, cd2Child2);
}

__code cd2Child2(struct GearsDirectoryImpl* gearsDirectory, struct Node* node, __code next(...)) {
    struct FTree* iNodeTree = new FTree();
    iNodeTree = gearsDirectory->iNodeTree;
    goto iNodeTree->get(node->value, cd2Child3);
}

__code cd2Child3(struct GearsDirectoryImpl* gearsDirectory, struct Node* node, __code next(...)) {
    gearsDirectory->currentDirectory = node->value;
    goto next(...);
}
```

## Unix Like な interface

### cd

<div style="text-align: center;">
  <img src="figs/cd.svg" width="1200">
</div>

-->

<!-- 課題 -->

## GearsDirectoryにおける非破壊編集ツリー

- GearsOSにおける永続データは非破壊的な編集を行う木構造を用いて保存する
- ディレクトリシステム自体にバックアップの機能を搭載することが可能と考える

<div style="text-align: center;">
  <img src="../paper/figs/nondestructive_tree_modification.png" width="1200">
</div>

## GearsOSにおけるメモリマネージメントシステム

- メモリとディスク上のデータ構造が等しくなる形で実装したい
  - 単純なコピーでメモリとディスク間のデータやり取りを行うことができる
  - メモリとディスクのデータアクセスの形式を統一することができる

<div style="text-align: center;">
  <img src="figs/disk-memory.svg" width="900">
</div>

## GearsOSにおけるメモリマネージメントシステム

- メモリとディスク上のデータ構造が等しくなる形で実装したい
  - 単純なコピーでメモリとディスク間のデータやり取りを行うことができる
  - メモリとディスクのアドレスの差はoffsetを変換することによって吸収する
  - メモリとディスクのデータアクセスの形式を統一することができる

<div style="text-align: center;">
  <img src="figs/data-access.svg" width="900">
</div>

## GearsOSにおけるメモリマネージメントシステム

- ガベージコレクションはCopying GCを用いる

<div style="text-align: center;">
  <img src="figs/copying-gc.svg" width="900">
</div>

## GearsFileSystemの今後

### gearsDirectory path

- gearsDirectoryにはpathの機能が実装されていない
- full path指定のlsなどが実装できない状態である
- FileSystemTreeを拡張し，ノードをたどりpathを生成する様な機能を実装する必要がある

### gearsDirectory filename

- 現状はgearsDirectoryのfilenameはIntegerの構造で管理されている
- filenameは一般的に文字列型であるためIntegerから文字列型に変更する必要がある

<!--
## GearsFileSystemの今後

### gearsDirectory on disk

- 現状はgearsDirectoryはon memoryで実装されている
- inodeをdisk上に構築する必要がある

### GearsShell

- 現状のGearsOSはユーザーの入力を受け付けることが出来ず，言語フレームワークの様に機能している
- gearsFileSystemなどGearsOSの各機能と接続し，今回作成したcdやlsの様なコマンドを受け付けるGearsShellを作成したい

### ファイルのバックアップ

- レコードのDataをファイルの差分履歴として保持し，日時情報を付け加えることでVersion Control Systemのような機能を持たせることが可能であると考えられる
-->

## gearsDirectoryまとめ

- gearsDirectoryの実装について説明した
  - RedBlackTreeを用いてinodeの仕組みを構築し，ls，cd，mkdirを作成するなどして，Unix Likeに構築することが出来た
  - RedBlackTreeのシンプルなinterfaceにより比較的容易に実装を行うことができた
  - 形式手法とファイルシステムの機能の両面で信頼性の向上が図れると考える
- メモリマネージメントシステムについて考察した

<!-- 

メモ書き

- [x] GearsAgdaの話入れて，どこに対する実装なのかはっきりさせる
- [x]「CbCでinodeファイルシステムを実装した」ことをはっきりさせる
- [ ] 実装部分と未実装部分をはっきりさせる
- [x] x.v6の話いらない？ -> 研究会で知らない人多分いないからいらない
- [ ] 仮想記憶との関係　これは図にできそう
- [x] まず大きな目的を述べる．その後，今回やったことを述べる


この流れがいいだろう

大きな研究目的　-> 今回の研究 -> 今回の研究に関する基礎概念
-> 実装したもの -> 実装したものの至らない点 -> 今後実装するものの紹介と考察
  
-->