Mercurial > hg > Papers > 2020 > anatofuz-sigos

changeset 60:be3419709cd3 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 28 May 2020 09:41:45 +0900
parents d1fe7f17320d
children
files slide/slide.html slide/slide.md
diffstat 2 files changed, 97 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/slide/slide.html	Thu May 28 09:04:44 2020 +0900
+++ b/slide/slide.html	Thu May 28 09:41:45 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 j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict */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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="1" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+/* @theme mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis */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="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="1" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1><svg data-marp-fitting="svg"><foreignObject><span data-marp-fitting-svg-content> xv6の構成要素の継続の分析</span></foreignObject></svg></h1>
 <ul>
 <li>清水 隆博
@@ -27,7 +27,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="2" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="2" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>研究目的</h1>
 <ul>
 <li>アプリケーションの信頼性を向上させたい
@@ -44,7 +44,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="3" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="3" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>ノーマルレベルとメタレベルを用いた信頼性の向上</h1>
 <ul>
 <li>プログラムの実行部分は以下の2つからなる
@@ -65,7 +65,7 @@
 <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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="4" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="4" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>モデル検査</h1>
 <ul>
 <li>実際に想定されるパターンを全て動かして検証する</li>
@@ -78,7 +78,7 @@
 <li>Spinを用いる方法では、 promelaという言語で実装し直す必要がある</li>
 </ul>
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="5" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="5" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>定理証明支援系</h1>
 <ul>
 <li>論理学的なモデルに変更して証明する
@@ -100,7 +100,7 @@
 </li>
 </ul>
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="6" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="6" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>GearsOSでの信頼性の保証</h1>
 <ul>
 <li>メタレベルのみで信頼性の保証を行う
@@ -118,7 +118,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="7" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="7" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>GearsOSでの信頼性の保証</h1>
 <ul>
 <li>デフォルトのメタレベルの計算は自動生成される</li>
@@ -130,9 +130,10 @@
 <li>OSの検証に利用できるinvariantの提供</li>
 </ul>
 </li>
+<li>CbCを用いたOSであるGearsOSを開発している</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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="8" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="8" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>CbCとCodeGear(ノーマルレベル)</h1>
 <ul>
 <li>軽量継続で表現する単位をCodeGearと呼ぶ</li>
@@ -154,7 +155,7 @@
 <li>cbcで書き直したxv6の<code>read</code>システムコールの例</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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="9" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="9" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>CbCとCodeGear(メタレベル)</h1>
 <ul>
 <li><code>cbc_read_stub</code>内で必要な引数をcontextから取り出す
@@ -168,7 +169,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="10" data-paginate="true" data-theme="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="10" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="10" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>cbcで書き直したシステムコールディスパッチの例</h1>
 <ul>
 <li>CbCは<code>goto</code>文で呼び出す
