---
marp: true
theme: cr
paginate: true
---

<!-- 全体の流れ
- 目的
- 基礎概念
- 問題提起 -> 解決 の繰り返し
- 評価 -->

# GearsOSのファイルシステムにおける GCとレプリケーション

<!--
スピーカーノート
-->

琉球大学 理工学研究科 工学専攻 知能情報プログラム
河野研究室

又吉 雄斗

---

<!-- 目的 -->

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

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

---

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

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

---

## 信頼性を上げる方法

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

---

<!-- ここからGears OSの基礎概念だと明示する -->

## Continuation based C

- Cの下位言語である
- 処理の単位 CodeGear
- データの単位 DataGear
- ノーマルレベルとメタレベルの切り分け
- gotoによる軽量継続

---

## CodeGearとmetaCodeGearの関係

- ノーマルレベルとメタレベルの存在

![w:1100](figs/meta_cg_dg.svg)

---

## Context

- Gears OS上全てのCodeGear，DataGearの参照を持つ
- OS上の処理の実行単位
  - プロセスに相当
- Gearの概念ではmetaDataGearに当たる
- ノーマルレベルから直接参照されない
  - metaCodeGearから参照される

---

## 3種類のGears OS

- GearsAgda(Agda)
  - 形式手法による信頼性の向上
- CbC x.v6
  - スタンドアロンOS
- Gears OS(CbC) ← 今回の実装対象
  - ユーザーレベルタスクマネージメント

---

## GearsAgdaとGearsOSの対応

- GearsOSのCodeGearと直接対応している
- GearsAgdaでRedBlackTreeの証明が進められている
  - find完了、insert証明中
- GearsOSの構造はRedBlackTreeが多くを占める

GearsAgdaでRedBlackTreeが証明できれば、GearsOSのファイルシステムの大部分を証明したことになる

---

## CodeGear遷移の流れ

![w:1100](figs/context.svg)

---

## 非破壊RedBlackTree

![w:1100](figs/nondestructive_tree_modification.png)

---

<!-- ここまでがGears OSの基礎概念だと明示する -->

## GearsFilesystem

- GearsOSで書かれたファイルシステム
  - i-nodeによるディレクトリシステム
  - 分散ファイルシステムの通信機能
- 非破壊RedBlackTreeで構成される
- ディスク上とメモリ上のデータ構造を統一する

---

## ファイルシステムの信頼性

- 電源断時にデータが残るpersistency
- データを書き込めたかどうかを判定するatomic write
- ノード喪失時にデータを保護する多重性
- 複数のコピーを調停するコミット機構

---

## メモリ管理や多重性の機能がない

<!-- それぞれが何のためにあるのか説明する感じでやると良い -->

メモリ管理

- アロケーション
- GC(ガベージコレクション)

多重性

- レプリケーション
- バックアップ


---

## メモリ管理や多重性の機能の要件

<!-- 照明のしやすさの維持が唐突な感じ
動作の正しさがわかりやすい実装で証明しやすく -->

- 信頼性を上げたい
  - 証明のしやすい実装
- データの持続性
  - 持続性のあるストレージにちゃんとコピーする
  - 適切なタイミングでコピーを行う
- 非破壊RedBlackTreeのメモリ管理
  - 非破壊RedBlackTreeは履歴を全て持つ
  - 過去の履歴分のメモリを解放する必要がある

---

## GearsOSにおけるGC
<!--  -->
CopyingGCを採用する
- 新しいContextのメモリに新規にコピーする
- 古いContextをそのまま全部解放する

---

## GearsOSにおけるレプリケーション

<!--  -->

単純に木をコピーする
複数のストレージに同時に木を置く
そのうちの一部は持続的なストレージにする
システム起動時には必要な分をメモリにコピーする

トランザクションも考慮する

---

## RedBlackTreeのトランザクション

- 木のルートのすげ替えがトランザクションになる
- read
- write

---

## copyRedBlackTreeの実装をした

- RedBlackTreeのコピーを行う
- GCやレプリケーションの機能のために木のコピーが必要

---

## copyRedBlackTreeによって出来ること

多重性やメモリ管理に関する機能を追加できる
GC(defragmentation)
レプリケーション
バックアップ

---

## Tree InterfaceのAPIとして実装

---

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

![w:1100](figs/)

---

## アロケーション部分

![w:1100](figs/)

---

## swap

![w:1100](figs/)

---

## 実行方法

---

## 評価

非破壊RedBlackTreeの増大抑制できる
コピーするだけなので木が持続的
課題点
  同一Contextへコピーしている
コピーの正しさ
Stack使っているので余計なメモリを消費する
Stackも非破壊であるという問題がある
-> 証明しやすさを優先しているから
Stackが非破壊である意味があまりない？のでここを破壊でやる。

---

## 今後の研究方針

別Contextコピー
GearsAgdaでの記述
Stack領域の圧縮
- Stackの再利用？
GC，レプリケーションの実装
多重性以外の機能

---

## まとめ

- copyRedBlackTreeを実装した
- それにより多重性を確保できるようになった
- 多重性はシステムの信頼性を向上させる
- 非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった