Binary file paper/ikkun-sigos.pdf has changed

--- a/paper/ikkun-sigos.tex	Thu May 07 22:00:44 2020 +0900
+++ b/paper/ikkun-sigos.tex	Thu May 07 22:42:40 2020 +0900
@@ -247,10 +247,12 @@
 
 タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。
 
- \section{GearsOSを用いたモデル検査} 
+\section{GearsOSを用いたモデル検査} 
 DPP は哲学者5人が同時に行動するので、5つのスレッドで同時に処理することで状態を生成する事ができる。まず Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\verb+__exit+を渡す。par goto で生成された Task は\verb|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能である。
-また Gears OS には　Synchronized Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue があり、これを使い5つのフォークの状態を管理する。
-Syncrhonized Queueは CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う命令である。CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータ今日がないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗し、もう一度 CAS を行う。
+%また Gears OS には　Synchronied Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue があり、これを使い5つのフォークの状態を管理する。
+%Syncrhonized Queueは CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う命令である。
+5つのフォークの状態はCASで管理する。
+CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータがないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗し、もう一度 CAS を行う。
 5スレッドで行われる処理の状態は以下の6通りで、think のあとPickup Right fork に戻ってくる。
 \begin{itemize}
 \item Pickup Right fork
@@ -260,7 +262,9 @@
 \item Put Left fork
 \item Thinking
 \end{itemize}
-この状態は goto next によって遷移する。またこの状態遷移は無限ループするのでMemoryTree に保管し、保管されている状態とはstat DB によって保管される
+この状態は goto next によって遷移する。この時に次に動作するのは5人のうちのどれでも良い。
+この状態遷移を深さ優先探索すると無限ループするが、同じ状態かどうかを Memort Tree と State DB により判定する。
+同じ状態であれば、深さ優先探索の一つ前の iterator に戻る。
 
 \begin{figure}[tb]
     \begin{center}
@@ -270,7 +274,42 @@
     \label{DPP_chacking}
 \end{figure}
 
+この実行は Single thread に行われるが、interator を使って並行実行しても良い。
 
+必要な時相論理的な仕様は codeGear にコンパイルすることができるので、それを同時に走らせることによりチェックできる。
+これは SPIN の LTL の仕様記述と同じことになる。このようにモデル検査を codeGear と dataGear 上に実現することができる。
+
+
+メモリ領域の登録には
+\verb+add_mamory_area(ContextPtr cbc_contex+ \verb+,void *addrss,long length)+ のようなAPIを用いる。
+状態の格納は、mera codeGear で行われるので、customize が可能である。この段階で対称性の利用や状態の抽象化を行うことができる。
+
+\section{OS自体のモデル検査}
+
+Gears OS 自体も codeGear/dataGear で書かれているので、この枠組みの中で検証することが可能であると思われる。
+しかし、いくつかの問題がある。
+
+OSの場合はほとんどがmeta levelの記述なので、それを emulation する必要がある。メモリやCPUは問題ないが TLB などは工夫が必要になる。
+CPUの状態、例えばキャッシュなども emulation する場合には、codeGear の大きさをメモリアクセスレベルまで小さくする必要がある。
+つまり、見つけたいバグを知っていれば検証は可能だが、起きる可能性のある未知のメタ計算に関しては何も教えてくれない。
+
+モデル検査は膨大な状態空間を探索する必要があり、OS込みのモデル検査となると厳しいと予想される。
+しかし、OS特定部分を調べるのに巨大なアプリケーションは必要ないと思われる。普通のテストの代わりにモデル検査を使うような感じになる。
+
+OSを含むモデル検査はデバイスドライバの開発などに向いていると考えられる。この場合は、デバイス自体の仕様が codeGear/dataGear
+で書かれている必要がある。
+
+Gears OS は Unix 上のApplicationとして実現されているものと、x.v6 の書き換えとして実現するものとの二種類がある。
+後者の開発にモデル検査が使えると良い。
+
+\section{まとめ}
+
+Gears OS でのモデル検査の実装方法について考察した。DPPの検証自体は前に書かれたことがある\cite{}。
+この時のmemory tree と state DB を使うことも可能だが、これ自体はCで書かれている。
+これも codeGear で書く方が望ましい。
+
+
+まず、DPPを動かすとこから始めて、OS自体を検証する方向に研究を進めていきたい。
 
 
 \nocite{*}