@@ -188,7 +189,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="11" data-paginate="true" data-theme="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="11" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="11" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>cbcで書き直したシステムコールディスパッチの例</h1>
 <pre><code class="language-c"><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">void</span> <span class="hljs-title">syscall</span><span class="hljs-params">(<span class="hljs-keyword">void</span>)</span>
 </span>{
@@ -214,7 +215,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="12" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="12" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>CbCを用いたソフトウェアの実装</h1>
 <ul>
 <li>計算を実行するためのメモリ領域が必要
@@ -235,7 +236,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="13" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="13" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>CbCのcotnext</h1>
 <ul>
 <li>CbCのプログラムで利用するCodeGearとデータの組を管理する機能
@@ -256,14 +257,14 @@
 <li>実際のデータの入手、保存はcontextを触ることが出来るMeta Code Gearが行う</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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="14" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="14" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>通常のCbCプログラム</h1>
 <ul>
 <li>プログラマから見るとCodeGearからCodeGearへの継続のみに見える<br />
 <img src="assets/context1.svg" alt="" style="padding-left: 100px;" /></li>
 </ul>
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="15" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="15" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>実際のCbCプログラム</h1>
 <ul>
 <li>実際は1度contextを参照するMetaCodeGearに継続する
@@ -274,7 +275,7 @@
 </ul>
 <img src="assets/context2.svg" alt="" style="padding-left: 100px;" />
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="16" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="16" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>実際のCbCプログラム</h1>
 <ul>
 <li>MetaCodeGearでは次の計算に必要なDataGearを取り出す
@@ -285,7 +286,7 @@
 </ul>
 <img src="assets/context_last.svg" alt="" style="padding-left: 100px;" />
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="17" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="17" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>CbCを用いたOSの再実装</h1>
 <ul>
 <li>CbCのCodeGearは状態遷移単位での記述に向いている</li>
@@ -297,7 +298,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="18" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="18" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>xv6</h1>
 <ul>
 <li>マサチューセッツ工科大学で開発されたv6OSをもとにしたOS
@@ -319,7 +320,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="19" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="19" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>xv6のCbCでの書き換え</h1>
 <ul>
 <li>既存のOSを段階的にCbCで書き換えていく
@@ -332,7 +333,7 @@
 <li>CbCのcontextをプロセス構造体に埋め込み、 <code>goto</code>文を利用する場合はcontextからデータを参照する</li>
 </ul>
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="20" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="20" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>read system callの書き換え</h1>
 <ul>
 <li>xv6のシステムコールの一部を書き換えることを検討する</li>
@@ -351,7 +352,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="21" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="21" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>read system callの継続の一部</h1>
 <ul>
 <li>実際に処理を切り分けているCodeGear
@@ -380,7 +381,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="22" data-paginate="true" data-theme="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="22" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="22" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>read システムコールの状態遷移図</h1>
 <ul>
 <li>システムコール中のCodeGearを状態遷移図にした
@@ -391,7 +392,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="23" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="23" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>システムコール単位での書き換え</h1>
 <ul>
 <li><code>cbc_fileread</code> CodeGearなどは複数のCodeGearの集合となっている
@@ -403,7 +404,7 @@
 </ul>
 <img src="assets/readsyscall.svg" alt="" style="padding-left: 20px;" />
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="24" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="24" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>Basic Block単位での書き換え</h1>
 <ul>
 <li>Basic Blockとはコンパイラの用語でループやリターンを区切りとするプログラミング単位
@@ -415,7 +416,7 @@
 <li>これによりCodeGearを割り込まれない検証の単位とする事ができる</li>
 </ul>
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="25" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="25" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>Basic Block単位での書き換え</h1>
 <ul>
 <li>仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている
@@ -431,7 +432,7 @@
 </li>
 </ul>
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="26" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="26" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>ファイルシステム操作の書き換え</h1>
 <ul>
 <li>ファイルシステムのAPIが実装されている<code>fs.c</code>のAPIからCodeGearの集合を定義する
@@ -454,7 +455,7 @@
 } fs;
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="27" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="27" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="27" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>もとのialloc関数</h1>
 <ul>
 <li>inodeのアロケーションを行う<code>ialloc</code>関数を書き換えた</li>
@@ -477,7 +478,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="28" data-paginate="true" data-theme="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="28" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="28" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>ialloc関数</h1>
 <ul>
 <li>対象のデバイスのinodeを一つずつ取り出すループ処理</li>
@@ -502,8 +503,8 @@
 }
 </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="29" data-paginate="true" data-theme="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="29" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
-<h1>ループ条件の確認のCodeGear</h1>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="29" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="29" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
+<h1>ループ条件の確認のCodeGear(ノーマルレベル)</h1>
 <ul>
 <li>CbCでループ条件の判定を行うCodeGearを実装した
 <ul>
@@ -522,8 +523,22 @@
 }
 </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="30" data-paginate="true" data-theme="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="30" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
-<h1>ループに復帰するかの判定</h1>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="30" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="30" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
+<h1>ループ条件の確認のCodeGear(メタレベル)</h1>
+<ul>
+<li>ノーマルレベルの直前に実行され、contextから値を取り出す</li>
+</ul>
+<pre><code class="language-c"><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">__code <span class="hljs-title">allocinode_loopcheck_stub</span><span class="hljs-params">(struct Context* cbc_context)</span> </span>{
+        fs_impl* fs_impl = Gearef(cbc_context, fs_impl);
+        uint inum = Gearef(cbc_context, fs_impl)-&gt;inum;
+        superblock* sb = Gearef(cbc_context, fs_impl)-&gt;sb;
+        <span class="hljs-keyword">enum</span> Code next = Gearef(cbc_context, fs_impl)-&gt;next;
+        <span class="hljs-function"><span class="hljs-keyword">goto</span> <span class="hljs-title">allocinode_loopcheck</span><span class="hljs-params">(cbc_context, fs_impl, inum, sb, 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="31" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="31" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
+<h1>ループに復帰するかの判定(ノーマルレベル)</h1>
 <ul>
 <li>空のinodeがあるかどうか(<code>dip-&gt;type == 0)</code>で継続を分岐させる
 <ul>
@@ -546,7 +561,21 @@
 }
 </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="31" data-paginate="true" data-theme="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="31" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="32" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="32" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
