# 令和5年度研究計画書

## 研究題目

Gears OSのファイルシステムとDB

## 研究目的

当研究室では，Continuation based C（CbC）を用い，定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している．OSにおいてFSは重要な機能の一つであるため実装する必要がある．その際，証明や検証を容易に行えるようになるべくシンプルな実装を考えたい．

## 研究内容

証明や検証を容易に行うため，FSとDBの実装をすべてRedBlackTreeで行う．FSとDBは本質的に同じものであるが，スキーマの有無などの違いがあるため，違いの部分を考察しつつ同一のRedBlackTreeで実装する．(FSとして実装したものがそのままDBとなりうると考える．) また，信頼性の向上のためトランザクションとロールバック，バックアップなどをRedBlackTreeに適した形で実装し，それぞれ検証する．全体としては，証明や検証への適正，システムとしての信頼性の確認，RedBlackTreeのみでの実装に関する考察を行う．

## 研究計画

~ 5月15日 OS研究会準備(実装・スライド・発表練習)

5月16日 ~ 5月17日 OS研究会発表

5月17日 ~ 11月 実装と検証
- 特にトランザクション部分やロールバック，バックアップ部分などシステムの信頼性に関わる部分の検証を行う

2024年

1月 修論提出

2月 修論発表

# 中間報告書

## 大学院在学中に実施した研究の内容

2023年5月のOS研究会に投稿した論文を研究内容とする

- 中間報告書の研究内容としての使用許可を和田先生と河野先生から得た
- http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2023/matac-sigos/raw-file/tip/Paper/paper.pdf
    - 読み込みに時間がかかるかもしれません
	
## 大学院入学以降の研究活動への取り組みに関する振り返り

- 実装にまだ全然手をつけていない
- 実装の方針は固まりつつあるが，詳細設計を行えていない
    - 今後は実装を積極的に進めていきたい
- 河野研の論文や研究に関しては調査を行い知見を深めることができた
    - 外部の研究についての調査が少ないので，DBの信頼性の関連研究を調査したい

### 2022年
#### 4月

- Gears OS(CbC)にてRedBlackTreeによるディレクトリシステムを構築
- 研究会論文執筆

#### 5月

- OS研究会発表
    - GearsOSにおけるinodeを用いたファイルシステムの構築
    - http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2022/matac-sigos/raw-file/tip/Paper/paper.pdf

#### 6月~12月

- 既存のファイルシステム，DBの調査
- データストアシステムの信頼性に関する考察
- Rust製RDBMSのコードリーディング

### 2023年

#### 1月~4月

- DBの信頼性に関する調査
- ファイルシステムとDBをRedBlackTreeで表現する考察
- CbC x.v6の調査
- 研究会論文執筆

#### 5月

- OS研究会発表
    - Gears OSのファイルシステムとDB
    - http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2023/matac-sigos/raw-file/tip/Paper/paper.pdf
	
## 修士論文完成までの計画

### 2023年

#### 5月~12月 実装と検証

- RedBlackTreeによるデータストアシステムの詳細設計
- CbC x.v6に対し，RedBlackTreeのデータストアを構築
    - 構築が間に合えばどこかに論文を投稿したい
- 特にトランザクション部分やロールバック，バックアップ部分などシステムの信頼性に関わる部分の検証
- 修士論文執筆

### 2024年

#### 1月

- 修論提出

#### 2月

- 修論発表