# HG changeset patch # User anatofuz # Date 1590620115 -32400 # Node ID b43d210923e782d20c10bb22698909a28d6cd3a6 # Parent 92e7655a74584168f0c297b3e44f873de0572be2 ... diff -r 92e7655a7458 -r b43d210923e7 slide/slide.html --- a/slide/slide.html Wed May 27 22:04:40 2020 +0900 +++ b/slide/slide.html Thu May 28 07:55:15 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 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%}
+/* @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%}

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,12 +118,12 @@
-
+

GearsOSでの信頼性の保証

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

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

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

CbCとCodeGear(メタレベル)

+
    +
  • cbc_read_stub内で必要な引数をcontextから取り出す +
      +
    • 取得するものがなければノーマルレベルのCodeGearに継続する
      • +
    +
    • +
+
__code cbc_read_stub(struct Context* cbc_context, enum Code next) {
+        goto cbc_read(cbc_context, next);
+}
+
+
+

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

  • CbCはgoto文で呼び出す @@ -173,17 +187,34 @@ goto (cbccodes[num])(cbc_ret); } -
      -
    • 呼び出し元には返ってこない +
+
+

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

+
void syscall(void)
+{
+    int num;
+    int ret;
+
+    if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
+        proc->cbc_arg.cbc_console_arg.num = num;
+        goto (cbccodes[num])(cbc_ret);
+    }
+
    -
  • goto trapreturn() ユーザープログラムにディスパッチする
    • -
  • goto panic() 致命的なエラーとしてOSを止める
    • -
  • goto err() システムコールのエラー処理をしてユーザープログラムにディスパッチする
    • +
  • 呼び出し元には帰らず、 特定のCodeGearに継続を行う +
      +
    • goto trapreturn() ユーザープログラムにディスパッチする
      • +
    • goto panic() 致命的なエラーとしてOSを止める
      • +
    • goto err() システムコールのエラー処理 +
        +
      • その後ユーザープログラムにディスパッチする
        • +
      +
-
+

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

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

CbCのcotnext

  • CbCのプログラムで利用するCodeGearとデータの組を管理する機能 @@ -215,25 +246,24 @@
  • ノーマルレベルのCodeGear間を遷移するようにプログラミングする
      -
    • ノーマルレベルからはCodeGearを直接操作できない +
    • ノーマルレベルからはCodeGearを直接操作できず、 メタレベルで操作する
      • メタ計算中でCodeGearの番号をcontextでディスパッチする
      • -
    • この間にMetaCodeGearが 実行される
  • 実際のデータの入手、保存はcontextを触ることが出来るMeta Code Gearが行う
-
+

通常のCbCプログラム

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

実際のCbCプログラム

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

実際のCbCプログラム

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

CbCを用いたOSの再実装

  • CbCのCodeGearは状態遷移単位での記述に向いている
  • 状態遷移を基本としたモデルに変換し、HoareLogicなどの形式手法を用いて信頼性を高めたい
    • -
  • CbCは比較的文法が簡易 -
      -
    • Agda/Coqなどの定理証明からCbCへのコード変換が可能であると考えている
      • -
    -
  • CbCや定理証明系を用いてアプリケーションとOSを再実装したい
    • 最初の段階として既存のOSをCbCで再実装する
      • @@ -272,7 +297,7 @@
-
+

xv6

  • マサチューセッツ工科大学で開発されたv6OSをもとにしたOS @@ -288,13 +313,13 @@
  • Raspberry Pi上で動作を目指したARM用のバージョンも存在する
      -
    • やっぱりRaspberryPiで動かしたい
      • +
    • RaspberryPiで動かしたい
    • 今回は ARMのバージョンをCbCで再実装する
-
+

xv6のCbCでの書き換え

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

read system callの書き換え

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

read system callの継続の一部

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

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

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

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

+
    +
  • cbc_fileread CodeGearなどは複数のCodeGearの集合となっている +
      +
    • CodeGearの数が書き換えに伴って増えてしまう
      • +
    • CbCのInterface機能によってAPI単位でCodeGearのモジュール化を行っている
      • +
    +
    • +
+ +
+

Basic Block単位での書き換え

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

    Basic Block単位での書き換え

    +
    • 仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている
        +
      • fs.cやvm.cなど
      • CodeGear用のAPIをいきなり設計するのではなく、 段階的に書き換える
      • @@ -388,10 +431,98 @@
    -
    -

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

    +
    +

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

    +
      +
    • ファイルシステムのAPIが実装されているfs.cのAPIからCodeGearの集合を定義する +
        +
      • 実装にはCbCのInterfaceを用いる
        • +
      • 各APIの内部は複数のCodeGearの継続として実装する
        • +
      +
      • +
    +
    typedef struct fs<Type,Impl> {
+    __code readsb(Impl* fs, uint dev, struct superblock* sb, __code next(...));
+    __code iinit(Impl* fs, __code next(...));
+    __code ialloc(Impl* fs, uint dev, short type, __code next(...));
+    __code iupdate(Impl* fs, struct inode* ip, __code next(...));
+    __code idup(Impl* fs, struct inode* ip, __code next(...));
+    __code ilock(Impl* fs, struct inode* ip, __code next(...));
+    __code iunlock(Impl* fs, struct inode* ip, __code next(...));
+    __code iput(Impl* fs, struct inode* ip, __code next(...));
+....
+} fs;
+
    +
    +
    +

    もとのialloc関数

    +
      +
    • inodeのアロケーションを行うialloc関数を書き換えた
      • +
    +
    struct inode* ialloc (uint dev, short type)
+{
+    readsb(dev, &sb);
+    for (inum = 1; inum < sb.ninodes; inum++) {
+        bp = bread(dev, IBLOCK(inum));
+        dip = (struct dinode*) bp->data + inum % IPB;
+
+        if (dip->type == 0) {  // a free inode
+            memset(dip, 0, sizeof(*dip));
+            ...
+            return iget(dev, inum);
+        }
+        brelse(bp);
+    }
+    panic("ialloc: no inodes");
+}
+
    -
    +
    +

    ialloc関数

    +
      +
    • 対象のデバイスのinodeを一つずつ取り出すループ処理
      • +
    • 空のinodeがあれば0で初期化後にigetでポインタを返す
      • +
    • アロケーションができなければpanicする
      • +
    +
    struct inode* ialloc (uint dev, short type)
+{
+    readsb(dev, &sb);
+    for (inum = 1; inum < sb.ninodes; inum++) {
+        bp = bread(dev, IBLOCK(inum));
+        dip = (struct dinode*) bp->data + inum % IPB;
+
+        if (dip->type == 0) {  // a free inode
+            memset(dip, 0, sizeof(*dip));
+            ...
+            return iget(dev, inum);
+        }
+        brelse(bp);
+    }
+    panic("ialloc: no inodes");
+}
+
    +
    +
    +

    ループ条件の確認のCodeGear

    +
      +
    • CbCでループ条件の判定を行うCodeGearを実装した +
        +
      • for (inum = 1; inum < sb.ninodes; inum++)に対応する
        • +
      • ループ条件を満たなかった場合はpanicに移動する
        • +
      +
      • +
    +
    __code allocinode_loopcheck(struct fs_impl* fs_impl, uint inum,  struct superblock* sb, __code next(...)){
+    if( inum < sb->ninodes){
+        goto allocinode_loop(fs_impl, next(...));
+    }
+    char* msg = "failed allocinode...";
+    struct Err* err = createKernelError(&kernel->cbc_context);
+    goto err->panic(msg);
+}
+
    +
    +

    まとめ

    • xv6の処理の一部を継続を用いてcbcで書き換えた diff -r 92e7655a7458 -r b43d210923e7 slide/slide.md --- a/slide/slide.md Wed May 27 22:04:40 2020 +0900 +++ b/slide/slide.md Thu May 28 07:55:15 2020 +0900 @@ -75,7 +75,7 @@ - デフォルトのメタレベルの計算は自動生成される - 資源管理あるいは検証用のメタ計算は必要に応じて挿入する -- これにより大きなコード変更無くモデル検査や定理証明を行うことができる +- これにより大きなコード変更が無くモデル検査や定理証明を行うことができる - モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮 - OSの検証に利用できるinvariantの提供 @@ -100,6 +100,19 @@ ``` - cbcで書き直したxv6の`read`システムコールの例 + +--- +# CbCとCodeGear(メタレベル) + +- `cbc_read_stub`内で必要な引数をcontextから取り出す + - 取得するものがなければノーマルレベルのCodeGearに継続する + +```c +__code cbc_read_stub(struct Context* cbc_context, enum Code next) { + goto cbc_read(cbc_context, next); +} +``` + --- # cbcで書き直したシステムコールディスパッチの例 @@ -118,10 +131,28 @@ } ``` -- 呼び出し元には返ってこない - - goto trapreturn() ユーザープログラムにディスパッチする - - goto panic() 致命的なエラーとしてOSを止める - - goto err() システムコールのエラー処理をしてユーザープログラムにディスパッチする +--- + +# cbcで書き直したシステムコールディスパッチの例 + + +```c +void syscall(void) +{ + int num; + int ret; + + if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) { + proc->cbc_arg.cbc_console_arg.num = num; + goto (cbccodes[num])(cbc_ret); + } +``` + +- 呼び出し元には帰らず、 特定のCodeGearに継続を行う + - `goto trapreturn()` ユーザープログラムにディスパッチする + - `goto panic()` 致命的なエラーとしてOSを止める + - `goto err()` システムコールのエラー処理 + - その後ユーザープログラムにディスパッチする --- @@ -145,9 +176,8 @@ - データをDataGearという単位として扱う - 計算で使用する各DataGearを実際に保存している - ノーマルレベルのCodeGear間を遷移するようにプログラミングする - - ノーマルレベルからはCodeGearを直接操作できない + - ノーマルレベルからはCodeGearを直接操作できず、 メタレベルで操作する - メタ計算中でCodeGearの番号をcontextでディスパッチする - - この間にMetaCodeGearが 実行される - 実際のデータの入手、保存はcontextを触ることが出来るMeta Code Gearが行う --- @@ -182,8 +212,6 @@ - CbCのCodeGearは状態遷移単位での記述に向いている - 状態遷移を基本としたモデルに変換し、HoareLogicなどの形式手法を用いて信頼性を高めたい -- CbCは比較的文法が簡易 - - Agda/Coqなどの定理証明からCbCへのコード変換が可能であると考えている - CbCや定理証明系を用いてアプリケーションとOSを再実装したい - 最初の段階として既存のOSをCbCで再実装する @@ -197,7 +225,7 @@ - 基本的な機能は実装されている - システムコール、 ファイルシステム、 プロセス処理... - Raspberry Pi上で動作を目指したARM用のバージョンも存在する - - やっぱりRaspberryPiで動かしたい + - RaspberryPiで動かしたい - 今回は ARMのバージョンをCbCで再実装する @@ -261,21 +289,121 @@ --- +# システムコール単位での書き換え +- `cbc_fileread` CodeGearなどは複数のCodeGearの集合となっている + - CodeGearの数が書き換えに伴って増えてしまう + - CbCのInterface機能によってAPI単位でCodeGearのモジュール化を行っている + + + +--- + # Basic Block単位での書き換え - Basic Blockとはコンパイラの用語でループやリターンを区切りとするプログラミング単位 - 長くかかるループは間にgotoを挟むことによりメタ計算を間にいれる - 1つのCodeGearにいる間は(論理的に)preemptされないことを保証する - これによりCodeGearを割り込まれない検証の単位とする事ができる + + +--- +# Basic Block単位での書き換え + - 仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている + - `fs.c`や`vm.c`など - CodeGear用のAPIをいきなり設計するのではなく、 段階的に書き換える - 今回はこれらの関数の内容をCodeGearで書き直した - 各関数への呼び出し時にダミーの関数を呼び出すことでCとCbCの相互移動が可能 --- -# メモリ管理部分の書き換え +# ファイルシステム操作の書き換え + +- ファイルシステムのAPIが実装されている`fs.c`のAPIからCodeGearの集合を定義する + - 実装にはCbCのInterfaceを用いる + - 各APIの内部は複数のCodeGearの継続として実装する + +```c +typedef struct fs { + __code readsb(Impl* fs, uint dev, struct superblock* sb, __code next(...)); + __code iinit(Impl* fs, __code next(...)); + __code ialloc(Impl* fs, uint dev, short type, __code next(...)); + __code iupdate(Impl* fs, struct inode* ip, __code next(...)); + __code idup(Impl* fs, struct inode* ip, __code next(...)); + __code ilock(Impl* fs, struct inode* ip, __code next(...)); + __code iunlock(Impl* fs, struct inode* ip, __code next(...)); + __code iput(Impl* fs, struct inode* ip, __code next(...)); +.... +} fs; +``` + +--- +# もとのialloc関数 +- inodeのアロケーションを行う`ialloc`関数を書き換えた + +```c +struct inode* ialloc (uint dev, short type) +{ + readsb(dev, &sb); + for (inum = 1; inum < sb.ninodes; inum++) { + bp = bread(dev, IBLOCK(inum)); + dip = (struct dinode*) bp->data + inum % IPB; + + if (dip->type == 0) { // a free inode + memset(dip, 0, sizeof(*dip)); + ... + return iget(dev, inum); + } + brelse(bp); + } + panic("ialloc: no inodes"); +} +``` +--- +# ialloc関数 + +- 対象のデバイスのinodeを一つずつ取り出すループ処理 +- 空のinodeがあれば0で初期化後に`iget`でポインタを返す +- アロケーションができなければpanicする + +```c +struct inode* ialloc (uint dev, short type) +{ + readsb(dev, &sb); + for (inum = 1; inum < sb.ninodes; inum++) { + bp = bread(dev, IBLOCK(inum)); + dip = (struct dinode*) bp->data + inum % IPB; + + if (dip->type == 0) { // a free inode + memset(dip, 0, sizeof(*dip)); + ... + return iget(dev, inum); + } + brelse(bp); + } + panic("ialloc: no inodes"); +} +``` + +--- + +# ループ条件の確認のCodeGear + +- CbCでループ条件の判定を行うCodeGearを実装した + - `for (inum = 1; inum < sb.ninodes; inum++)`に対応する + - ループ条件を満たなかった場合はpanicに移動する + +```c +__code allocinode_loopcheck(struct fs_impl* fs_impl, uint inum, struct superblock* sb, __code next(...)){ + if( inum < sb->ninodes){ + goto allocinode_loop(fs_impl, next(...)); + } + char* msg = "failed allocinode..."; + struct Err* err = createKernelError(&kernel->cbc_context); + goto err->panic(msg); +} +``` --- # まとめ