# HG changeset patch # User ikkun # Date 1590624399 -32400 # Node ID d460c442d596dc22a70958188187cf2738611469 # Parent 43d413be71c4d43201cf4313d598d2ca919ec5ce fix diff -r 43d413be71c4 -r d460c442d596 presen/sigos.html --- a/presen/sigos.html Thu May 28 01:39:29 2020 +0900 +++ b/presen/sigos.html Thu May 28 09:06:39 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 za9t5jbg9rpnsigrrkzqv5ozsjj37semsamptgsyysj */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 cogs0ys78vbpl4r4b4kisjkzjeosxlddkvql93vwbme */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%}

Gears OSでモデル検査を実現する手法について

  • 東恩納 琢偉 @@ -22,15 +22,15 @@
-
+

研究目的

  • OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る。
  • 本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、今回はモデル検査による信頼性の保証について考察する。
    • -
  • またGearsOS そのものをGearsOS上でモデル検査することに関しても考察する。
    • +
  • またGearsOS そのものをGearsOS上でモデル検査する手法について考察する。
-
+

Gears OS

  • 軽量継続を基本とする言語 Contnution based C を用いて記述されている。
    • @@ -38,10 +38,10 @@
  • 信頼性を保証する方法としてモデル検査による検証や、定理証明を用いる事で、信頼性へのアプローチを行っています。
-
+

Continution based C

    -
  • CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear　という単位で遷移する。
    • +
  • CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear という単位で遷移する。
  • goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。
  • 以下は CbC によって記述された codeGear です。
@@ -57,7 +57,7 @@ }
-
+

goto

  • goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。
    • @@ -66,7 +66,7 @@
-
+

dataGear と meta dataGear

  • CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル
    @@ -74,7 +74,7 @@
  • メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearを格納するcontext などがある。context は一般的なOSのプロセスに相当する。
-
+

stub CodeGear

  • メタレベルから見ると、code Gearの入力はcontext ただ1つである。
    • @@ -93,15 +93,15 @@ }
-
-

cotntextと状態数

+
+

contextと状態数

  • プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。
  • 並列実行の非決定性は、同時に実行される codeGear の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。
  • しかし、このcontextの状態はとても巨大になる事がある、そのためそれらを抽象化する必要性がある。
-
+

GearsOSの実装

  • codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。
    • @@ -109,21 +109,21 @@
  • しかし、GearsOSにおいては正しく実行される事を保証されるように実装されているとする。
-
+

モデル検査

  • モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。
    • -
  • このモデルが仕様を満たしているかどうかを検査するものである。

状態遷移モデル
論理モデル
組み合わせモデル
フローモデル ..etc

    +
  • このモデルが仕様を満たしているかどうかを検査するのがモデル検査である。
  • 検査の要点によってモデルを使い分ける必要性がある。
-
+

状態遷移モデル

  • 今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。
    • @@ -160,15 +160,16 @@
-
+

既存のモデル検査手法(SPIN)

    +
  • 一般的に扱われるモデル検査ツールとしてSPINがある。
  • SPIN はPromela (Process Meta Language)で記述される。
  • C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語であり、検証機を生成し、コンパイルと実行を行うことで検証される。
    • -
  • チャネルを使って通信や並列動作を記述する
    • +
  • チャネルを使って通信や並列動作を記述する。
  • 有限オートマトンに変換してモデル検査を行う。
  • Promelaへの書き換えが必要
    • -
  • SPIN では以下の性質を検査可能な性質
    +
  • SPIN での検査可能な性質
    アサーション
    デッドロック
    到達性
    @@ -176,50 +177,50 @@ 線形時相論理で記述された仕様
-
+

既存のモデル検査手法(Java path Finder)

  • Java Path Finder はjavaプログラムの検査ツール
  • java バーチャルマシン(JVM) を直接シュミレーション実行している、これによりjavaのバイトコードを直接実行可能である。
  • バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査している。
    • -
  • 実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して実行する必要がある。
    • -
  • JPF では以下の性質を検査することができる
    +
  • 実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して検査する必要がある。
    • +
  • JPF で検査可能な性質
    スレッドの可能な実行すべてを調べる
    デッドロックの検出
    アサーション
    Partial Order Reduction
-
+

モデル検査手法について

  • GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。
    • -
  • codegear 実行後の状態を検査し、データベースに格納する。
    • -
  • 新しい上体が生成されなくなった時モデル検査が終了する。
    • +
  • codegear 実行後の状態を、データベースに格納する。
    • +
  • 新しい状態が生成されなくなった時モデル検査が終了する。
  • 哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。
  • 必要な状態はフォークの状態だけになるので、それ以外の状態は無視することができる。
  • これにより状態数を下げることができる。
  • つまり、問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。
    • -
  • GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。
    • +
  • GearsOS による検証用プログラムとして Dining Philosohers Ploblem (DPP）を用いる。
-
-

DPP

+
+

DPP(dining philosohers ploblem)

  • 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。
    • -
  • フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。
    • +
  • フォークは皿の間に１本ずつの計5本しかないため、すべての哲学者が同時に食事することはできず、また全員がフォークを1本ずつ持ってしまった場合、誰も食事することは出来ない。この状態をデッドロックとする。
-
+
-
+

DPP

  • 状態は以下の構成要素からなる
    Pickup Right fork Pickup Left fork eating Put Right fork Put Left fork Thinking
-

+

-
+

GeasOS におけるDPP実装(1/3)

  • 5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。
    • @@ -228,7 +229,7 @@
  • par goto は複数スレッドでの実行であるので、各スレッドで実行後に__exitに継続する事で終了する。
-
+

GearsOS におけるDPP実装(2/3)

  • マルチスレッドでのデータの一貫性を保証する手法としてCAS がある。
    • @@ -237,22 +238,22 @@
  • DPPの例題ではフォークがスレッドで共有されるデータにあたるので、synchronixed Queue を用いることによってスレッド間での同期を行う。
-
+

GearsOS におけるDPP実装(3/3)

+

v- 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。

    -
  • 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。
  • この状態遷移は goto next によって遷移し、metaCodeGear を 挟みメタレベルで各スレッドの状態を 各スレッドごとに用意した Memory Tree に保存する。
  • Memory Tree はstateDBによってまとめられ、同じ状態は共有される。
  • またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。
-
+

GearsOS でのモデル検査を実現する手法について

  • DPP をGearsOS 上のアプリケーションとして実装する。
    • -
  • DPP codeGear のシャッフルの１つとして実行する。
    • -
  • 可能な実行を生成するiterator を作成する
    • -
  • 状態を記録するmemory Tree とstateDBを作成する。
    • +
  • DPP を codeGear のシャッフルの１つとして実行する。
    • +
  • 可能な実行を生成する iterator を作成する
    • +
  • 状態を記録する memory Tree と stateDB を作成する。