# HG changeset patch # User anatofuz # Date 1590584680 -32400 # Node ID 92e7655a74584168f0c297b3e44f873de0572be2 # Parent 76a8f55f23fad184de9b606a99409ffeba671b92 ... diff -r 76a8f55f23fa -r 92e7655a7458 slide/slide.html --- a/slide/slide.html Wed May 27 22:03:59 2020 +0900 +++ b/slide/slide.html Wed May 27 22:04:40 2020 +0900 @@ -12,7 +12,7 @@ /* @theme example */div#p>svg>foreignObject>section{background-image:url("assets/logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto} -/* @theme c2kfvr8jgqfsn3ewehvvwh4jg228qrr336cc0x1hrsq7 */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}
+/* @theme xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}

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

  • 清水 隆博 @@ -27,54 +27,46 @@
-
+

研究目的

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

OSの信頼性

-
    -
  • OSそのもの動作も保証されるべき
    • -
  • アプリケーションが行いたい処理の他に、 メモリやCPUの資源管理などが存在する +
    +

    ノーマルレベルとメタレベルを用いた信頼性の向上

      -
    • アプリケーション側からするとOSの機能
      • -
    - -
  • 本来行いたい処理 +
  • プログラムの実行部分は以下の2つからなる
      -
    • ノーマルレベルと呼ぶ
      • +
    • 入力と出力の関係を決める計算(ノーマルレベル)
      • +
    • プログラムを実行したり、 信頼性を保証するために必要な計算(メタレベル)
    • -
  • 資源管理など +
  • メタレベルの例
      -
    • メタレベルと呼ぶ
      • -
    • この別け方はOSの実装でも存在する
      • +
    • メモリやCPUの資源管理
      • +
    • システムコールの動作(副作用)
      • +
    • 並行実行(他のプロセスとの干渉)
      • +
    • モデル検査(可能な実行を列挙する方式の実行)
      • +
    • 証明(入力時と出力時の論理的な条件)、(invariant)
    • -
  • ノーマル、メタレベルの計算の両方を保証しないといけない
    • +
  • メタレベルの計算として信頼性を保証する
    • -
    -

    テスト以外で信頼性を高める方法

    -
      -
    • モデル検査 +
      +

      モデル検査

      • 実際に想定されるパターンを全て動かして検証する
      • デッドロック発生の検知 @@ -82,9 +74,12 @@
      • JavaPathFinderなど
      +
    • 状態爆発が問題になる
      • +
    • Spinを用いる方法では、 promelaという言語で実装し直す必要がある
      • - -
    • 定理証明支援系 +
      • +
      +

      定理証明支援系

      • 論理学的なモデルに変更して証明する
          @@ -92,48 +87,29 @@
        • Coq
        • +
      • HoareLogicを用いる +
          +
        • PreCondition -> Statement -> PostCondition
        • -
      • OSをこれらの方法で信頼性を高めたい
        • -
      -
      -
      -

      OSの信頼性を高めるためには

      -
        -
      • 既存のOSのソースコードをそのまま使うのは困難
        • -
      • モデル検査の場合 +
      • 従来の方法ではStatementには限られたコマンドしか使えない
          -
        • OS自体をモデル検査する機能をOSに組み込む必要がある
          • -
        -
        • -
      • 定理証明系の場合 -
          -
        • Agda/CoqでOSを再実装する必要がある
          • -
        • それらのコードはそのままコンパイルする事ができない
          • -
        -
        • -
      • ノーマルレベル/メタレベルを切り分けるのも困難
        • -
      • 動きつつ証明可能なOSを目指したい -
          -
        • これらを同時に達成出来るプログラミング言語でOSを実装する必要がある
          • +
        • ループは不変条件を使うが、 条件を見つけることが一般的には困難
          • +
        • 実装言語と同じ記述で証明をすることはできない
      -
      -

      Continuation Based C

      +
      +

      GearsOSでの信頼性の保証

        -
      • ノーマルレベル/メタレベルの実装に適している言語 +
      • メタレベルのみで信頼性の保証を行う
          -
        • 通称CbC
          • +
        • ノーマルレベルでの記述は変更しない
        • -
      • C言語の下位言語であり、 いくつかのCコンパイラ上で実装している -
          -
        • gcc
          • -
        • llvm/clang
          • -
        -
        • +
      • Continuation Based C(CbC)をつかって、ノーマルレベルとメタレベルの分離を行う
        • +
      • C言語の下位言語であり、 いくつかのCコンパイラ上で実装している
      • C言語の構文は使用可能だが、 関数呼び出しの他に軽量継続を持つ
        • 関数呼び出し時のスタックの操作を行わずjmp命令で次の処理に移動する
          • @@ -142,8 +118,22 @@
      -
      -

      CbCとCodeGear

      +
      +

      GearsOSでの信頼性の保証

      +
        +
      • デフォルトのメタレベルの計算は自動生成される
        • +
      • 資源管理あるいは検証用のメタ計算は必要に応じて挿入する
        • +
      • これにより大きなコード変更無くモデル検査や定理証明を行うことができる
        • +
      • モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する +
          +
        • 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮
          • +
        • OSの検証に利用できるinvariantの提供
          • +
        +
        • +
      +
      +
      +

      CbCとCodeGear(ノーマルレベル)

      • 軽量継続で表現する単位をCodeGearと呼ぶ
      • CodeGearはCの関数とアセンブラの中間の様に使える
        • @@ -164,11 +154,10 @@
      • cbcで書き直したxv6のreadシステムコールの例
      -
      -

      CbCの呼び出し

      +
      +

      cbcで書き直したシステムコールディスパッチの例

        -
      • CbCはgoto文で呼び出す
        • -
      • cbcで書き直したシステムコールディスパッチの例 +
      • CbCはgoto文で呼び出す
        • 受け取ったシステムコール番号に対応するCodeGearに継続する
        @@ -185,27 +174,37 @@ }
          -
        • 呼び出し元には返ってこない
          • +
        • 呼び出し元には返ってこない +
            +
          • goto trapreturn() ユーザープログラムにディスパッチする
            • +
          • goto panic() 致命的なエラーとしてOSを止める
            • +
          • goto err() システムコールのエラー処理をしてユーザープログラムにディスパッチする
            • +
          +
      -
      +

      CbCを用いたソフトウェアの実装

        -
      • CodeGearはスタックを持てない為にデータの管理やCodeGear自体の管理をローカル変数で行えない +
      • 計算を実行するためのメモリ領域が必要
          -
        • 実際に利用するデータはスタック以外の場所で確保する必要がある
          • -
        • 確保した場所からメタ計算でデータを取り出し、 CodeGearに渡したい
          • +
        • MetaDataGearと呼ぶ
        • -
      • OS内部でノーマルレベル/メタレベルの処理の切り分けをしたい +
      • メタレベルから見た実行ではcontextとして持ち歩く
        • +
      • ノーマルレベルからはアクセスするDataGearのみが見えていて、 ポインタなどは直接は見えない
        • +
      • contextはプロセスごとに別に存在する
        • +
      • kernel内で共有されているデータ構造
          -
        • メタな計算を行うCodeGearは直接呼び出したくない
          • +
        • ページテーブル
          • +
        • ファイル構造体
          • +
        • キャッシュやバッファ
          • +
        • これらはkernel context内に置かれる
        • -
      • ノーマル/メタのCodeGearの切り分けと、データの管理をする構造を作成した
      -
      +

      CbCのcotnext

      • CbCのプログラムで利用するCodeGearとデータの組を管理する機能 @@ -227,14 +226,14 @@
      • 実際のデータの入手、保存はcontextを触ることが出来るMeta Code Gearが行う
      -
      +

      通常のCbCプログラム

      • プログラマから見るとCodeGearからCodeGearへの継続のみに見える
      -
      +

      実際のCbCプログラム

      • 実際は1度contextを参照するMetaCodeGearに継続する @@ -245,7 +244,7 @@
      -
      +

      実際のCbCプログラム

      • MetaCodeGearでは次の計算に必要なDataGearを取り出す @@ -256,16 +255,7 @@
      -
      -

      CbCのcotnext

      -
        -
      • CbCのcontextを使うことでメタ計算とノーマルレベルの計算を切り分ける事ができる
        • -
      • 計算に必要な全てのデータはcontext上に保存される
        • -
      • 使用するCodeGearの組や入出力の情報もcontextに保存される
        • -
      • これらを用いてOSを書き換えたい
        • -
      -
      -
      +

      CbCを用いたOSの再実装

      • CbCのCodeGearは状態遷移単位での記述に向いている
        • @@ -282,7 +272,7 @@
      -
      +

      xv6

      • マサチューセッツ工科大学で開発されたv6OSをもとにしたOS @@ -304,11 +294,12 @@
      -
      +

      xv6のCbCでの書き換え

      • 既存のOSを段階的にCbCで書き換えていく
          +
        • 一部スタックを持っている
        • CbCでOSを実装する際のプロトタイプ実装としての段階
        • @@ -316,7 +307,7 @@
      • CbCのcontextをプロセス構造体に埋め込み、 goto文を利用する場合はcontextからデータを参照する
      -
      +

      read system callの書き換え

      • xv6のシステムコールの一部を書き換えることを検討する
        • @@ -335,7 +326,7 @@
      -
      +

      read system callの継続の一部

      • 実際に処理を切り分けているCodeGear @@ -364,7 +355,7 @@ }
      -
      +

      read システムコールの状態遷移図

      • システムコール中のCodeGearを状態遷移図にした @@ -375,9 +366,16 @@
      -
      +

      Basic Block単位での書き換え

        +
      • Basic Blockとはコンパイラの用語でループやリターンを区切りとするプログラミング単位 +
          +
        • 長くかかるループは間にgotoを挟むことによりメタ計算を間にいれる
          • +
        • 1つのCodeGearにいる間は(論理的に)preemptされないことを保証する
          • +
        +
        • +
      • これによりCodeGearを割り込まれない検証の単位とする事ができる
      • 仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている
        • CodeGear用のAPIをいきなり設計するのではなく、 段階的に書き換える
          • @@ -390,10 +388,10 @@
      -
      +

      メモリ管理部分の書き換え

      -
      +

      まとめ

      • xv6の処理の一部を継続を用いてcbcで書き換えた