# HG changeset patch # User anatofuz # Date 1590626505 -32400 # Node ID be3419709cd323b36a101a272e3601f784bb43f5 # Parent d1fe7f17320d762bda244bc34118a5874bb1cc23 ... diff -r d1fe7f17320d -r be3419709cd3 slide/slide.html --- a/slide/slide.html Thu May 28 09:04:44 2020 +0900 +++ b/slide/slide.html Thu May 28 09:41:45 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 j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict */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 mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis */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,7 +27,7 @@
-
+

研究目的

  • アプリケーションの信頼性を向上させたい @@ -44,7 +44,7 @@
-
+

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

  • プログラムの実行部分は以下の2つからなる @@ -65,7 +65,7 @@
  • メタレベルの計算として信頼性を保証する
-
+

モデル検査

  • 実際に想定されるパターンを全て動かして検証する
    • @@ -78,7 +78,7 @@
  • Spinを用いる方法では、 promelaという言語で実装し直す必要がある
-
+

定理証明支援系

  • 論理学的なモデルに変更して証明する @@ -100,7 +100,7 @@
-
+

GearsOSでの信頼性の保証

  • メタレベルのみで信頼性の保証を行う @@ -118,7 +118,7 @@
-
+

GearsOSでの信頼性の保証

  • デフォルトのメタレベルの計算は自動生成される
    • @@ -130,9 +130,10 @@
  • OSの検証に利用できるinvariantの提供
+
  • CbCを用いたOSであるGearsOSを開発している
    • -
    +

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

    • 軽量継続で表現する単位をCodeGearと呼ぶ
      • @@ -154,7 +155,7 @@
    • cbcで書き直したxv6のreadシステムコールの例
    -
    +

    CbCとCodeGear(メタレベル)

    • cbc_read_stub内で必要な引数をcontextから取り出す @@ -168,7 +169,7 @@ }
    -
    +

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

    • CbCはgoto文で呼び出す @@ -188,7 +189,7 @@ }
    -
    +

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

    void syscall(void)
 {
@@ -214,7 +215,7 @@
 
 
 
-
    
+
    
 
    CbCを用いたソフトウェアの実装
    
 
      
 
    • 計算を実行するためのメモリ領域が必要
@@ -235,7 +236,7 @@
 
      • 
 
    
 
    
-
    
+
    
 
    CbCのcotnext
    
 
      
 
    • CbCのプログラムで利用するCodeGearとデータの組を管理する機能
@@ -256,14 +257,14 @@
 
    • 実際のデータの入手、保存はcontextを触ることが出来るMeta Code Gearが行う
      • 
 
    
 
    
-
    
+
    
 
    通常のCbCプログラム
    
 
      
 
    • プログラマから見るとCodeGearからCodeGearへの継続のみに見える
      
 
      • 
 
    
 
    
-
    
+
    
 
    実際のCbCプログラム
    
 
      
 
    • 実際は1度contextを参照するMetaCodeGearに継続する
@@ -274,7 +275,7 @@
 
    
 
 
    
-
    
+
    
 
    実際のCbCプログラム
    
 
      
 
    • MetaCodeGearでは次の計算に必要なDataGearを取り出す
@@ -285,7 +286,7 @@
 
    
 
 
    
-
    
+
    
 
    CbCを用いたOSの再実装
    
 
      
 
    • CbCのCodeGearは状態遷移単位での記述に向いている
      • 
@@ -297,7 +298,7 @@
 
 
    
 
    
-
    
+
    
 
    xv6
    
 
      
 
    • マサチューセッツ工科大学で開発されたv6OSをもとにしたOS
@@ -319,7 +320,7 @@
 
      • 
 
    
 
    
-
    
+
    
 
    xv6のCbCでの書き換え
    
 
      
 
    • 既存のOSを段階的にCbCで書き換えていく
@@ -332,7 +333,7 @@
 
    • CbCのcontextをプロセス構造体に埋め込み、 goto文を利用する場合はcontextからデータを参照する
      • 
 
    
 
    
-
    
+
    
 
    read system callの書き換え
    
 
      
 
    • xv6のシステムコールの一部を書き換えることを検討する
      • 
@@ -351,7 +352,7 @@
 
 
    
 
    
-
    
+
    
 
    read system callの継続の一部
    
 
      
 
    • 実際に処理を切り分けているCodeGear
@@ -380,7 +381,7 @@
 }
 
 
    
-
    
+
    
 
    read システムコールの状態遷移図
    
 
      
 
    • システムコール中のCodeGearを状態遷移図にした
@@ -391,7 +392,7 @@
 
      • 
 
    
 
    
-
    
+
    
 
    システムコール単位での書き換え
    
 
      
 
    • cbc_fileread CodeGearなどは複数のCodeGearの集合となっている
@@ -403,7 +404,7 @@
 
    
 
 
    
-
    
+
    
 
    Basic Block単位での書き換え
    
 
      
 
    • Basic Blockとはコンパイラの用語でループやリターンを区切りとするプログラミング単位
@@ -415,7 +416,7 @@
 
    • これによりCodeGearを割り込まれない検証の単位とする事ができる
      • 
 
    
 
    
-
    
+
    
 
    Basic Block単位での書き換え
    
 
      
 
    • 仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている
@@ -431,7 +432,7 @@
 
      • 
 
    
 
    
-
    
+
    
 
    ファイルシステム操作の書き換え
    
 
      
 
    • ファイルシステムのAPIが実装されているfs.cのAPIからCodeGearの集合を定義する
@@ -454,7 +455,7 @@
 } fs;
 
 
    
-
    
