# HG changeset patch # User ikkun # Date 1590597569 -32400 # Node ID 43d413be71c4d43201cf4313d598d2ca919ec5ce # Parent eeaaa64b291618cc7cd455bf2453a30ed92e516b fix diff -r eeaaa64b2916 -r 43d413be71c4 presen/sigos.html --- a/presen/sigos.html Thu May 28 01:31:29 2020 +0900 +++ b/presen/sigos.html Thu May 28 01:39:29 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 vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr */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 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%}

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

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

研究目的

  • OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る。
    • @@ -30,7 +30,7 @@
  • またGearsOS そのものをGearsOS上でモデル検査することに関しても考察する。
-
+

Gears OS

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

Continution based C

  • CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて 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,7 +93,7 @@ }
-
+

cotntextと状態数

  • プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。
    • @@ -101,7 +101,7 @@
  • しかし、このcontextの状態はとても巨大になる事がある、そのためそれらを抽象化する必要性がある。
-
+

GearsOSの実装

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

モデル検査

  • モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。
    • @@ -123,21 +123,44 @@
  • 検査の要点によってモデルを使い分ける必要性がある。
-
+

状態遷移モデル

  • 今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。
  • 状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。
    • -
  • 構成要素としては以下のような物がある。
-

| ---------- | --------------------------------- |
-| 状態 | プログラムの状態 |
-| 初期状態 |何らかの処理、計算が行われる前の状態|
-| 終了状態 |処理、または計算が行われた状態 |
-| 処理(計算) |状態を変化させる |
-| 遷移条件 |状態が分岐する際の条件 |

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
構成要素
状態プログラムの状態
初期状態何らかの処理、計算が行われる前の状態
終了状態処理、または計算が行われた状態
処理(計算)状態を変化させる
遷移条件状態が分岐する際の条件
-
+

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

  • SPIN はPromela (Process Meta Language)で記述される。
    • @@ -153,7 +176,7 @@ 線形時相論理で記述された仕様
-
+

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

  • Java Path Finder はjavaプログラムの検査ツール
    • @@ -167,8 +190,8 @@ Partial Order Reduction
-
-

+
+

モデル検査手法について

  • GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。
  • codegear 実行後の状態を検査し、データベースに格納する。
    • @@ -180,27 +203,23 @@
  • GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。
-
+

DPP

  • 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。
  • フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。
-
+
-
+

DPP

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

+

-
+

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

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

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

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

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

  • 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。
    • @@ -227,7 +246,7 @@
  • またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。
-
+

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

  • DPP をGearsOS 上のアプリケーションとして実装する。
    • diff -r eeaaa64b2916 -r 43d413be71c4 presen/sigos.md --- a/presen/sigos.md Thu May 28 01:31:29 2020 +0900 +++ b/presen/sigos.md Thu May 28 01:39:29 2020 +0900 @@ -118,8 +118,8 @@ - 今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。 - 状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。 -- 構成要素としては以下のような物がある。 +| 構成要素 | | | ---------- | --------------------------------- | | 状態 | プログラムの状態 | | 初期状態 |何らかの処理、計算が行われる前の状態| @@ -159,7 +159,7 @@ --- -# +# モデル検査手法について - GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。 - codegear 実行後の状態を検査し、データベースに格納する。 - 新しい上体が生成されなくなった時モデル検査が終了する。 @@ -175,20 +175,16 @@ - 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。 - フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。 -
    +
    --- # DPP - 状態は以下の構成要素からなる -Pickup Right -fork Pickup -Left fork eating Put Right fork - Put Left fork - Thinking +`Pickup Right fork` ` Pickup Left fork` `eating` ` Put Right fork` `Put Left fork` ` Thinking ` - + ---