--- a/presen/sigos.md	Wed May 27 21:42:42 2020 +0900
+++ b/presen/sigos.md	Thu May 28 01:31:29 2020 +0900
@@ -11,16 +11,16 @@
 
 # 研究目的
 
-- OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る
-- 本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、モデル検査による保証について考察する
-- GearsOS そのものをGearsOS上でモデル検査することに関しても考察する。
+- OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る。
+- 本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、今回はモデル検査による信頼性の保証について考察する。
+- またGearsOS そのものをGearsOS上でモデル検査することに関しても考察する。
 ---
 
 # Gears OS
 
-- アプリケーションやサービスの信頼性をOSの機能として保証することを目指している。
-- 信頼性を保証する手法としてモデル検査を上げている。
-- GearsOS は軽量継続を基本とする言語 CbC を用いたOSの実装である。
+- 軽量継続を基本とする言語 Contnution based C を用いて記述されている。
+- アプリケーションやサービスの信頼性をOSの機能として保証することを目指しています。
+- 信頼性を保証する方法としてモデル検査による検証や、定理証明を用いる事で、信頼性へのアプローチを行っています。
 
 ---
 
@@ -28,13 +28,18 @@
 
 - CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear　という単位で遷移する。
 - goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。
-
+- 以下は CbC によって記述された codeGear です。
 ```
-__code cg0(int a, int b) { goto cg1(a+b);
+code pickup_lfork(PhilsPtr self, TaskPtr current_task)
+{
+    if (self->left_fork->owner == NULL) {
+        self->left_fork->owner = self;
+        self->next = pickup_rfork;
+        goto scheduler(self, current_task);
+    } else {
+        self->next = hungry1;
+        goto scheduler(self, current_task);
 }
-__code cg1(int c) { goto cg2(c);
- }
-
 ```
 
 ---
@@ -64,17 +69,27 @@
 - ノーマルレベルからMeta dataGear であるcontext を直接参照してしまう事は、ユーザーがメタレベルに対して自由に記述できてしまう事になる。
 - この問題を防ぐため context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub CodeGearがある。
 
----　
+```
+__code clearSingleLinkedStack(struct Context *context,struct SingleLinkedStack* stack,enum Code next) {
+    stack->top = NULL;
+    goto meta(context, next);
+}
+
+__code clearSingleLinkedStack_stub(struct Context* context) {
+    SingleLinkedStack* stack = (SingleLinkedStack*)GearImpl(context, Stack, stack);
+    enum Code next = Gearef(context, Stack)->next;
+    goto clearSingleLinkedStack(context, stack, next);
+} 
+```
+
+---
 
 # cotntextと状態数
 
-- プログラムの非決定的な実行は入力あるいは並列実行の非決定性から生じる。
-- 並列実行における非決定性は、同時に実行される codeGear　の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。
+- プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。
+- 並列実行の非決定性は、同時に実行される codeGear の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。
 - しかし、このcontextの状態はとても巨大になる事がある、そのためそれらを抽象化する必要性がある。
 
-
-
-
 ---
 
 # GearsOSの実装
@@ -103,26 +118,24 @@
 
 - 今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。
 - 状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。
-- 構成要素
+- 構成要素としては以下のような物がある。
 
-|構成要素    |					  |
 | ---------- | ---------------------------------  |
-| 状態       |　プログラムの状態		  |
+| 状態       | プログラムの状態	 		  |
 |  初期状態  |何らかの処理、計算が行われる前の状態|
 |  終了状態  |処理、または計算が行われた状態	  |
-|  状態変数  |プログラムの状態を表す変数	  |
 | 処理(計算) |状態を変化させる			  |
 | 遷移条件   |状態が分岐する際の条件		  |
 
 ---
 
-# 既存のモデル検査手法(1/2)
+# 既存のモデル検査手法(SPIN)
 
-- モデル検査ツールとしてSPINと java path finder（JPF)がある
 - SPIN はPromela (Process Meta Language)で記述される。
