Mercurial > hg > Papers > 2020 > ikkun-sigos

Binary file paper/ikkun-sigos.pdf has changed
--- a/presen/sigos.html	Wed May 27 21:42:42 2020 +0900
+++ b/presen/sigos.html	Thu May 28 01:31:29 2020 +0900
@@ -12,7 +12,7 @@

 /* @theme example */div#p>svg>foreignObject>section{background-image:url("assets/logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto}

-/* @theme 1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="1" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+/* @theme vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="1" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1><svg data-marp-fitting="svg"><foreignObject><span data-marp-fitting-svg-content> Gears OSでモデル検査を実現する手法について</span></foreignObject></svg></h1>
 <ul>
 <li>東恩納 琢偉
@@ -22,36 +22,42 @@
 </li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="2" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="2" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>研究目的</h1>
 <ul>
-<li>OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る</li>
-<li>本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、モデル検査による保証について考察する</li>
-<li>GearsOS そのものをGearsOS上でモデル検査することに関しても考察する。</li>
+<li>OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る。</li>
+<li>本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、今回はモデル検査による信頼性の保証について考察する。</li>
+<li>またGearsOS そのものをGearsOS上でモデル検査することに関しても考察する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="3" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="3" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>Gears OS</h1>
 <ul>
-<li>アプリケーションやサービスの信頼性をOSの機能として保証することを目指している。</li>
-<li>信頼性を保証する手法としてモデル検査を上げている。</li>
-<li>GearsOS は軽量継続を基本とする言語 CbC を用いたOSの実装である。</li>
+<li>軽量継続を基本とする言語 Contnution based C を用いて記述されている。</li>
+<li>アプリケーションやサービスの信頼性をOSの機能として保証することを目指しています。</li>
+<li>信頼性を保証する方法としてモデル検査による検証や、定理証明を用いる事で、信頼性へのアプローチを行っています。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="4" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="4" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>Continution based C</h1>
 <ul>
 <li>CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear　という単位で遷移する。</li>
 <li>goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。</li>
+<li>以下は CbC によって記述された codeGear です。</li>
 </ul>
-<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>__code c<span class="hljs-name">g0</span><span class="hljs-comment">(int a, int b)</span> { <span class="hljs-keyword">goto</span> c<span class="hljs-name">g1</span><span class="hljs-comment">(a+b)</span>;
+<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>code pickup_lfork(PhilsPtr <span class="hljs-keyword">self</span>, TaskPtr current_task)
+{
+    <span class="hljs-keyword">if</span> (<span class="hljs-keyword">self</span>-&gt;left_fork-&gt;owner == <span class="hljs-keyword">NULL</span>) {
+        <span class="hljs-keyword">self</span>-&gt;left_fork-&gt;owner = <span class="hljs-keyword">self</span>;
+        <span class="hljs-keyword">self</span>-&gt;next = pickup_rfork;
+        <span class="hljs-keyword">goto</span> scheduler(<span class="hljs-keyword">self</span>, current_task);
+    } <span class="hljs-keyword">else</span> {
+        <span class="hljs-keyword">self</span>-&gt;next = hungry1;
+        <span class="hljs-keyword">goto</span> scheduler(<span class="hljs-keyword">self</span>, current_task);
 }
-__code c<span class="hljs-name">g1</span><span class="hljs-comment">(int c)</span> { <span class="hljs-keyword">goto</span> c<span class="hljs-name">g2</span><span class="hljs-comment">(c)</span>;
- }
-
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="5" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="5" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>goto</h1>
 <ul>
 <li>goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。</li>
@@ -60,7 +66,7 @@
 </ul>
 <center><img src="./pic/input-outputDataSegment.svg" alt="" width="100%" height="100%" /></center>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="6" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="6" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>dataGear と meta dataGear</h1>
 <ul>
 <li>CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル<br />
@@ -68,22 +74,34 @@
 <li>メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearを格納するcontext などがある。context は一般的なOSのプロセスに相当する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="7" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="7" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>stub CodeGear</h1>
 <ul>
 <li>メタレベルから見ると、code Gearの入力はcontext ただ1つである。</li>
 <li>ノーマルレベルからMeta dataGear であるcontext を直接参照してしまう事は、ユーザーがメタレベルに対して自由に記述できてしまう事になる。</li>
 <li>この問題を防ぐため context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub CodeGearがある。</li>
 </ul>
-<p>---</p>
+<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>__code clear<span class="hljs-constructor">SingleLinkedStack(<span class="hljs-params">struct</span> Context <span class="hljs-operator">*</span><span class="hljs-params">context</span>,<span class="hljs-params">struct</span> SingleLinkedStack<span class="hljs-operator">*</span> <span class="hljs-params">stack</span>,<span class="hljs-params">enum</span> Code <span class="hljs-params">next</span>)</span> {
+    stack-&gt;top = NULL;
+    goto meta(context, next);
+}
+
+__code clear<span class="hljs-constructor">SingleLinkedStack_stub(<span class="hljs-params">struct</span> Context<span class="hljs-operator">*</span> <span class="hljs-params">context</span>)</span> {
+    SingleLinkedStack* stack = (SingleLinkedStack*)<span class="hljs-constructor">GearImpl(<span class="hljs-params">context</span>, Stack, <span class="hljs-params">stack</span>)</span>;
+    enum Code next = <span class="hljs-constructor">Gearef(<span class="hljs-params">context</span>, Stack)</span>-&gt;next;
+    goto clear<span class="hljs-constructor">SingleLinkedStack(<span class="hljs-params">context</span>, <span class="hljs-params">stack</span>, <span class="hljs-params">next</span>)</span>;
+}
+</span></span></foreignObject></svg></code></pre>
+</section>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="8" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>cotntextと状態数</h1>
 <ul>
-<li>プログラムの非決定的な実行は入力あるいは並列実行の非決定性から生じる。</li>
-<li>並列実行における非決定性は、同時に実行される codeGear　の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。</li>
+<li>プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。</li>
+<li>並列実行の非決定性は、同時に実行される codeGear の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。</li>
 <li>しかし、このcontextの状態はとても巨大になる事がある、そのためそれらを抽象化する必要性がある。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="8" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="9" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>GearsOSの実装</h1>
 <ul>
 <li>codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。</li>
@@ -91,7 +109,7 @@
 <li>しかし、GearsOSにおいては正しく実行される事を保証されるように実装されているとする。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="9" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="10" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>モデル検査</h1>
 <ul>
 <li>モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。</li>
@@ -105,56 +123,28 @@
 <li>検査の要点によってモデルを使い分ける必要性がある。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="10" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="11" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>状態遷移モデル</h1>
 <ul>
 <li>今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。</li>
 <li>状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。</li>
-<li>構成要素</li>
+<li>構成要素としては以下のような物がある。</li>
 </ul>
-<table>
-<thead>
-<tr>
-<th>構成要素</th>
-<th></th>
-</tr>
-</thead>
-<tbody>
-<tr>
-<td>状態</td>
-<td>プログラムの状態</td>
-</tr>
-<tr>
-<td>初期状態</td>
-<td>何らかの処理、計算が行われる前の状態</td>
-</tr>
-<tr>
-<td>終了状態</td>
-<td>処理、または計算が行われた状態</td>
-</tr>
-<tr>
-<td>状態変数</td>
-<td>プログラムの状態を表す変数</td>
-</tr>
-<tr>
-<td>処理(計算)</td>
-<td>状態を変化させる</td>
-</tr>
-<tr>
-<td>遷移条件</td>
-<td>状態が分岐する際の条件</td>
-</tr>
-</tbody>
-</table>
+<p>| ---------- | ---------------------------------  |<br />
+| 状態       | プログラムの状態	 		  |<br />
+|  初期状態  |何らかの処理、計算が行われる前の状態|<br />
+|  終了状態  |処理、または計算が行われた状態	  |<br />
+| 処理(計算) |状態を変化させる			  |<br />
+| 遷移条件   |状態が分岐する際の条件		  |</p>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="11" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
-<h1>既存のモデル検査手法(1/2)</h1>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="12" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
+<h1>既存のモデル検査手法(SPIN)</h1>
 <ul>
-<li>モデル検査ツールとしてSPINと java path finder（JPF)がある</li>
 <li>SPIN はPromela (Process Meta Language)で記述される。</li>
-<li>C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語である。</li>
-<li>C言語で記述された検証機を生成し、コンパイル実行することで検証する。</li>
-<li>チャネルを使ってお通信や並列動作する有限オートマトンのモデル検査が可能である。</li>
+<li>C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語であり、検証機を生成し、コンパイルと実行を行うことで検証される。</li>
+<li>チャネルを使って通信や並列動作を記述する</li>
+<li>有限オートマトンに変換してモデル検査を行う。</li>
+<li>Promelaへの書き換えが必要</li>
 <li>SPIN では以下の性質を検査可能な性質<br />
 アサーション<br />
 デッドロック<br />
@@ -163,8 +153,8 @@
 線形時相論理で記述された仕様</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="12" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
-<h1>既存のモデル検査手法(2/2)</h1>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="13" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
+<h1>既存のモデル検査手法(Java path Finder)</h1>
 <ul>
 <li>Java Path Finder はjavaプログラムの検査ツール</li>
 <li>java バーチャルマシン(JVM) を直接シュミレーション実行している、これによりjavaのバイトコードを直接実行可能である。</li>
@@ -177,54 +167,58 @@
 Partial Order Reduction</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="13" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
-<h1>タブロー展開</h1>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="14" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
+<h1></h1>
 <ul>
-<li>GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。</li>
-<li>タブロー法は生成可能な状態のすべてを生成する手法である。</li>
-<li>生成された状態の組み合わせを深さ優先探索で調べ、木構造で保存する。この時、同じ状態の組み合わせがあれば抽象化し共有することで、状態数が増えすぎる事を抑える。</li>
+<li>GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。</li>
+<li>codegear 実行後の状態を検査し、データベースに格納する。</li>
+<li>新しい上体が生成されなくなった時モデル検査が終了する。</li>
+<li>哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。</li>
+<li>必要な状態はフォークの状態だけになるので、それ以外の状態は無視することができる。</li>
+<li>これにより状態数を下げることができる。</li>
+<li>つまり、問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。</li>
 <li>GearsOS による検証用プログラムとして Dining Philosohers Ploblem (以下DPP）を用いる。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="14" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="15" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>DPP</h1>
 <ul>
 <li>5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。</li>
 <li>フォークは席の間に１本ずつある。哲学者は、思考とフォークを持つ、食事する。</li>
 </ul>
-<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>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="15" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="16" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>DPP</h1>
 <ul>
-<li>状態は以下のようになる<br />
+<li>状態は以下の構成要素からなる<br />
 Pickup Right<br />
 fork Pickup<br />
 Left fork eating Put Right fork<br />
 Put Left fork<br />
 Thinking</li>
 </ul>
-<center><img src="./pic/dpp_image.svg" alt="" width="50%" height="50%" /></center>
+<p><right><img src="./pic/dpp_image.svg" alt="" width="50%" height="50%" /></right></p>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="16" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="17" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>GeasOS におけるDPP実装(1/3)</h1>
 <ul>
 <li>5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。</li>
-<li>gearsOSには並列機構の　par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。</li>
+<li>gearsOSには並列機構の par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。</li>
 <li>par goto は引数として dataGear と実行後に継続する _exit をわたす。</li>
 <li>par goto は複数スレッドでの実行であるので、各スレッドで実行後に__exitに継続する事で終了する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="17" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="18" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>GearsOS におけるDPP実装(2/3)</h1>
 <ul>
-<li>マルチスレッドでのデータの一貫性を保証するのにSyncrhonized queue がある。</li>
-<li>Syncrhonized queue はCAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う。</li>
+<li>マルチスレッドでのデータの一貫性を保証する手法としてCAS がある。</li>
+<li>CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う。</li>
 <li>CAS は書き込みの際に、書き込む MetaCodeGear に更新前と更新後の値を渡し、更新前の値が保存されているメモリ番地の値と比較し同じデータがであれば書き込みを行う。異なる場合はほかからの書き込みがあったとみなし、値の更新に失敗し、もう一度CASを行う。</li>
 <li>DPPの例題ではフォークがスレッドで共有されるデータにあたるので、synchronixed Queue を用いることによってスレッド間での同期を行う。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="18" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="19" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
 <h1>GearsOS におけるDPP実装(3/3)</h1>
 <ul>
 <li>5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。</li>
@@ -233,8 +227,14 @@
 <li>またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq" data-marpit-pagination="19" data-marpit-pagination-total="19" style="--paginate:true;--theme:1k4ul11fffqn6mfg63zownsfu490x1y131x8rvu8suq;">
-<h1>まとめ</h1>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr" data-marpit-pagination="20" data-marpit-pagination-total="20" style="--paginate:true;--theme:vl9xq2qe7yx7y1tsxus7otwvroffivurz7uvmdagkr;">
+<h1>GearsOS でのモデル検査を実現する手法について</h1>
+<ul>
+<li>DPP をGearsOS 上のアプリケーションとして実装する。</li>
+<li>DPP codeGear のシャッフルの１つとして実行する。</li>
+<li>可能な実行を生成するiterator を作成する</li>
+<li>状態を記録するmemory Tree とstateDBを作成する。</li>
+</ul>
 </section>
 <script>!function(){"use strict";function t(t){Array.from(document.getElementsByTagName("svg"),e=>{if(e.hasAttribute("data-marpit-svg")){const{clientHeight:r,clientWidth:a}=e;e.style.transform||(e.style.transform="translateZ(0)");const o=t||e.currentScale||1,i=e.viewBox.baseVal.width/o,n=e.viewBox.baseVal.height/o,s=Math.min(r/n,a/i);Array.from(e.querySelectorAll(":scope > foreignObject"),t=>{const e=t.x.baseVal.value,o=t.y.baseVal.value;Array.from(t.querySelectorAll(":scope > section"),t=>{t.style.transformOrigin||(t.style.transformOrigin="0 0");const l=(a-s*i)/2-e,c=(r-s*n)/2-o;t.style.transform=`translate3d(${l}px,${c}px,0) scale(${s}) translate(${e}px,${o}px)`})})}})}const e=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function r(a=!0){for(const e of"Apple Computer, Inc."===navigator.vendor?[t]:[])e();Array.from(document.querySelectorAll('svg[data-marp-fitting="svg"]'),t=>{const r=t.firstChild,a=r.firstChild,{scrollWidth:o,scrollHeight:i}=a;let n,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(n=t.parentElement.parentElement),t.hasAttribute("data-marp-fitting-math")&&(n=t.parentElement),n){const t=getComputedStyle(n),e=Math.ceil(n.clientWidth-parseFloat(t.paddingLeft)-parseFloat(t.paddingRight));e&&(s=e)}const l=Math.max(o,s),c=Math.max(i,1),p=`0 0 ${l} ${c}`;e(r,"width",""+l),e(r,"height",""+c),e(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),e(t,"viewBox",p)&&t.classList.toggle("__reflow__")}),a&&window.requestAnimationFrame(()=>r(a))}!function(){if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");window.marpCoreBrowserScript?console.warn("Marp Core's browser script has already executed."):(Object.defineProperty(window,"marpCoreBrowserScript",{value:!0}),r())}()}();
 </script></foreignObject></svg></div><script>!function(){"use strict";var e=function(e,t){var n,r=1===(e.parent||e).nodeType?e.parent||e:document.querySelector(e.parent||e),s=[].filter.call("string"==typeof e.slides?r.querySelectorAll(e.slides):e.slides||r.children,(function(e){return"SCRIPT"!==e.nodeName})),a={},o=function(e,t){return(t=t||{}).index=s.indexOf(e),t.slide=e,t},i=function(e,t){a[e]=(a[e]||[]).filter((function(e){return e!==t}))},l=function(e,t){return(a[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},c=function(e,t){s[e]&&(n&&l("deactivate",o(n,t)),n=s[e],l("activate",o(n,t)))},d=function(e,t){var r=s.indexOf(n)+e;l(e>0?"next":"prev",o(n,t))&&c(r,t)},u={off:i,on:function(e,t){return(a[e]||(a[e]=[])).push(t),i.bind(null,e,t)},fire:l,slide:function(e,t){if(!arguments.length)return s.indexOf(n);l("slide",o(s[e],t))&&c(e,t)},next:d.bind(null,1),prev:d.bind(null,-1),parent:r,slides:s,destroy:function(e){l("destroy",o(n,e)),a={}}};return(t||[]).forEach((function(e){e(u)})),n||c(0),u};function t(e){e.parent.classList.add("bespoke-marp-parent"),e.slides.map(e=>e.classList.add("bespoke-marp-slide")),e.on("activate",t=>{e.slides.map(e=>e.classList.remove("bespoke-marp-active")),t.slide.classList.add("bespoke-marp-active")})}function n(e=2e3){return t=>{let n;function r(){n&&clearTimeout(n),n=setTimeout(()=>{t.parent.classList.add("bespoke-marp-inactive")},e),t.parent.classList.remove("bespoke-marp-inactive")}document.addEventListener("mousedown",r),document.addEventListener("mousemove",r),document.addEventListener("touchend",r),setTimeout(r,0)}}const r=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"];function s(e){e.parent.addEventListener("keydown",e=>{if(!e.target)return;const t=e.target;(r.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()})}function a(e){window.addEventListener("load",()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute("data-bespoke-marp-load",e)}})}function o(e){let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map(e=>[null,...e.querySelectorAll("[data-marpit-fragment]")])});const r=r=>void 0!==e.fragments[t][n+r],s=(r,s)=>{t=r,n=s,e.fragments.forEach((e,t)=>{e.forEach((e,n)=>{if(null==e)return;const a=t<r||t===r&&n<=s;e.setAttribute("data-bespoke-marp-fragment",a?"active":"inactive"),t===r&&n===s?e.setAttribute("data-bespoke-marp-current-fragment","current"):e.removeAttribute("data-bespoke-marp-current-fragment")})}),e.fragmentIndex=s;const a={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:s};e.fire("fragment",a)};e.on("next",()=>{if(r(1))return s(t,n+1),!1;const a=t+1;e.fragments[a]&&s(a,0)}),e.on("prev",()=>{if(r(-1))return s(t,n-1),!1;const a=t-1;e.fragments[a]&&s(a,e.fragments[a].length-1)}),e.on("slide",({index:t,fragment:n})=>{let r=0;if(void 0!==n){const s=e.fragments[t];if(s){const{length:e}=s;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}s(t,r)}),s(0,0)}var i,l=function(e,t){return e(t={exports:{}},t.exports),t.exports}((function(e){
--- 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を作成する。


-
-