Mercurial > hg > Papers > 2021 > ikkun-master
changeset 5:4c39c90d1b1b
fix
| author | ikkun <ikkun@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 15 Feb 2021 14:50:17 +0900 |
| parents | 3139ed741e26 |
| children | 15e75aa845ea |
| files | poster/poster.html poster/poster.md |
| diffstat | 2 files changed, 47 insertions(+), 121 deletions(-) [+] |
line wrap: on
line diff
--- a/poster/poster.html Mon Feb 15 13:56:04 2021 +0900 +++ b/poster/poster.html Mon Feb 15 14:50:17 2021 +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 vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr */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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="1" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +/* @theme wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d */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="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="1" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1><svg data-marp-fitting="svg"><foreignObject><span data-marp-fitting-svg-content> Gears OSでモデル検査を実現する手法について</span></foreignObject></svg></h1> <ul> <li>東恩納 琢偉 @@ -22,27 +22,26 @@ </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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="2" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="2" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>研究目的</h1> <ul> <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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="3" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="3" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>Gears OS</h1> <ul> <li>Continuation based C によって記述されている。</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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="4" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="4" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>Continution based C (CbC)</h1> <ul> <li>Gear という単位で分割され、goto 文によって遷移する。</li> -<li>codeGear は プログラムにおける処理記述になっている。</li> -<li>また 変数や構造体といったデータは dataGear に保管される。</li> +<li>プログラムにおける処理記述を codeGear と呼ぶ。</li> +<li>変数や構造体といったデータは dataGear に保管される。</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 pickup<span class="hljs-constructor">_lfork(<span class="hljs-params">struct</span> PhilsImpl<span class="hljs-operator">*</span> <span class="hljs-params">phils</span>, <span class="hljs-params">__code</span> <span class="hljs-params">next</span>(<span class="hljs-operator">...</span>)</span>) { @@ -53,17 +52,17 @@ </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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="5" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="5" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>goto</h1> <ul> -<li>CbC での遷移は軽量継続といいgoto 文を用いる。</li> +<li>goto 文による遷移を軽量継続という。</li> <li>これは関数呼び出しと異なり、stackや環境を隠して持つことがありません。</li> <li>CbC において、処理を行うのは codeGear であるため、プログラムの状態の変化は codeGear によって決まる。</li> <li>よって CbC での遷移記述をそのまま状態記述とすることが出来る。</li> </ul> <center><img src="./pic/goto.svg" alt="" width="80%" height="80%" /></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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="6" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="6" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>メタ計算</h1> <ul> <li>軽量継続である CbC は遷移する際に別の処理を挟む事が可能で、この処理をメタ計算という。</li> @@ -71,7 +70,7 @@ </ul> <center><img src="./pic/meta_gear2.svg" alt="" width="90%" height="90%" /></center> </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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="7" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="7" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>data Gear と meta dataGear</h1> <ul> <li>CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル<br /> @@ -79,12 +78,12 @@ <li>メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearも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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="8" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="8" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>stub CodeGear (メタレベルからノーマルレベルへの橋渡し)</h1> <ul> <li>メタレベルから見ると、code Gearの入力はcontext ただ1つである。</li> <li>ノーマルレベルからメタレベルの context を直接参照してしまうことはできない。</li> -<li>context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub codeGearを用意する。</li> +<li>context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出す、仲介役としてメタレベルの stub 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 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->top = NULL; @@ -98,17 +97,16 @@ } </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="9" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="9" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="9" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>プロセスであるcontext の並べ替えによる並列実行</h1> <ul> <li>プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。</li> -<li>並列実行の非決定性は、実行される codeGear の並び替えを生成し、contextの状態を数え上げる。</li> -<li>これがモデル検査になる。</li> +<li>並列実行の非決定性は、実行される codeGear の並び替えを生成し、contextの状態を数え上げることでモデル検査を行う。</li> <li>並び替えの数(プログラム全体の可能な状態)はとても巨大になる場合がある。</li> <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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="10" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="10" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>codeGearのatomicity</h1> <ul> <li>codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。</li> @@ -116,62 +114,24 @@ <li>GearsOS においては codeGear が正しくatomicに実行されるように実装する。</li> </ul> </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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="11" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> -<h1>モデル検査する仕様の記述法</h1> -<ul> -<li> -<p>検証したい内容を時様相論理式 p をつくり、対象のシステムの初期状態 s のモデル M があるとき、M,s |= p(M,s が p を満たすか)をモデル検査器を用いて調べることによって信頼性を保証する手法である。</p> -</li> -<li> -<p>時相論理式にはCTL(Computation Tree Logic) や LTTL(Linear Time Temporal Logic)といったものがあり、それぞれ計算木と線形時相論理式と言われるものである。</p> -</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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="12" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> -<h1>他のモデル検査実装例</h1> -<ul> -<li> -<p>SPIN<br /> -Promela (Process Meta Language)で仕様と実装を記述する。</p> -</li> -<li> -<p>Java Path Finder<br /> -JVM を直接シュミレーション実行する。<br /> -様相論理ではなくassert 検証したい性質を記述する。</p> -</li> -<li> -<p>XMV<br /> -CMU で開発されたモデル検査器<br /> -SAT solver</p> -</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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="13" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> -<h1>Geras OS のモデル検査</h1> -<ul> -<li>CbC によって記述されており、CbC の記述そのものを状態遷移として落とし込む。</li> -<li>par goto により複数スレッドの並行実行する。</li> -<li>メタ計算によって並行実行のモデル検査を行う。</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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="14" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> -<h1>Gears OS におけるモデル検査の実装手順</h1> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="11" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> +<h1>Gears OS におけるモデル検査</h1> <ol> <li>GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。</li> <li>codegear 実行後の状態を、データベースに格納する。</li> <li>新しい状態が生成されなくなった時モデル検査が終了する。</li> <li>哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。</li> -<li>必要な状態はフォークの状態だけになるので、それ以外の状態は無視することができる。</li> +<li>必要な状態はフォークの状態と哲学者の状態で、それ以外の状態は無視することができる。</li> <li>これにより状態数を下げることができる。</li> <li>問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。</li> <li>GearsOS による検証用プログラムとして Dining Philosohers Ploblem (DPP）を用いる。</li> </ol> </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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="15" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="12" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>DPP</h1> <p><right><img src="./pic/dpp_image.svg" alt="" height="90%" /></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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="16" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="13" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>DPP(dining philosohers ploblem)</h1> <ul> <li>5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。</li> @@ -180,7 +140,7 @@ <code>Pickup Right fork</code> <code> Pickup Left fork</code> <code>eating</code> <code> Put Right fork</code> <code>Put Left fork</code> <code>Thinking</code></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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="17" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="14" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>GearsOS におけるDPP実装(1/2)</h1> <ul> <li>マルチスレッドでのデータの一貫性を保証する手法としてCheck and Set (CAS) を用いる。</li> @@ -189,7 +149,7 @@ <li>DPPの例題ではフォークがスレッドで共有されるデータにあたるので、CAS を用いることによってスレッド間での同期を行う。</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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="18" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="15" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>GearsOS におけるDPP実装(2/2)</h1> <ul> <li>5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表される。</li> @@ -198,40 +158,40 @@ <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="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="19" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="16" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <center><img src="./pic/model_checking.svg" width="50%" /></center> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="20" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="17" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>GearsOS でのモデル検査を実現する方法について</h1> <ul> <li>DPP をGearsOS 上のアプリケーションとして実装する。</li> <li>DPP を codeGear の１つとしてシャッフル実行する。</li> -<li>可能な実行を生成する iterator</li> +<li>可能な実行を生成する iterator を作成する。</li> <li>状態を記録する memory Tree と stateDB を作成する。</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="21" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="18" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>モデル検査器の現状</h1> <ul> <li>GearsOS 上での導出木の生成</li> <li>生成した木のマーキングによる時相論理の検証</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="22" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> -<h1>Metaの入れ替え</h1> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="19" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> +<h1>シャッフル実行</h1> <ul> <li>perl script を用いて、遷移先のmetaを置き換える事が可能となっている。</li> <li>遷移先のmetaを切り替えることによって、ノーマルレベルで走るプログラムを書き換える事なく、mcMeta によるシングルスレッド実行と並列実行ようのランダム実行を行う事が出来る。</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="23" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="20" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>モデル検査のフラグ管理</h1> <ul> <li>モデル検査を行う際に全ての状態を網羅的に実行していく、この時実行した状態にフラグを立てていくことによって走った状態を記録しておく。</li> <li>フラグはeating のt_eating と、¬◇ eating の f_F_eating フラグの2種類で、食事中といつか食事できないを表している。</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="24" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="21" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>DPP のメタ計算</h1> <ul> <li>導出木を作る時にはノーマルレベルの putdown_lfrok は putdown_lforkPhilsImpl となり、context に代入を行うマクロである Gearef を使いCaS を行う。<br /> @@ -252,7 +212,7 @@ } </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="25" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="25" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="22" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>mcDPP</h1> <ul> <li>フラグを確認しモデル検査を行っている。</li> @@ -282,7 +242,7 @@ </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="26" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="26" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="23" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1><a href="http://meta.pm">meta.pm</a></h1> <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><span class="hljs-function"><span class="hljs-keyword">sub</span> <span class="hljs-title">replaceMeta</span> </span>{ <span class="hljs-keyword">return</span> ( @@ -305,7 +265,7 @@ <span class="hljs-number">1</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="27" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="27" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="24" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>まとめ</h1> <ul> <li> @@ -318,11 +278,11 @@ <p><a href="http://meta.pm">meta.pm</a> を使うことでモデル検査を行う際のランダム生成を行う事が可能になった。</p> </li> <li> -<p>GeearsOS で汎用モデル検査器を作ることができた。</p> +<p>GearsOS で汎用モデル検査器を作ることができた。</p> </li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="28" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="25" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>今後の展開</h1> <ul> <li> @@ -336,7 +296,7 @@ </li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="29" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="29" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="26" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>GearsOS の GearsOS によるモデル検査</h1> <ul> <li>GerasOS そのものも codeGear で記述されている。</li> @@ -347,7 +307,7 @@ <li>異なるmeta codeGear を指定してコンパイル出来る。</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="30" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="30" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="27" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="27" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>OS のモデル検査における問題点</h1> <ul> <li>他のアプリケーションと違い、OS の記述はそれ自体が メタレベルのものであるため、それをemulationする方法を考える必要がある。</li> @@ -356,14 +316,13 @@ -ユーザーcontext が単純であっても OS は膨大な状態数を有するので、その全てを探索するのが厳しいと考えられる。</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="31" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="31" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-theme="wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d" data-marpit-pagination="28" data-marpit-pagination-total="28" style="--paginate:true;--theme:wu5b79v8xwgs8vdb7xw6f410kvjflfpdai617ct837d;"> <h1>OS のモデル検査</h1> <ul> <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="32" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="32" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"></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/poster/poster.md Mon Feb 15 13:56:04 2021 +0900 +++ b/poster/poster.md Mon Feb 15 14:50:17 2021 +0900 @@ -13,7 +13,7 @@ - OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こる。 - 本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性の保証をOSの機能として行うことを目指しており、本研究ではモデル検査をもちいた手法について発表する。 -- また GearsOS そのものを GearsOS 上でモデル検査する手法についても考察する。 + --- # Gears OS @@ -26,8 +26,8 @@ # Continution based C (CbC) - Gear という単位で分割され、goto 文によって遷移する。 -- codeGear は プログラムにおける処理記述になっている。 -- また 変数や構造体といったデータは dataGear に保管される。 +- プログラムにおける処理記述を codeGear と呼ぶ。 +- 変数や構造体といったデータは dataGear に保管される。 - 下の例題は CbC によって記述された codeGear である。 ``` __code pickup_lfork(struct PhilsImpl* phils, __code next(...)) { @@ -41,7 +41,7 @@ --- # goto -- CbC での遷移は軽量継続といいgoto 文を用いる。 +- goto 文による遷移を軽量継続という。 - これは関数呼び出しと異なり、stackや環境を隠して持つことがありません。 - CbC において、処理を行うのは codeGear であるため、プログラムの状態の変化は codeGear によって決まる。 - よって CbC での遷移記述をそのまま状態記述とすることが出来る。 @@ -71,7 +71,7 @@ - メタレベルから見ると、code Gearの入力はcontext ただ1つである。 - ノーマルレベルからメタレベルの context を直接参照してしまうことはできない。 -- context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub codeGearを用意する。 +- context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出す、仲介役としてメタレベルの stub codeGearを用意する。 ``` __code clearSingleLinkedStack(struct Context *context,struct SingleLinkedStack* stack,enum Code next) { @@ -91,8 +91,7 @@ # プロセスであるcontext の並べ替えによる並列実行 - プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。 -- 並列実行の非決定性は、実行される codeGear の並び替えを生成し、contextの状態を数え上げる。 -- これがモデル検査になる。 +- 並列実行の非決定性は、実行される codeGear の並び替えを生成し、contextの状態を数え上げることでモデル検査を行う。 - 並び替えの数(プログラム全体の可能な状態)はとても巨大になる場合がある。 - 状態はデータベースに格納する。 @@ -104,38 +103,6 @@ - 一般的には、他の codeGear が共有されたdataGearに競合的に書き込んだり、割り込みにより処理が中断したりする。 - GearsOS においては codeGear が正しくatomicに実行されるように実装する。 ---- - -# モデル検査する仕様の記述法 <> - -- 検証したい内容を時様相論理式 p をつくり、対象のシステムの初期状態 s のモデル M があるとき、M,s |= p(M,s が p を満たすか)をモデル検査器を用いて調べることによって信頼性を保証する。。 - -- 時相論理式にはCTL(Computation Tree Logic) や LTTL(Linear Time Temporal Logic)といったものがあり、それぞれ計算木と線形時相論理式と言われるものである。 - - ----- - -# 他のモデル検査実装例<> -- SPIN - Promela (Process Meta Language)で仕様と実装を記述する。 - -- Java Path Finder - JVM を直接シュミレーション実行する。 - 様相論理ではなくassert 検証したい性質を記述する。 - -- XMV - CMU で開発されたモデル検査器 - SAT solver - ----- - -# Geras OS のモデル検査 - -- CbC によって記述されており、CbC の記述そのものを状態遷移として落とし込む。 -- par goto により複数スレッドの並行実行する。 -- メタ計算によって並行実行のモデル検査を行う。 - - ---- # Gears OS におけるモデル検査 @@ -188,7 +155,7 @@ - DPP をGearsOS 上のアプリケーションとして実装する。 - DPP を codeGear の１つとしてシャッフル実行する。 -- 可能な実行を生成する iterator +- 可能な実行を生成する iterator を作成する。 - 状態を記録する memory Tree と stateDB を作成する。 --- @@ -200,7 +167,7 @@ ---- -# Metaの入れ替え +# シャッフル実行 - perl script を用いて、遷移先のmetaを置き換える事が可能となっている。 - 遷移先のmetaを切り替えることによって、ノーマルレベルで走るプログラムを書き換える事なく、mcMeta によるシングルスレッド実行と並列実行ようのランダム実行を行う事が出来る。 @@ -293,7 +260,7 @@ - meta.pm を使うことでモデル検査を行う際のランダム生成を行う事が可能になった。 -- GeearsOS で汎用モデル検査器を作ることができた。 +- GearsOS で汎用モデル検査器を作ることができた。 ----