# 研究目的

## システム全体の信頼性を上げたい

- システムの構成要素全体の信頼性を上げる必要がある
  - アプリケーション
  - OS
  - ファイルシステム
  - DB
  - メモリとSSD
  - 分散ノード
  - ネットワーク

## ファイルシステムとDBの信頼性を考える

- ファイルシステムとは何か

- DBとは何か

- これらは何が違うのか

- 検証・モデル検査をできる形に記述したい

## ファイルシステム

- 可変長の文字列を格納するファイル

- そのファイルにアクセスするための名前管理

- 同時アクセスした時に名前管理の一貫性を保証する

- ファイルに同時に書き込まれた時の一貫性の保証はしない
  - ファイルの書き込みを制御するロック機構がある

## DB

- 入力の属性名と型の組みを複数持つレコード

- 特定の属性をキーとしたテーブル

- レコードのinsert, delete, updateの直列化可能性を保証する機能がある

## ファイルシステムとDBの違い

- 格納するものの形式

- それにアクセスする方法

- 直列化可能性を保証する手法

- これらが違うだけで本質的な違いはない

## ファイルシステムとDBのもつ追加機能

- 電源切った時にデータが残る(持続性persistency)

- 書き込めたかどうかをtrue, falseで判定するatomic write

- ひとつのノードが失われた時にデータを保護する多重性

- 適当なチェックポイントからDB、ファイルシステムを回復する機能

- 複数のコピーを調停するコミット機構

## Gears OSを使って実現する


- CodeGear
  - 処理の単位
- DataGear
  - データの単位
- metaGear
  - データの整合性
  - 資源管理

非破壊的なRedBlackTreeでほとんどのものが記述できるのではないか

## 信頼性を上げる方法

- 証明
  - GearsAgdaを使ってinvariantを証明する
- テスト
- モデル検査
- システムの構成要素全体にこれらの方法を適用したい
- 既存システムの信頼性における問題点の解決

## GearsOS上のファイルシステムやDB

- RedBlackTreeでどちらも一応実現できてはいるが、できていないことも多い

- 複数のreplicationを持てていない

- GCがない

RedBlackTreeのコピーをやると良いのではないか

## RedBlackTreeのコピー

- 単なるコピーだが実際は複雑

- Treeをコピーしている間に変更されたら？

- 頭から最後までコピーすることはできない

- コピー前と後で同一であることを確認する必要がある

## コピーのアルゴリズム

- insertはRedBlackTreeを辿って必要なノードまでTreeをコピーしながら下っていく

- 見つかったら変更したTreeを返す

- そのためにはStackを使ってTreeを辿っていく

- まず左側を深さ優先で辿る

- アロケートしたノードは別のContext上に作る必要がある
  - なぜならばGCしたいから
  - 全部のTreeをコピーしたら古いContextを消すことでGCになる
  - これはメモリ管理をモナドで表していることになる

- リーフまできたらStackを巻き戻すCGを呼ぶ
  - この時左側はできているので右側を呼び出す

- Stackのノードの情報だけでできるのか

- Stackが二つ必要かもしれない
  - 全体と途中まで作りかけのTreeのStack

## 進捗など