+<h1>ループに復帰するかの判定(メタレベル)</h1>
+<ul>
+<li>同様に計算に必要は値を取り出して継続する</li>
+</ul>
+<pre><code class="language-c"><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">__code <span class="hljs-title">allocinode_loop_stub</span><span class="hljs-params">(struct Context* cbc_context)</span> </span>{
+        fs_impl* fs_impl = Gearef(cbc_context, fs_impl);
+        uint inum = Gearef(cbc_context, fs_impl)-&gt;inum;
+        short type = Gearef(cbc_context, fs_impl)-&gt;type;
+        <span class="hljs-keyword">enum</span> Code next = Gearef(cbc_context, fs_impl)-&gt;next;
+        <span class="hljs-function"><span class="hljs-keyword">goto</span> <span class="hljs-title">allocinode_loop</span><span class="hljs-params">(cbc_context, fs_impl, inum, type, 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="33" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="33" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>BasicBlock単位での書き換えの考察</h1>
 <ul>
 <li>従来のxv6の関数呼び出しをもとにしているために、コードの変更点が少ない</li>
@@ -558,7 +587,7 @@
 </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="j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict" data-marpit-pagination="32" data-marpit-pagination-total="32" style="--paginate:true;--theme:j18ztucocdha700kv6ro3v1zvd7gi16wpae5ix87hict;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="34" data-paginate="true" data-theme="mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis" data-marpit-pagination="34" data-marpit-pagination-total="34" style="--paginate:true;--theme:mpvqxndejjoz4s2vkaglp3cbxyd3d62e4o8nexdwis;">
 <h1>まとめ</h1>
 <ul>
 <li>xv6の処理の一部を継続を用いてcbcで書き換えた
--- a/slide/slide.md	Thu May 28 09:04:44 2020 +0900
+++ b/slide/slide.md	Thu May 28 09:41:45 2020 +0900
@@ -79,6 +79,7 @@
 - モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する
     - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮
     - OSの検証に利用できるinvariantの提供
+- CbCを用いたOSであるGearsOSを開発している
 
 ---
 # CbCとCodeGear(ノーマルレベル)
@@ -388,7 +389,7 @@
 
 ---
 
-# ループ条件の確認のCodeGear
+# ループ条件の確認のCodeGear(ノーマルレベル)
 
 - CbCでループ条件の判定を行うCodeGearを実装した
     - `for (inum = 1; inum < sb.ninodes; inum++)`に対応する
@@ -406,8 +407,23 @@
 ```
 
 ---
+# ループ条件の確認のCodeGear(メタレベル)
 
-# ループに復帰するかの判定
+- ノーマルレベルの直前に実行され、contextから値を取り出す
+
+```c
+__code allocinode_loopcheck_stub(struct Context* cbc_context) {
+        fs_impl* fs_impl = Gearef(cbc_context, fs_impl);
+        uint inum = Gearef(cbc_context, fs_impl)->inum;
+        superblock* sb = Gearef(cbc_context, fs_impl)->sb;
+        enum Code next = Gearef(cbc_context, fs_impl)->next;
+        goto allocinode_loopcheck(cbc_context, fs_impl, inum, sb, next);
+}
+```
+
+---
+
+# ループに復帰するかの判定(ノーマルレベル)
 - 空のinodeがあるかどうか(`dip->type == 0)`で継続を分岐させる
     - 0のものがあった場合は初期化を行うCodeGearに遷移する
     - なければループ条件の確認のCodeGearに継続する
@@ -428,6 +444,21 @@
 ```
 
 ---
+# ループに復帰するかの判定(メタレベル)
+
+- 同様に計算に必要は値を取り出して継続する
+
+```c
+__code allocinode_loop_stub(struct Context* cbc_context) {
+        fs_impl* fs_impl = Gearef(cbc_context, fs_impl);
+        uint inum = Gearef(cbc_context, fs_impl)->inum;
+        short type = Gearef(cbc_context, fs_impl)->type;
+        enum Code next = Gearef(cbc_context, fs_impl)->next;
+        goto allocinode_loop(cbc_context, fs_impl, inum, type, next);
+}
+```
+
+---
 # BasicBlock単位での書き換えの考察
 
 - 従来のxv6の関数呼び出しをもとにしているために、コードの変更点が少ない
@@ -435,6 +466,7 @@
 - APIそのものはCodeGearを基本とした状態に書き直していない
     - スタックを前提とした処理と共存している
 
+
 ---
 # まとめ
 - xv6の処理の一部を継続を用いてcbcで書き換えた