+
    
 
    もとのialloc関数
    
 
      
 
    • inodeのアロケーションを行うialloc関数を書き換えた
      • 
@@ -477,7 +478,7 @@
 }
 
 
    
-
    
+
    
 
    ialloc関数
    
 
      
 
    • 対象のデバイスのinodeを一つずつ取り出すループ処理
      • 
@@ -502,8 +503,8 @@
 }
 
 
    
-
    
-
    ループ条件の確認のCodeGear
    
+
    
+
    ループ条件の確認のCodeGear(ノーマルレベル)
    
 
      
 
    • CbCでループ条件の判定を行うCodeGearを実装した
 
        
@@ -522,8 +523,22 @@
 }
 
 
    
-
    
-
    ループに復帰するかの判定
    
+
    
+
    ループ条件の確認のCodeGear(メタレベル)
    
+
      
+
    • ノーマルレベルの直前に実行され、contextから値を取り出す
      • 
+
    
+
    __code allocinode_loopcheck_stub(struct Context* cbc_context) {
+        fs_impl* fs_impl = Gearef(cbc_context, fs_impl);
+        uint inum = Gearef(cbc_context, fs_impl)->inum;
+        superblock* sb = Gearef(cbc_context, fs_impl)->sb;
+        enum Code next = Gearef(cbc_context, fs_impl)->next;
+        goto allocinode_loopcheck(cbc_context, fs_impl, inum, sb, next);
+}
+
    
+
    
+
    
+
    ループに復帰するかの判定(ノーマルレベル)
    
 
      
 
    • 空のinodeがあるかどうか(dip->type == 0)で継続を分岐させる
 
        
@@ -546,7 +561,21 @@
 }
 
 
    
-
    
+
    
+
    ループに復帰するかの判定(メタレベル)
    
+
      
+
    • 同様に計算に必要は値を取り出して継続する
      • 
+
    
+
    __code allocinode_loop_stub(struct Context* cbc_context) {
+        fs_impl* fs_impl = Gearef(cbc_context, fs_impl);
+        uint inum = Gearef(cbc_context, fs_impl)->inum;
+        short type = Gearef(cbc_context, fs_impl)->type;
+        enum Code next = Gearef(cbc_context, fs_impl)->next;
+        goto allocinode_loop(cbc_context, fs_impl, inum, type, next);
+}
+
    
+
    
+
    
 
    BasicBlock単位での書き換えの考察
    
 
      
 
    • 従来のxv6の関数呼び出しをもとにしているために、コードの変更点が少ない
      • 
@@ -558,7 +587,7 @@
 
 
    
 
    
-
    
+
    
 
    まとめ
    
 
      
 
    • xv6の処理の一部を継続を用いてcbcで書き換えた
diff -r d1fe7f17320d -r be3419709cd3 slide/slide.md
--- a/slide/slide.md	Thu May 28 09:04:44 2020 +0900
+++ b/slide/slide.md	Thu May 28 09:41:45 2020 +0900
@@ -79,6 +79,7 @@
 - モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する
     - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮
     - OSの検証に利用できるinvariantの提供
+- CbCを用いたOSであるGearsOSを開発している
 
 ---
 # CbCとCodeGear(ノーマルレベル)
@@ -388,7 +389,7 @@
 
 ---
 
-# ループ条件の確認のCodeGear
+# ループ条件の確認のCodeGear(ノーマルレベル)
 
 - CbCでループ条件の判定を行うCodeGearを実装した
     - `for (inum = 1; inum < sb.ninodes; inum++)`に対応する
@@ -406,8 +407,23 @@
 ```
 
 ---
+# ループ条件の確認のCodeGear(メタレベル)
 
-# ループに復帰するかの判定
+- ノーマルレベルの直前に実行され、contextから値を取り出す
+
+```c
+__code allocinode_loopcheck_stub(struct Context* cbc_context) {
+        fs_impl* fs_impl = Gearef(cbc_context, fs_impl);
+        uint inum = Gearef(cbc_context, fs_impl)->inum;
+        superblock* sb = Gearef(cbc_context, fs_impl)->sb;
+        enum Code next = Gearef(cbc_context, fs_impl)->next;
+        goto allocinode_loopcheck(cbc_context, fs_impl, inum, sb, next);
+}
+```
+
+---
+
+# ループに復帰するかの判定(ノーマルレベル)
 - 空のinodeがあるかどうか(`dip->type == 0)`で継続を分岐させる
     - 0のものがあった場合は初期化を行うCodeGearに遷移する
     - なければループ条件の確認のCodeGearに継続する
@@ -428,6 +444,21 @@
 ```
 
 ---
+# ループに復帰するかの判定(メタレベル)
+
+- 同様に計算に必要は値を取り出して継続する
+
+```c
+__code allocinode_loop_stub(struct Context* cbc_context) {
+        fs_impl* fs_impl = Gearef(cbc_context, fs_impl);
+        uint inum = Gearef(cbc_context, fs_impl)->inum;
+        short type = Gearef(cbc_context, fs_impl)->type;
+        enum Code next = Gearef(cbc_context, fs_impl)->next;
+        goto allocinode_loop(cbc_context, fs_impl, inum, type, next);
+}
+```
+
+---
 # BasicBlock単位での書き換えの考察
 
 - 従来のxv6の関数呼び出しをもとにしているために、コードの変更点が少ない
@@ -435,6 +466,7 @@
 - APIそのものはCodeGearを基本とした状態に書き直していない
     - スタックを前提とした処理と共存している
 
+
 ---
 # まとめ
 - xv6の処理の一部を継続を用いてcbcで書き換えた