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

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

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

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

又吉 雄斗, 佐野 巧曜, 河野 真治

---

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

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

---

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

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

---

## 信頼性を上げる方法

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

---

<!-- 全体的な問題提起 -->

## OSとFSとDBがバラバラ

- 全体を組み合わせた時の正しさが怪しい
- DBは実はファイルの上に作られていたり
  - ファイルに対する書き込みのatomicityが保証されてない
- それぞれ別々なトランザクションがある

---

<!-- 全体的(検証における)解決方法 -->

## FSとDBの要素をRBTreeに対応させる

<!-- システムの構成要素全体にこれらの方法を適用するために -->

- ファイルシステムとDBをRedBlackTreeで統一
  - 信頼性向上のために必要なDBの仕組み
  - データ持続性に必要なファイルシステムの仕組み
- RedBlackTreeはinvariantで証明する
- システム統一によりシステム全体の検証が簡単に
- トランザクションの統一化

<!-- FS, DBの統一的な実装により，複雑性が取り払われ正しさの検証が楽になる -->

---

## 実装がブロックベース

- B-Treeによる実装はディスクのブロックアクセスが前提
- SSDのようなランダムアクセスが前提となっていない
- ランダムアクセスの場合B-Treeを用いる利点は少ない
- 証明しやすいRedBlackTreeを用いることが考えられる

---

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

---

## CodeGear遷移の流れ

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

---

## ファイルシステムとDB

<!-- ここから本編 -->

- 両方ともRedBlackTreeで実装する
  - 本質的な役割は一緒
  - 信頼性の向上
  - 証明のしやすさ
- 非破壊Tree
  - データの持続性

---

<!-- 問題提起 -->

## データの持続性

- メモリとディスクみたいな分け方が時代遅れに
  - ほとんどのデータはメモリ上にある
  - 分散ノード上に多重のコピーが存在する
  - 分散台帳などの多様なconsistensyがある
- 多様なストレージ階層に対応できていない
  - 大量のメモリ
  - NVMe
  - SSD
  - RAID
  - テープ

---

## 非破壊的なRedBlackTree

<!-- これで統一することでトランザクションの統一が可能という話を入れたい -->

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

---

## RedBlackTreeはDBのテーブル

- テーブルのキーがRedBlackTreeのkey
- トランザクションはテーブルのルートの置き換え
- 複数の書き込みポイント

![bg right:45% 65%](figs/transaction.svg)

---

## データの持続性

<!-- ディスク上とメモリ上のデータ構造が一緒という話を入れる -->
<!-- 解決方法 -->

- オンメモリーなRedBlackTree
- SSD上のコピー
  - ログ的にコピーしていく
  - Copying GC

---

<!-- 問題提起 -->

スキーマ
    テーブルに入るレコードの決まった形
    実は頻繁に変更される
    なので動的な属性名を設定されたりする
    DB理論が役に立たない
    過去のDBとの互換性がない
    扱うデータはjsonなどで，もはや第一正規形でない
    ファイルシステムには型が存在しない
    ファイルシステムが提供してるトランザクションが明快でない
第一正規形
    表がネストしてないこと
    実際にプログラムに出てくるのはstack, list, queue
        これらは第一正規形ではない
        なのでFSになってる
<!-- 第一正規形を満たさないデータを扱う場合はFSが必要 -->

---

<!-- 解決方法 -->

## スキーマ

- DBの各テーブルのレコードの型定義
- Contextに登録されているDataGearの型
- キーを用いたDataGearの参照

---

<!-- 解決方法 -->

## インピーダンスミスマッチ

- プログラムで使用するデータ構造
  - queue
  - stack
- DBにはリストやキューは入らない
  - 第一正規系でないから
- データ構造を持続的にしたい
  - なのでファイルシステムが必要

---

<!-- 解決方法 -->

## RedBlackTreeベースのファイルシステム

- i-node番号をkeyにする
- inodeにはDGのリストが入る
- 持続性
  - オンメモリーなRedBlackTree
  - SSD上のコピー
    - ログ的にコピーしていく

---

## バックアップとロールバック

- ロールバックの必要性
  - トランザクションの失敗
  - システムクラッシュ
- SSDのログからロールバックする
  - Copying GCによるバックアップ
  - ルートノードがデータのバージョン

---

## 構成要素

- すべてRedBlackTreeで構成されている
  - 検証はRedBlackTreeだけで良い
  - invariantで証明する
- RedBlackTreeによる権限の表現
  - metaDGで行う
  - ContextからアクセスできるRedBlackTreeがある

---

## 信頼性の保証

- RedBlackTreeの変更の正しさ
- トランザクションの正しさ
- アクセス権限の正しさ
- SSDへのコピーの正しさ
- ポータビリティ
  - 異なる計算機アーキテクチャ
  - 異なるエンコード
  - 異なる分散ノード
- 正しくスキーマに対応しているかどうか
  - 違反しても良い

---

## 今後の課題

- データクエリ言語
  - SQL
  - SQLより良いものが欲しい
    - ファイルシステムとDBの両方で使える
- 時系列データ
  - データ圧縮
- スタンドアロンなDB
  - ポータビリティ

<!-- 今後やりたいことで締めるとなんか締まりがない... -->