# GearsOSにおけるinodeを用いたFile systemの設計
## 研究目的
### GearsOSとは
#### 信頼性と拡張性
#### ノーマルレベルメタレベルの分離
##### 信頼性
###### モデル検査
継続性
###### 定理証明
agda
### ファイルシステム未実装
だがOSにおいて重要な機能である
### GearsOSのファイルシステム設計
基幹となるディレクトリシステム
ファイル構造
API設計中
### 取り入れたい要素
backup
log
## CbC
### 簡単な説明
#### Cの下位言語
Cとの違いは
#### 関数呼び出しの代わりに継続を用いる
継続とは
#### 環境を持たない
##### 環境とは
プログラムが実行される際、その出力に影響を与える変数やデータのこと
#### 関数型言語のtail callスタイルにあたるプログラミング
tail call スタイルとは
末尾再帰とも言う
### Code Gear
関数の代わり
_codeで宣言を行う
Input/Output DG
### Data Gear
### normal level
user
### meta level
kernel
### 継続性
#### goto
jmp命令を用いる
引数付き
普通のgotoと違うところは
#### 軽量継続
##### 環境を持たない
必要なデータは毎回inputする
##### 関数呼び出し(call)せず、jmpする
処理はcallよりjmpが軽量
## GearsOSについて
### GearsOSとは
#### 信頼性の保証が目的
##### モデル検査
##### ノーマルレベルメタレベル切り分けがされている
### Context
#### 全てのCG, DGを参照できるMetaDG
normalレベルのCGから直接参照してしまうとメタレベルを切り分けた意味がなくなってしまう
Metaなのでnormalから直接参照しない
必ずMetaCGから参照される
CodeGearはDataGearの一種であるからMetaDGにMetaCGの参照を入れることが可能
CGとDGの接続に用いられる
#### 従来OSのプロセスに相当
UserプロセスにあたるUser Contextが存在する
#### 種類
##### Kernel Context
OS上の全てのContextを参照できる
##### User Context
ユーザーごとに存在する
##### CPU Context
実行しているCPUやGPUごとに存在する
#### Context参照の流れ
CGがOutputDataGearへデータをoutput
次のCGのstubCodeGearへgoto
stubCGはinputDataGear(前のCGのoutputDG)とOutputDGを参照
CGへgoto
OutputDGへOutput
次のstubCodeGearへgoto
### stub
## Christie
### Christieとは
#### 並列分散通信フレームワーク
#### CbCとは異なるGearの概念
##### DataGear
atomic
##### CodeGear
### DataGearManager
#### DGを管理している
#### key value store
CGMが利用するCGのkeyとputされたDG(value)の組み合わせをもつ
#### Fileとして用いる
#### LocalDGMとRemoteDGM
LocalはCGM自身が所持するDGのプール
RemoteはCGMが配線されている別のCGMがもつDGのプール
### topology manager
#### 任意のtopologyを生成することができる
topologyのノードはCGM
##### ノード同士の通信接続を管理
#### 分散プログラムを簡潔に書くために必要
#### 静的topology
任意のtopologyとノードの配線ができる
dotファイルに記述し，TopologyManagerに参照させる
dotファイルに記述したノードの数と参加ノードの数が一致した場合に動作する
#### 動的topology
参加を表明したノードに対し，自動的に配線を行う
## UnixのFilesystem
### xv6
MITで教育用の目的で開発されたOS
Unixの基本構造を持つ
#### filesystem
inode
#### CbCによるxv6の書き換えが行われた
### inode
#### Fileの属性情報
File Types
Permissions
UID
GID
File Size
Time Stamps
Number of link
Location on hard disk
#### inode number
inodeを識別するための番号
ファイル名とinodeがペアになっている
Mac OSではls -iで確認可能
ファイルシステム内で一意の番号
ファイル数の上限がここで決まってくる
## GearsFileSystemのディレクトリ
### Treeによるディレクトリ構造(図などでここ詳しく)
#### RedBlackTree
DataGearManagerを格納してFileSystemに
##### API
put
get
remove
#### 2つの木を用いる
##### inumとfile pointer
key: inum
value: file pointer
##### inumとfilename
key: filename
value: inum
### Unix Like
mkdir
cd
#### ls
filenameのlistを入れることでlsのリスト表示を実装できる
### 非破壊的編集によるBackUp
#### バックアップ機能をOS自体に持たせたいという目的
#### GearsOSにおける永続データ
##### 木構造を用いる
RedBlackTree
##### ルートノードから変更ノードまでのパスを全てコピー
##### コピーしたパス上に存在しないノードはコピー元の木構造と共有
## ファイル構造
### 構成
#### I/O stream
##### keyで参照
##### 競合的アクセス
###### synchronizedQueue
parusuさんの論文
##### 3つのQueue
###### input
データをinputしたい場合にこのQueueにput
###### output
####### データを取得したい場合にこのQueueからtake
Synchronized QueueかSingleLinkedQueueを選べる
###### main
データそのもの
input -> main -> output のような繋がり
###### queueの中身は共通してelement
####### elementとは
###### これらのQueueはkeyとペアになっており，keyで参照することができる．
#### logによるバージョン管理
git mercurial的
## WordCount
### APIの設計に用いる
### 機能
#### ファイルの中身を読み取り
文字数
行数
#### Unix Fileに対して行う
#### 中間報告の時の図
### GearBox的に処理する
一木さん図5
File操作の仕組み
#### GearBoxとは
GearsOSの機能を表現する手法
状態遷移図とクラスダイアグラムを組み合わせたような図
## 考察
### 現状
#### 実装できた部分
RBTreeの動作test(予定)
#### 課題
GearsOSへのtopologyManagerの実装
ディレクトリ構造の作成
### 今後の課題
分散ファイルシステム
#### 信頼性
GearsAgda
モデル検査
#### shell
#### path
### 信頼性について
#### モデル検査
RedBlackTreeのモデル検査
#### 定理証明
## 参考文献
### 一木さん
https://ie.u-ryukyu.ac.jp/~kono/papers/kono/2021/ikki-sigos-2021.pdf
一木 貴裕 ，河野 真治(琉球大学), 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), May, 2021
### アナグラさん
http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2021/anatofuz-master/raw-file/tip/paper/master_paper.pdf
parusuさん
### xv6
https://pdos.csail.mit.edu/6.828/2018/xv6/book-rev11.pdf
Papers/2020/anatofuz-sigos/
## 付録
mindmap
gearsDirectory source
## 章立て
### GearsOSにおける分散ファイルシステム(研究目的)
### CbC
### GearsOSについて
### Christie
Gear概念
DataGearManager
### UnixのFilesystem
inode
### GearsFileSystemのディレクトリ
Treeによるディレクトリ構造(図などでここ詳しく)
#### Unix Like
inodeを用いたディレクトリエントリ
非破壊的編集によるBackUp
### ファイル構造
#### 構成
logによるバージョン管理
### WordCount
### 考察
今後の課題
### 参考文献