# HG changeset patch # User ikkun # Date 1590581494 -32400 # Node ID 9c8a9f059ddfe26e7fb2c742ddee2168c236b87e # Parent 6389876c941ade4568f8c181c917639b3b92dea8 fix diff -r 6389876c941a -r 9c8a9f059ddf presen/sigos.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presen/sigos.html Wed May 27 21:11:34 2020 +0900 @@ -0,0 +1,231 @@ +Gears OSでモデル検査を実現する手法について
+

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

+
    +
  • 東恩納 琢偉 +
      +
    • 琉球大学理工学研究科 情報工学専攻
      • +
    +
    • +
+
+
+

研究目的

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

Gears OS

+
    +
  • アプリケーションやサービスの信頼性をOSの機能として保証することを目指している。
    • +
  • 信頼性を保証する手法としてモデル検査を上げている。
    • +
  • GearsOS は軽量継続を基本とする言語 CbC を用いたOSの実装である。
    • +
+
+
+

Continution based C

+
    +
  • CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear　という単位で遷移する。
    • +
  • goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。
    • +
+
__code cg0(int a, int b) { goto cg1(a+b);
+}
+__code cg1(int c) { goto cg2(c);
+ }
+
+
+
+
+

goto

+
    +
  • goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。
    • +
  • goto による遷移は軽量継続と言い、関数呼び出しのような環境変数を持たず、遷移元の処理に囚われず、遷移先を自由に変更する事が可能である。これにより処理の間にメタレベルの計算を挿入する事が可能である。
    • +
  • CbC における遷移記述はそのまま状態遷移記述にすることができる。
    • +
+
+
+
+

dataGear と meta dataGear

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

stub CodeGear

+
    +
  • メタレベルから見ると、code Gearの入力はcontext ただ1つである。
    • +
  • ノーマルレベルからMeta dataGear であるcontext を直接参照してしまう事は、ユーザーがメタレベルに対して自由に記述できてしまう事になる。
    • +
  • この問題を防ぐため context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub CodeGearがある。
    • +
+

---

+

context

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

GearsOSの実装

+
    +
  • codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。
    • +
  • しかし一般的には、他のcodeGearが共有されたdataGearに競合的に書き込んだり、割り込みにより処理が中断したりする。
    • +
  • しかし、GearsOSにおいては正しく実行される事を保証されるように実装されているとする。
    • +
+
+
+

モデル検査

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

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

+
    +
  • 検査の要点によってモデルを使い分ける必要性がある。
    • +
+
+
+

状態遷移モデル

+
    +
  • 今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。
    • +
  • 状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。
    • +
  • 構成要素
    • +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
構成要素
状態プログラムの状態
初期状態何らかの処理、計算が行われる前の状態
終了状態処理、または計算が行われた状態
状態変数プログラムの状態を表す変数
処理(計算)状態を変化させる
遷移条件状態が分岐する際の条件
+
+
+

既存のモデル検査手法(1/2)

+
    +
  • モデル検査ツールとしてSPINと java path finder（JPF)がある
    • +
  • SPIN はPromela (Process Meta Language)で記述される。
    • +
  • C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語である。
    • +
  • C言語で記述された検証機を生成し、コンパイル実行することで検証する。
    • +
  • チャネルを使ってお通信や並列動作する有限オートマトンのモデル検査が可能である。
    • +
  • SPIN では以下の性質を検査可能な性質
    +アサーション
    +デッドロック
    +到達性
    +進行性
    +線形時相論理で記述された仕様
    • +
+
+
+

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

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

タブロー展開

+
    +
  • GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。
    • +
  • タブロー法は生成可能な状態のすべてを生成する手法である。
    • +
  • 生成された状態の組み合わせを深さ優先探索で調べ、木構造で保存する。この時、同じ状態の組み合わせがあれば抽象化し共有することで、状態数が増えすぎる事を抑える。
    • +
+
+
+

notitle

+
    +
  • GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。
    • +
+
+
+

DPP

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

DPP

+
    +
  • 状態は以下のようになる
    +Pickup Right
    +fork Pickup
    +Left fork eating Put Right fork
    +Put Left fork
    +Thinking
    • +
+
+
+
+

GeasOS におけるDPP実装

+
    +
  • 5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。
    • +
  • gearsOSには並列機構の　par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。
    • +
  • フォークの管理をsynchronixed Queue を用いることによってスレッド間での同期を行う。
    • +
  • スレッドの状態遷移に　metaCodeGear を 挟みメタレベルで各スレッドの状態の保存を行う。
    • +
