# 研究目的

• 一般的にアプリケーションはテストと言われる方法を用いてバグを発見し修正することで信頼性を高める、しかしバグの再現性が低い場合には発見は困難になる。この際にはデバックを行うプログラマーの経験による予測が必要であり、予想した原因に基づいて１つ１つチェックをしていく必要がある。
• モデル検査とは、検証したいアプリケーションの状態遷移記述を用いて行われ、特定の状態から遷移する全ての組み合わせに対して検査を行うことで、信頼性を保証する。
• 当研究室で開発しているGearsOSはアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、モデル検査による検証や、定理証明を用いる事での信頼性へのアプローチを行っています。
• 本研究ではGearsOSにおけるDPPのモデル検査を行うことでGearsOSにおけるモデル検査手法の確立と、さらにGearsOS上での自身のモデル検査について研究する。

# 実装の全体像

• モデル検査を行うための例題としてのDPPを扱う。DPPは並列で動きつつ、スレッド間でデータのやり取りを行う。このためデッドロックが起こる。今回の研究ではこのデッドロックをモデル検査で検出する。
• スレッド間でのデータのやり取りはCASを用いているSynchronizedQueueでデータの保証を行う。
• モデル検査を行うために、DPPを動かしつつstatmantDBとmemoryTreeによってログを保存する。

# コメント

interface を通してぐるぐる回るようにしないといけない

dpp_common.h でアクション_next はいらない

phils はリソース？

goto meta を読んでる部分で、順々によんでやるやつにすればいい

cpu worker を持ってる、それぞれcontextのリストを持っているので、その分だけスレッドを投げてやる cpuworkerは本来複数いて、 実行可能な複数のqueueのうちどれかを動かしてやる。

スレッドはcpuの数をこえるので、こえた分どうにかしないといけない。 スレッドプールに投げるけど、そのあとgotometaで切り替えてやらないといけない。 taskは赤黒きにぶっこんでたような par goto もCPUの数以上に投げると、終了を待ってしまうので、それだといけない セリウムだと、もっとベクトライズされていたのでタスクが小さい想定だった。 Gearsの場合は自分でタスクを小さくする想定、しかしphiloは終わらないので、自分でgotometaでタスクマネージャーに戻るかを選択しないといけない。これはメタ側に書かれるもの。

C++？？ cpuwokerのモデルチェッキングと、それようのgoto metaの作成

synchonizedqueue はシングルワーカーだと動かない。 モデルチェッキングワーカーが持ってる複数スレッドの中でエミュレートしないといけない。 chack and set

Atomic で　chack and setq　は書かれている。 こいつはcpuwokerからは特別扱いされないと行けない。こいつが来たときに優先できるように。

今はコンストラクタをファンクションコールにしているけど。それを~するとTaskManagerの方も簡単になりそう

第２フィロソファーをそのまま動かしたい。 第二フィロソファーは清水君のやってる新しい感じで書く必要がある。