Binary file paper/ikkun-sigos.pdf has changed

--- a/paper/ikkun-sigos.tex	Sat May 02 04:55:50 2020 +0900
+++ b/paper/ikkun-sigos.tex	Mon May 04 03:34:12 2020 +0900
@@ -64,14 +64,46 @@
 
 %1
 \section{プログラムの信頼性}
-リアルタイムプログラムや並列プログラムのような非決定生を含むプログラムは、逐次型のプログラムに有効な二分法などによるうデバック手法ではデバックする事が困難である。そのため、非決定生を含むプログラムに対して有効なデバック手法や検証手法の確立が重要な課題となっている。本研究ではモデル検査を用いる事でプログラムの信頼性を保証する手法として、GearsOSにおけるモデル検査手法について提案する。
+ 現在、CPUの処理性能はクロック数の向上は電力消費の増大の問題から伸び悩んでおり、マルチコアCPUやGPUを利用した並列化処理を行うことによって処理速度の向上を図る事が多く、また画像処理や機械学習の分野では並列化処理は重要な役割を果たしている。しかし処理を並列化する場合、個々のプログラムが正しく動作する事が証明されていてもそれらを並列に実行したとき、全体の動作の正しさは保証されない。これは並列化されたプログラムの非決定性によるものである。また非決定性を含むプログラムは、逐次型のプログラムに有効な二分法などによるうデバック手法ではデバックする事が困難である。そのため、非決定生を含むプログラムに対して有効なデバック手法や検証手法の確立が重要な課題となっている。本研究ではモデル検査を用いる事でプログラムの信頼性を保証する手法として、GearsOSにおけるモデル検査手法について提案する。\\
 モデル検査はプログラムの設計から導出されたモデルが形式仕様を満たすかを検証することで信頼性を保証する、しかしプログラムの規模が大きくなると導出されるモデルの状態数が爆発的に増えるため、それら全てを検証する手法は好ましくない、そのため記録する状態を抽象化、または限定する方法について考察する。
 
+\section{モデル検査手法}
+ モデル検査にはタブロー法という手法が用いられる。タブロー法は様相論理式の恒真性を検証する定理証明アルゴリズムで、プログラムの大域的な状態の全てを生成する手法である。反例を探す場合は反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての大域的な状態を生成する必要がある。大域的な状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数状の計算量がかかる。この展開の際に仕様うも同時に展開することでプログラムに対する仕様の検証を行う事が可能である。\\
+
+ タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。タブロー法に沿って状態を展開する事をタブロー展開といい、 SPIN と java path finder(以下JVM)というツールがある。\\
+　SPIN は PROMELA という仕様記述言語で記述する事でC言語の検証器を生成する事で、コンパイルまたは実行時に検証する事ができる。チェネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。\\
+SPIN では以下の性質を検査する事ができる。
+\begin{itemize}
+\item アサーション
+\item デッドロック
+\item 到達生
+\item 進行性
+\item 線形時相論理で記述された仕様
+\end{itemize}
+ Java Path Finder(JPF) は java プログラムに対するモデル検査ツールで、javaバーチャルマシン(JVM)を直接シミュレーションして実行している。そのため、javaのバイトコードを直接実行可能である。バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査する。バイトコードの実行パターンを網羅的に調べるために、膨大なCPU時間を必要とする。またJVMヘースであるため、複数のプロセスの取り扱いが出来ず、状態空間が巨大になる場合は直接実行は出来ず、一部を抜き出してデバックをするのに使用される。\\
+JPF では以下の事ができる。
+\begin{itemize}
+\item スレッドの可能な実行全てを調べる
+\item デッドロックの検出
+\item アサーション
+\item Partial Order Reduction
+\end{itemize}
+
+
+
+\section{DPP}
+ 検証用のサンプルプログラムとしてDining Philosohers Ploblem を用いる。これは資源共有問題の１つで、次のような内容である。
+ 5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。食べるには2本のフォークを使わないと食べれないが、フォークは円卓に5本しかなく、また各々の間に一本ずつ置かれている。哲学者は思索と食事を交互に繰り返そうとし、食事するにはフォークを2本取る必要があるが取れなかった場合はフォークが空くのを待つ。
+ 各哲学者を１つのプロセスとすると、この問題は後このプロセスが並列に動くことになる。
+
 \section{Gears OS}
-モデル検査はプログラムの状態記述を線形時相論理の論理式の形式で記述し検証する手法が一般的である。
-本研究室で開発しているGeasOS は CbC で記述されており、プログラムの処理が記述された code gear と変数などのデータを格納する data gear によって構成され、Code Gear 間の遷移にはgoto を用いて遷移する。このため CbC による記述は状態遷移記述になる性質がある。
+ 本研究室で開発しているGeasOS は CbC で記述されており、プログラムの処理が記述された code gear と変数などのデータを格納する data gear によって構成され、Code Gear 間の遷移にはgoto を用いて遷移する。このため CbC による記述は状態遷移記述になる性質がある。
 また goto による遷移は大域変数を持たない遷移であるため、遷移前の処理に囚われず遷移先を自由に変更する事が可能である。
-Gears OS はこの性質を利用して処理の間に meta Code Gear を入れることでメタ計算を途中で行う事ができる。
+Gears OS はこの性質を利用して処理の間にメタレベルの計算である meta Code Gear またmeta Code Gear を入れることができる　
+　メタ計算である meta Code Gear、meta Data Gaer と対比して、Coed Gear、Data Gaer をインターフェースといい、OSとしての重要な
+
+ \seciton{GearsOSを用いたモデル検査}
+