+
+
\ No newline at end of file diff -r 6389876c941a -r 9c8a9f059ddf presen/sigos.md --- a/presen/sigos.md Wed May 27 16:02:50 2020 +0900 +++ b/presen/sigos.md Wed May 27 21:11:34 2020 +0900 @@ -1,43 +1,106 @@ +--- +marp: true +title: Gears OSでモデル検査を実現する手法について +paginate: true +--- + +# Gears OSでモデル検査を実現する手法について +- 東恩納 琢偉 + - 琉球大学理工学研究科 情報工学専攻 +--- # 研究目的 + - OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る - 本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、モデル検査による保証について考察する - GearsOS そのものをGearsOS上でモデル検査することに関しても考察する。 +--- # Gears OS + - アプリケーションやサービスの信頼性をOSの機能として保証することを目指している。 - 信頼性を保証する手法としてモデル検査を上げている。 - GearsOS は軽量継続を基本とする言語 CbC を用いたOSの実装である。 +--- + # Continution based C + - CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear　という単位で遷移する。 - goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。 -
-　normalCodeGear -
+``` +__code cg0(int a, int b) { goto cg1(a+b); +} +__code cg1(int c) { goto cg2(c); + } + +``` + +--- + +# goto + +- goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。 +- goto による遷移は軽量継続と言い、関数呼び出しのような環境変数を持たず、遷移元の処理に囚われず、遷移先を自由に変更する事が可能である。これにより処理の間にメタレベルの計算を挿入する事が可能である。 +- CbC における遷移記述はそのまま状態遷移記述にすることができる。 + + +
+ +--- # dataGear と meta dataGear + - CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル とメタレベルがある。 - メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearを格納するcontext などがある。context は一般的なOSのプロセスに相当する。 -# goto -- goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。 -- goto による遷移は軽量継続と言い、関数呼び出しのような環境変数を持たず、遷移元の処理に囚われず、遷移先を自由に変更する事が可能である。これにより処理の間にメタレベルの計算を挿入する事が可能である。 -- CbC における遷移記述はそのまま状態遷移記述にすることができる。 +--- + +# stub CodeGear + +- メタレベルから見ると、code Gearの入力はcontext ただ1つである。 +- ノーマルレベルからMeta dataGear であるcontext を直接参照してしまう事は、ユーザーがメタレベルに対して自由に記述できてしまう事になる。 +- この問題を防ぐため context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub CodeGearがある。 + +---　 + +# cotntextと状態数 + +- プログラムの非決定的な実行は入力あるいは並列実行の非決定性から生じる。 +- 並列実行における非決定性は、同時に実行される codeGear　の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。 +- しかし、このcontextの状態はとても巨大になる事がある、そのためそれらを抽象化する必要性がある。 + + + + +--- + +# GearsOSの実装 + +- codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。 +- しかし一般的には、他のcodeGearが共有されたdataGearに競合的に書き込んだり、割り込みにより処理が中断したりする。 +- しかし、GearsOSにおいては正しく実行される事を保証されるように実装されているとする。 + + +--- # モデル検査 + - モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。 - このモデルが仕様を満たしているかどうかを検査するものである。 -* 状態遷移モデル -* 論理モデル -* 組み合わせモデル -* フローモデル ..etc + 状態遷移モデル + 論理モデル + 組み合わせモデル + フローモデル ..etc - 検査の要点によってモデルを使い分ける必要性がある。 +--- + # 状態遷移モデル + - 今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。 - 状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。 - 構成要素 @@ -51,48 +114,74 @@ | 処理(計算) |状態を変化させる | | 遷移条件 |状態が分岐する際の条件 | -# 既存のモデル検査手法 +--- + +# 既存のモデル検査手法(1/2) + - モデル検査ツールとしてSPINと java path finder（JPF)がある - SPIN はPromela (Process Meta Language)で記述される。 +- C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語である。 - C言語で記述された検証機を生成し、コンパイル実行することで検証する。 +- チャネルを使ってお通信や並列動作する有限オートマトンのモデル検査が可能である。 +- SPIN では以下の性質を検査可能な性質 + アサーション + デッドロック + 到達性 + 進行性 + 線形時相論理で記述された仕様 - SPIN では以下の性質を検査可能な性質 -* アサーション -* デッドロック -* 到達性 -* 進行性 -* 線形時相論理で記述された仕様 +--- + +# 既存のモデル検査手法(2/2) - Java Path Finder はjavaプログラムの検査ツール +- java バーチャルマシン(JVM) を直接シュミレーション実行している、これによりjavaのバイトコードを直接実行可能である。 +- バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査している。 +- 実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して実行する必要がある。 - JPF では以下の性質を検査することができる -* スレッドの可能な実行すべてを調べる -* デッドロックの検出 -* アサーション -* Partial Order Reduction + スレッドの可能な実行すべてを調べる + デッドロックの検出 + アサーション + Partial Order Reduction -# タブロー展開と状態数の抽象化 +--- + +# タブロー展開 + - GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。 - タブロー法は生成可能な状態のすべてを生成する手法である。 - 生成された状態の組み合わせを深さ優先探索で調べ、木構造で保存する。この時、同じ状態の組み合わせがあれば抽象化し共有することで、状態数が増えすぎる事を抑える。 -# +--- + +# + - GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。 +--- # DPP -- 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。 + +- 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 -
-　dpp -
+
+ +--- # GeasOS におけるDPP実装 + - 5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。 - gearsOSには並列機構の　par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。 - フォークの管理をsynchronixed Queue を用いることによってスレッド間での同期を行う。