# HG changeset patch # User anatofuz # Date 1590485770 -32400 # Node ID f68cad98da695a79e0ccd64d268b7e04f0b0f481 # Parent 778f4b2b68f0a125ec436f7530bdc955b7121300 add slide diff -r 778f4b2b68f0 -r f68cad98da69 slide/slide.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/slide.html Tue May 26 18:36:10 2020 +0900 @@ -0,0 +1,139 @@ +
+

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
      • +
    +
    • +
+
+
\ No newline at end of file diff -r 778f4b2b68f0 -r f68cad98da69 slide/slide.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/slide.md Tue May 26 18:36:10 2020 +0900 @@ -0,0 +1,66 @@ +# 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