-- C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語である。
-- C言語で記述された検証機を生成し、コンパイル実行することで検証する。
-- チャネルを使ってお通信や並列動作する有限オートマトンのモデル検査が可能である。
+- C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語であり、検証機を生成し、コンパイルと実行を行うことで検証される。
+- チャネルを使って通信や並列動作を記述する
+- 有限オートマトンに変換してモデル検査を行う。
+- Promelaへの書き換えが必要
 - SPIN では以下の性質を検査可能な性質
  アサーション
  デッドロック
@@ -132,7 +145,7 @@
 
 ---
 
-# 既存のモデル検査手法(2/2)
+# 既存のモデル検査手法(Java path Finder)
 
 - Java Path Finder はjavaプログラムの検査ツール
 - java バーチャルマシン(JVM) を直接シュミレーション実行している、これによりjavaのバイトコードを直接実行可能である。
@@ -146,11 +159,14 @@
 
 ---
 
-# タブロー展開
-
-- GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。
-- タブロー法は生成可能な状態のすべてを生成する手法である。
-- 生成された状態の組み合わせを深さ優先探索で調べ、木構造で保存する。この時、同じ状態の組み合わせがあれば抽象化し共有することで、状態数が増えすぎる事を抑える。
+# 
+- GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。
+- codegear 実行後の状態を検査し、データベースに格納する。
+- 新しい上体が生成されなくなった時モデル検査が終了する。
+- 哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。
+- 必要な状態はフォークの状態だけになるので、それ以外の状態は無視することができる。
+- これにより状態数を下げることができる。
+- つまり、問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。
 - GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。
 
 ---
@@ -159,20 +175,20 @@
 
 - 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。
 - フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。
-<center><img src="./pic/dpp_image.svg" alt="" width="50%" height="50%" ></center>
+<center><img src="./pic/dpp_image.svg" alt="" width="55%" height="55%" ></center>
 
 ---
 
 # DPP
 
-- 状態は以下のようになる
+- 状態は以下の構成要素からなる
 Pickup Right
 fork Pickup
 Left fork eating Put Right fork
  Put Left fork
  Thinking
 
-<center><img src="./pic/dpp_image.svg" alt="" width="50%" height="50%" ></center>
+<right><img src="./pic/dpp_image.svg" alt="" width="50%" height="50%" ></right>
 
 ---
 
@@ -180,7 +196,7 @@
 # GeasOS におけるDPP実装(1/3)
 
 - 5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。
-- gearsOSには並列機構の　par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。
+- gearsOSには並列機構の par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。
 - par goto は引数として dataGear と実行後に継続する _exit をわたす。
 - par goto は複数スレッドでの実行であるので、各スレッドで実行後に__exitに継続する事で終了する。
 
@@ -188,8 +204,8 @@
 
 # GearsOS におけるDPP実装(2/3)
 
-- マルチスレッドでのデータの一貫性を保証するのにSyncrhonized queue がある。
-- Syncrhonized queue はCAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う。
+- マルチスレッドでのデータの一貫性を保証する手法としてCAS がある。
+- CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う。
 - CAS は書き込みの際に、書き込む MetaCodeGear に更新前と更新後の値を渡し、更新前の値が保存されているメモリ番地の値と比較し同じデータがであれば書き込みを行う。異なる場合はほかからの書き込みがあったとみなし、値の更新に失敗し、もう一度CASを行う。
 - DPPの例題ではフォークがスレッドで共有されるデータにあたるので、synchronixed Queue を用いることによってスレッド間での同期を行う。
 
@@ -203,10 +219,12 @@
 
 ---
 
-# まとめ
+# GearsOS でのモデル検査を実現する手法について
+- DPP をGearsOS 上のアプリケーションとして実装する。
+- DPP codeGear のシャッフルの１つとして実行する。
+- 可能な実行を生成するiterator を作成する
+- 状態を記録するmemory Tree とstateDBを作成する。
 
 
 
 
-
-