# HG changeset patch # User anatofuz # Date 1590624284 -32400 # Node ID d1fe7f17320d762bda244bc34118a5874bb1cc23 # Parent b43d210923e782d20c10bb22698909a28d6cd3a6 update diff -r b43d210923e7 -r d1fe7f17320d slide/slide.html --- a/slide/slide.html Thu May 28 07:55:15 2020 +0900 +++ b/slide/slide.html Thu May 28 09:04:44 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 v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79 */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 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%}

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での信頼性の保証

  • デフォルトのメタレベルの計算は自動生成される
    • @@ -132,7 +132,7 @@
-
+

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

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

CbCとCodeGear(メタレベル)

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

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

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

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

void syscall(void)
 {
@@ -214,7 +214,7 @@
 
 
 
-

+

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

 
    
 
  • 計算を実行するためのメモリ領域が必要
@@ -235,7 +235,7 @@
 
    • 
 

 

-

+

 
CbCのcotnext

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

 

-

+

 
通常のCbCプログラム

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

 

-

+

 
実際のCbCプログラム

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

 
 

-

+

 
実際のCbCプログラム

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

 
 

-

+

 
CbCを用いたOSの再実装

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

 

-

+

 
xv6

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

 

-

+

 
xv6のCbCでの書き換え

 
    
 
  • 既存のOSを段階的にCbCで書き換えていく
@@ -332,7 +332,7 @@
 
  • CbCのcontextをプロセス構造体に埋め込み、 goto文を利用する場合はcontextからデータを参照する
    • 
 

 

-

+

 
read system callの書き換え

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

 

-

+

 
read system callの継続の一部

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

-

+

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

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

 

-

+

 
システムコール単位での書き換え

 
    
 
  • cbc_fileread CodeGearなどは複数のCodeGearの集合となっている
@@ -403,7 +403,7 @@
 

 
 

-

+

 
Basic Block単位での書き換え

 
    
 
  • Basic Blockとはコンパイラの用語でループやリターンを区切りとするプログラミング単位
@@ -415,7 +415,7 @@
 
  • これによりCodeGearを割り込まれない検証の単位とする事ができる
    • 
 

 

-

+

 
Basic Block単位での書き換え

 
    
 
  • 仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている
@@ -431,7 +431,7 @@
 
    • 
 

 

-

+

 
ファイルシステム操作の書き換え

 
    
 
  • ファイルシステムのAPIが実装されているfs.cのAPIからCodeGearの集合を定義する
@@ -454,7 +454,7 @@
 } fs;
 
 

-

+

 
もとのialloc関数

 
    
 
  • inodeのアロケーションを行うialloc関数を書き換えた
    • 
@@ -477,7 +477,7 @@
 }
 
 

-

+

 
ialloc関数

 
    
 
  • 対象のデバイスのinodeを一つずつ取り出すループ処理
    • 
@@ -502,13 +502,13 @@
 }
 
 

-

+

 
ループ条件の確認のCodeGear

 
    
 
  • CbCでループ条件の判定を行うCodeGearを実装した
 
      
 
    • for (inum = 1; inum < sb.ninodes; inum++)に対応する
      • 
-
    • ループ条件を満たなかった場合はpanicに移動する
      • 
+
    • ループ条件を満たなかった場合はpanicに継続する
      • 
 
    
 
    • 
 

@@ -522,7 +522,43 @@
 }
 
 

-

+

+
ループに復帰するかの判定

+
    
+
  • 空のinodeがあるかどうか(dip->type == 0)で継続を分岐させる
+
      
+
    • 0のものがあった場合は初期化を行うCodeGearに遷移する
      • 
+
    • なければループ条件の確認のCodeGearに継続する
      • 
+
    
+
    • 
+
  • 次のCodeGearへの引数の整合性の確認はメタ計算で実行される
    • 
+

+
__code allocinode_loop(struct fs_impl* fs_impl, uint inum, short type,   __code next(...)){
+    bp = bread(dev, IBLOCK(inum));
+    dip = (struct dinode*) bp->data + inum % IPB;
+    if(dip->type == 0){
+        goto allocinode_loopexit(fs_impl, inum,  bp, dip, next(...));
+    }
+
+    brelse(bp);
+    inum++;
+    goto allocinode_loopcheck(fs_impl, next(...));
+}
+

+

+

+
BasicBlock単位での書き換えの考察

+
    
+
  • 従来のxv6の関数呼び出しをもとにしているために、コードの変更点が少ない
    • 
+
  • CodeGearへの変換を機械的に行うことが可能
    • 
+
  • APIそのものはCodeGearを基本とした状態に書き直していない
+
      
+
    • スタックを前提とした処理と共存している
      • 
+
    
+
    • 
+

+

+

 
まとめ

 
    
 
  • xv6の処理の一部を継続を用いてcbcで書き換えた
diff -r b43d210923e7 -r d1fe7f17320d slide/slide.md
--- a/slide/slide.md	Thu May 28 07:55:15 2020 +0900
+++ b/slide/slide.md	Thu May 28 09:04:44 2020 +0900
@@ -392,7 +392,7 @@
 
 - CbCでループ条件の判定を行うCodeGearを実装した
     - `for (inum = 1; inum < sb.ninodes; inum++)`に対応する
-    - ループ条件を満たなかった場合はpanicに移動する
+    - ループ条件を満たなかった場合はpanicに継続する
 
 ```c
 __code allocinode_loopcheck(struct fs_impl* fs_impl, uint inum,  struct superblock* sb, __code next(...)){
@@ -406,6 +406,36 @@
 ```
 
 ---
+
+# ループに復帰するかの判定
+- 空のinodeがあるかどうか(`dip->type == 0)`で継続を分岐させる
+    - 0のものがあった場合は初期化を行うCodeGearに遷移する
+    - なければループ条件の確認のCodeGearに継続する
+- 次のCodeGearへの引数の整合性の確認はメタ計算で実行される
+
+```c
+__code allocinode_loop(struct fs_impl* fs_impl, uint inum, short type,   __code next(...)){
+    bp = bread(dev, IBLOCK(inum));
+    dip = (struct dinode*) bp->data + inum % IPB;
+    if(dip->type == 0){
+        goto allocinode_loopexit(fs_impl, inum,  bp, dip, next(...));
+    }
+
+    brelse(bp);
+    inum++;
+    goto allocinode_loopcheck(fs_impl, next(...));
+}
+```
+
+---
+# BasicBlock単位での書き換えの考察
+
+- 従来のxv6の関数呼び出しをもとにしているために、コードの変更点が少ない
+- CodeGearへの変換を機械的に行うことが可能
+- APIそのものはCodeGearを基本とした状態に書き直していない
+    - スタックを前提とした処理と共存している
+
+---
 # まとめ
 - xv6の処理の一部を継続を用いてcbcで書き換えた
   - システムコールに着目する手法