Binary file .DS_Store has changed

Binary file paper/GearsOS-modelchecking.pdf has changed

Binary file paper/ikkun-sigos.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/codegear-goto	Wed May 27 16:02:50 2020 +0900
@@ -0,0 +1,7 @@
+ __code cg0(int a, int b) {
+     goto cg1(a+b);
+ }
+ 
+ __code cg1(int c) {
+     goto cg2(c);
+   }
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presen/pic/dpp_image.bb	Wed May 27 16:02:50 2020 +0900
@@ -0,0 +1,5 @@
+%%Title: ./dpp_image.pdf
+%%Creator: ebb Version 0.5.2
+%%BoundingBox: 0 0 626 475
+%%CreationDate: Tue Feb 12 04:12:11 2008
+

Binary file presen/pic/dpp_image.pdf has changed

Binary file presen/pic/input-outputDataSegment.pdf has changed

Binary file presen/pic/meta_gear.pdf has changed

Binary file presen/pic/model_checking.odg has changed

Binary file presen/pic/model_checking.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presen/sigos.md	Wed May 27 16:02:50 2020 +0900
@@ -0,0 +1,99 @@
+
+# 研究目的
+- OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る
+- 本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、モデル検査による保証について考察する
+- GearsOS そのものをGearsOS上でモデル検査することに関しても考察する。
+
+# Gears OS
+- アプリケーションやサービスの信頼性をOSの機能として保証することを目指している。
+- 信頼性を保証する手法としてモデル検査を上げている。
+- GearsOS は軽量継続を基本とする言語 CbC を用いたOSの実装である。
+
+# Continution based C
+- CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear　という単位で遷移する。
+- goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。
+
+<div style="text-align: center;">
+　<img src="../paper/pic/meta_gear.pdf" alt="normalCodeGear" width="600">
+</div>
+
+# dataGear と meta dataGear
+- CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル
+とメタレベルがある。
+- メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearを格納するcontext などがある。context は一般的なOSのプロセスに相当する。
+
+# goto
+- goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。
+- goto による遷移は軽量継続と言い、関数呼び出しのような環境変数を持たず、遷移元の処理に囚われず、遷移先を自由に変更する事が可能である。これにより処理の間にメタレベルの計算を挿入する事が可能である。
+- CbC における遷移記述はそのまま状態遷移記述にすることができる。
+
+# モデル検査
+- モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。
+- このモデルが仕様を満たしているかどうかを検査するものである。
+
+* 状態遷移モデル
+* 論理モデル
+* 組み合わせモデル
+* フローモデル ..etc
+- 検査の要点によってモデルを使い分ける必要性がある。
+
+# 状態遷移モデル
+- 今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。
+- 状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。
+- 構成要素
+
+|構成要素    |					  |
+| ---------- | ---------------------------------  |
+| 状態       |　プログラムの状態		  |
+|  初期状態  |何らかの処理、計算が行われる前の状態|
+|  終了状態  |処理、または計算が行われた状態	  |
+|  状態変数  |プログラムの状態を表す変数	  |
+| 処理(計算) |状態を変化させる			  |
+| 遷移条件   |状態が分岐する際の条件		  |
+
+# 既存のモデル検査手法
+- モデル検査ツールとしてSPINと java path finder（JPF)がある
+- SPIN はPromela (Process Meta Language)で記述される。
+- C言語で記述された検証機を生成し、コンパイル実行することで検証する。
+
+ SPIN では以下の性質を検査可能な性質
+* アサーション
+* デッドロック
+* 到達性
+* 進行性
+* 線形時相論理で記述された仕様
+
+- Java Path Finder はjavaプログラムの検査ツール
+- JPF では以下の性質を検査することができる
+* スレッドの可能な実行すべてを調べる
+* デッドロックの検出
+* アサーション
+* Partial Order Reduction
+
+# タブロー展開と状態数の抽象化
+- GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。
+- タブロー法は生成可能な状態のすべてを生成する手法である。
+- 生成された状態の組み合わせを深さ優先探索で調べ、木構造で保存する。この時、同じ状態の組み合わせがあれば抽象化し共有することで、状態数が増えすぎる事を抑える。
+# 
+- GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。
+
+
+# DPP
+- 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。
+- 状態は以下のようになる
+* Pickup Right fork
+* Pickup Left fork
+* eating
+* Put Right fork
+* Put Left fork
+* Thinking
+
+<div style="text-align: center;">
+　<img src="./pic/dpp_image.pdf " alt="dpp" width="600">
+</div>
+
+# GeasOS におけるDPP実装
+- 5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。
+- gearsOSには並列機構の　par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。
+- フォークの管理をsynchronixed Queue を用いることによってスレッド間での同期を行う。
+- スレッドの状態遷移に　metaCodeGear を 挟みメタレベルで各スレッドの状態の保存を行う。