# xv6の構成要素の継続の分析

- 清水 隆博
    - 琉球大学大学院理工学研究科情報工学専攻
- 河野 真治
    - 琉球大学工学部


---

# 研究目的

- アプリケーションの信頼性を向上させるたい
  - その為には土台となる OS 自体の信頼性を高く保証したい
- OSそのものも巨大なプログラムである
    - テストコードを用いた方法で信頼性を確保する事が可能
- しかし並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大
    - テストで完全にバグを発見するのは困難
    - テスト以外の方法でOSの信頼性を高めたい

---
# OSの信頼性
- OSそのもの動作も保証されるべき
- アプリケーションが行いたい処理の他に、 メモリやCPUの資源管理などが存在する
    - アプリケーション側からするとOSの機能
- 本来行いたい処理
    - ノーマルレベルと呼ぶ
- 資源管理など
    - メタレベルと呼ぶ
    - この別け方はOSの実装でも存在する
- ノーマル、メタレベルの計算の両方を保証しないといけない

---

# テスト以外で信頼性を高める方法
- モデル検査
    - 実際に想定されるパターンを全て動かして検証する
    - デッドロック発生の検知
      - JavaPathFinderなど
- 定理証明支援系
    - 論理学的なモデルに変更して証明する
      - Agda
      - Coq
- OSをこれらの方法で信頼性を高めたい



---

# OSの信頼性を高めるためには
- 既存のOSのソースコードをそのまま使うのは困難
- モデル検査の場合
    - OS自体をモデル検査する機能をOSに組み込む必要がある
- 定理証明系の場合
    - Agda/CoqでOSを再実装する必要がある
    - それらのコードはそのままコンパイルする事ができない
- ノーマルレベル/メタレベルを切り分けるのも困難
- 動きつつ証明可能なOSを目指したい
    - これらを同時に達成出来るプログラミング言語でOSを実装する必要がある

---
# Continuation Based C
- ノーマルレベル/メタレベルの実装に適している言語
- C言語の下位言語であり、 いくつかのCコンパイラ上で実装している
    - gcc
    - llvm/clang