Mercurial > hg > Papers > 2020 > anatofuz-sigos
changeset 58:b43d210923e7
...
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 28 May 2020 07:55:15 +0900 |
| parents | 92e7655a7458 |
| children | d1fe7f17320d |
| files | slide/slide.html slide/slide.md |
| diffstat | 2 files changed, 308 insertions(+), 49 deletions(-) [+] |
line wrap: on
line diff
--- a/slide/slide.html Wed May 27 22:04:40 2020 +0900 +++ b/slide/slide.html Thu May 28 07:55:15 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 xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu */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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="1" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +/* @theme v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79 */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="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="1" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="2" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="2" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="3" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="3" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="4" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="4" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="5" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="5" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="6" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="6" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>GearsOSでの信頼性の保証</h1> <ul> <li>メタレベルのみで信頼性の保証を行う @@ -118,12 +118,12 @@ </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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="7" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="7" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>GearsOSでの信頼性の保証</h1> <ul> <li>デフォルトのメタレベルの計算は自動生成される</li> <li>資源管理あるいは検証用のメタ計算は必要に応じて挿入する</li> -<li>これにより大きなコード変更無くモデル検査や定理証明を行うことができる</li> +<li>これにより大きなコード変更が無くモデル検査や定理証明を行うことができる</li> <li>モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する <ul> <li>例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮</li> @@ -132,7 +132,7 @@ </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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="8" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="8" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>CbCとCodeGear(ノーマルレベル)</h1> <ul> <li>軽量継続で表現する単位をCodeGearと呼ぶ</li> @@ -154,7 +154,21 @@ <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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="9" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="9" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> +<h1>CbCとCodeGear(メタレベル)</h1> +<ul> +<li><code>cbc_read_stub</code>内で必要な引数をcontextから取り出す +<ul> +<li>取得するものがなければノーマルレベルのCodeGearに継続する</li> +</ul> +</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">cbc_read_stub</span><span class="hljs-params">(struct Context* cbc_context, <span class="hljs-keyword">enum</span> Code next)</span> </span>{ + <span class="hljs-function"><span class="hljs-keyword">goto</span> <span class="hljs-title">cbc_read</span><span class="hljs-params">(cbc_context, 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="10" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="10" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>cbcで書き直したシステムコールディスパッチの例</h1> <ul> <li>CbCは<code>goto</code>文で呼び出す @@ -173,17 +187,34 @@ <span class="hljs-keyword">goto</span> (cbccodes[num])(cbc_ret); } </span></span></foreignObject></svg></code></pre> -<ul> -<li>呼び出し元には返ってこない +</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="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="11" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> +<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>{ + <span class="hljs-keyword">int</span> num; + <span class="hljs-keyword">int</span> ret; + + <span class="hljs-keyword">if</span>((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) { + proc->cbc_arg.cbc_console_arg.num = num; + <span class="hljs-keyword">goto</span> (cbccodes[num])(cbc_ret); + } +</span></span></foreignObject></svg></code></pre> <ul> -<li>goto trapreturn() ユーザープログラムにディスパッチする</li> -<li>goto panic() 致命的なエラーとしてOSを止める</li> -<li>goto err() システムコールのエラー処理をしてユーザープログラムにディスパッチする</li> +<li>呼び出し元には帰らず、 特定のCodeGearに継続を行う +<ul> +<li><code>goto trapreturn()</code> ユーザープログラムにディスパッチする</li> +<li><code>goto panic()</code> 致命的なエラーとしてOSを止める</li> +<li><code>goto err()</code> システムコールのエラー処理 +<ul> +<li>その後ユーザープログラムにディスパッチする</li> +</ul> +</li> </ul> </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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="10" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="12" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>CbCを用いたソフトウェアの実装</h1> <ul> <li>計算を実行するためのメモリ領域が必要 @@ -204,7 +235,7 @@ </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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="11" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="13" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>CbCのcotnext</h1> <ul> <li>CbCのプログラムで利用するCodeGearとデータの組を管理する機能 @@ -215,25 +246,24 @@ </li> <li>ノーマルレベルのCodeGear間を遷移するようにプログラミングする <ul> -<li>ノーマルレベルからはCodeGearを直接操作できない +<li>ノーマルレベルからはCodeGearを直接操作できず、 メタレベルで操作する <ul> <li>メタ計算中でCodeGearの番号をcontextでディスパッチする</li> </ul> </li> -<li>この間にMetaCodeGearが 実行される</li> </ul> </li> <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="12" data-paginate="true" data-theme="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="12" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="14" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <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="13" data-paginate="true" data-theme="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="13" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="15" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>実際のCbCプログラム</h1> <ul> <li>実際は1度contextを参照するMetaCodeGearに継続する @@ -244,7 +274,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="14" data-paginate="true" data-theme="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="14" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="16" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>実際のCbCプログラム</h1> <ul> <li>MetaCodeGearでは次の計算に必要なDataGearを取り出す @@ -255,16 +285,11 @@ </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="15" data-paginate="true" data-theme="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="15" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="17" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>CbCを用いたOSの再実装</h1> <ul> <li>CbCのCodeGearは状態遷移単位での記述に向いている</li> <li>状態遷移を基本としたモデルに変換し、HoareLogicなどの形式手法を用いて信頼性を高めたい</li> -<li>CbCは比較的文法が簡易 -<ul> -<li>Agda/Coqなどの定理証明からCbCへのコード変換が可能であると考えている</li> -</ul> -</li> <li>CbCや定理証明系を用いてアプリケーションとOSを再実装したい <ul> <li>最初の段階として既存のOSをCbCで再実装する</li> @@ -272,7 +297,7 @@ </li> </ul> </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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="16" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="18" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>xv6</h1> <ul> <li>マサチューセッツ工科大学で開発されたv6OSをもとにしたOS @@ -288,13 +313,13 @@ </li> <li>Raspberry Pi上で動作を目指したARM用のバージョンも存在する <ul> -<li>やっぱりRaspberryPiで動かしたい</li> +<li>RaspberryPiで動かしたい</li> <li>今回は ARMのバージョンをCbCで再実装する</li> </ul> </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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="17" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="19" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>xv6のCbCでの書き換え</h1> <ul> <li>既存のOSを段階的にCbCで書き換えていく @@ -307,7 +332,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="18" data-paginate="true" data-theme="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="18" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="20" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>read system callの書き換え</h1> <ul> <li>xv6のシステムコールの一部を書き換えることを検討する</li> @@ -326,7 +351,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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="19" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="21" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>read system callの継続の一部</h1> <ul> <li>実際に処理を切り分けているCodeGear @@ -355,7 +380,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="20" data-paginate="true" data-theme="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="20" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="22" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>read システムコールの状態遷移図</h1> <ul> <li>システムコール中のCodeGearを状態遷移図にした @@ -366,7 +391,19 @@ </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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="21" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="23" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> +<h1>システムコール単位での書き換え</h1> +<ul> +<li><code>cbc_fileread</code> CodeGearなどは複数のCodeGearの集合となっている +<ul> +<li>CodeGearの数が書き換えに伴って増えてしまう</li> +<li>CbCのInterface機能によってAPI単位でCodeGearのモジュール化を行っている</li> +</ul> +</li> +</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="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="24" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>Basic Block単位での書き換え</h1> <ul> <li>Basic Blockとはコンパイラの用語でループやリターンを区切りとするプログラミング単位 @@ -376,8 +413,14 @@ </ul> </li> <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="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="25" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> +<h1>Basic Block単位での書き換え</h1> +<ul> <li>仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている <ul> +<li><code>fs.c</code>や<code>vm.c</code>など</li> <li>CodeGear用のAPIをいきなり設計するのではなく、 段階的に書き換える</li> </ul> </li> @@ -388,10 +431,98 @@ </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="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="22" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> -<h1>メモリ管理部分の書き換え</h1> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="26" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> +<h1>ファイルシステム操作の書き換え</h1> +<ul> +<li>ファイルシステムのAPIが実装されている<code>fs.c</code>のAPIからCodeGearの集合を定義する +<ul> +<li>実装にはCbCのInterfaceを用いる</li> +<li>各APIの内部は複数のCodeGearの継続として実装する</li> +</ul> +</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-keyword">typedef</span> <span class="hljs-class"><span class="hljs-keyword">struct</span> <span class="hljs-title">fs</span><Type,Impl> {</span> + <span class="hljs-function">__code <span class="hljs-title">readsb</span><span class="hljs-params">(Impl* fs, uint dev, struct superblock* sb, __code next(...))</span></span>; + <span class="hljs-function">__code <span class="hljs-title">iinit</span><span class="hljs-params">(Impl* fs, __code next(...))</span></span>; + <span class="hljs-function">__code <span class="hljs-title">ialloc</span><span class="hljs-params">(Impl* fs, uint dev, short type, __code next(...))</span></span>; + <span class="hljs-function">__code <span class="hljs-title">iupdate</span><span class="hljs-params">(Impl* fs, struct inode* ip, __code next(...))</span></span>; + <span class="hljs-function">__code <span class="hljs-title">idup</span><span class="hljs-params">(Impl* fs, struct inode* ip, __code next(...))</span></span>; + <span class="hljs-function">__code <span class="hljs-title">ilock</span><span class="hljs-params">(Impl* fs, struct inode* ip, __code next(...))</span></span>; + <span class="hljs-function">__code <span class="hljs-title">iunlock</span><span class="hljs-params">(Impl* fs, struct inode* ip, __code next(...))</span></span>; + <span class="hljs-function">__code <span class="hljs-title">iput</span><span class="hljs-params">(Impl* fs, struct inode* ip, __code next(...))</span></span>; +.... +} 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="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="27" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> +<h1>もとのialloc関数</h1> +<ul> +<li>inodeのアロケーションを行う<code>ialloc</code>関数を書き換えた</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">struct inode* <span class="hljs-title">ialloc</span> <span class="hljs-params">(uint dev, short type)</span> +</span>{ + readsb(dev, &sb); + <span class="hljs-keyword">for</span> (inum = <span class="hljs-number">1</span>; inum < sb.ninodes; inum++) { + bp = bread(dev, IBLOCK(inum)); + dip = (struct dinode*) bp->data + inum % IPB; + + <span class="hljs-keyword">if</span> (dip->type == <span class="hljs-number">0</span>) { <span class="hljs-comment">// a free inode</span> + <span class="hljs-built_in">memset</span>(dip, <span class="hljs-number">0</span>, <span class="hljs-keyword">sizeof</span>(*dip)); + ... + <span class="hljs-keyword">return</span> iget(dev, inum); + } + brelse(bp); + } + panic(<span class="hljs-string">"ialloc: no inodes"</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="23" data-paginate="true" data-theme="xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu" data-marpit-pagination="23" data-marpit-pagination-total="23" style="--paginate:true;--theme:xaf9wumbjrcj6leq41cctez8slpif4zqklnz8ncdnu;"> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="28" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> +<h1>ialloc関数</h1> +<ul> +<li>対象のデバイスのinodeを一つずつ取り出すループ処理</li> +<li>空のinodeがあれば0で初期化後に<code>iget</code>でポインタを返す</li> +<li>アロケーションができなければpanicする</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">struct inode* <span class="hljs-title">ialloc</span> <span class="hljs-params">(uint dev, short type)</span> +</span>{ + readsb(dev, &sb); + <span class="hljs-keyword">for</span> (inum = <span class="hljs-number">1</span>; inum < sb.ninodes; inum++) { + bp = bread(dev, IBLOCK(inum)); + dip = (struct dinode*) bp->data + inum % IPB; + + <span class="hljs-keyword">if</span> (dip->type == <span class="hljs-number">0</span>) { <span class="hljs-comment">// a free inode</span> + <span class="hljs-built_in">memset</span>(dip, <span class="hljs-number">0</span>, <span class="hljs-keyword">sizeof</span>(*dip)); + ... + <span class="hljs-keyword">return</span> iget(dev, inum); + } + brelse(bp); + } + panic(<span class="hljs-string">"ialloc: no inodes"</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="29" data-paginate="true" data-theme="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="29" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> +<h1>ループ条件の確認のCodeGear</h1> +<ul> +<li>CbCでループ条件の判定を行うCodeGearを実装した +<ul> +<li><code>for (inum = 1; inum < sb.ninodes; inum++)</code>に対応する</li> +<li>ループ条件を満たなかった場合はpanicに移動する</li> +</ul> +</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</span><span class="hljs-params">(struct fs_impl* fs_impl, uint inum, struct superblock* sb, __code next(...))</span></span>{ + <span class="hljs-keyword">if</span>( inum < sb->ninodes){ + <span class="hljs-function"><span class="hljs-keyword">goto</span> <span class="hljs-title">allocinode_loop</span><span class="hljs-params">(fs_impl, next(...))</span></span>; + } + <span class="hljs-keyword">char</span>* msg = <span class="hljs-string">"failed allocinode..."</span>; + <span class="hljs-class"><span class="hljs-keyword">struct</span> <span class="hljs-title">Err</span>* <span class="hljs-title">err</span> = <span class="hljs-title">createKernelError</span>(&<span class="hljs-title">kernel</span>-><span class="hljs-title">cbc_context</span>);</span> + <span class="hljs-keyword">goto</span> err->panic(msg); +} +</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="v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79" data-marpit-pagination="30" data-marpit-pagination-total="30" style="--paginate:true;--theme:v6hn8h7l4tg8ne1ukz9ln213yxen5miovp2jk59lw9h79;"> <h1>まとめ</h1> <ul> <li>xv6の処理の一部を継続を用いてcbcで書き換えた
--- a/slide/slide.md Wed May 27 22:04:40 2020 +0900 +++ b/slide/slide.md Thu May 28 07:55:15 2020 +0900 @@ -75,7 +75,7 @@ - デフォルトのメタレベルの計算は自動生成される - 資源管理あるいは検証用のメタ計算は必要に応じて挿入する -- これにより大きなコード変更無くモデル検査や定理証明を行うことができる +- これにより大きなコード変更が無くモデル検査や定理証明を行うことができる - モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮 - OSの検証に利用できるinvariantの提供 @@ -100,6 +100,19 @@ ``` - cbcで書き直したxv6の`read`システムコールの例 + +--- +# CbCとCodeGear(メタレベル) + +- `cbc_read_stub`内で必要な引数をcontextから取り出す + - 取得するものがなければノーマルレベルのCodeGearに継続する + +```c +__code cbc_read_stub(struct Context* cbc_context, enum Code next) { + goto cbc_read(cbc_context, next); +} +``` + --- # cbcで書き直したシステムコールディスパッチの例 @@ -118,10 +131,28 @@ } ``` -- 呼び出し元には返ってこない - - goto trapreturn() ユーザープログラムにディスパッチする - - goto panic() 致命的なエラーとしてOSを止める - - goto err() システムコールのエラー処理をしてユーザープログラムにディスパッチする +--- + +# cbcで書き直したシステムコールディスパッチの例 + + +```c +void syscall(void) +{ + int num; + int ret; + + if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) { + proc->cbc_arg.cbc_console_arg.num = num; + goto (cbccodes[num])(cbc_ret); + } +``` + +- 呼び出し元には帰らず、 特定のCodeGearに継続を行う + - `goto trapreturn()` ユーザープログラムにディスパッチする + - `goto panic()` 致命的なエラーとしてOSを止める + - `goto err()` システムコールのエラー処理 + - その後ユーザープログラムにディスパッチする --- @@ -145,9 +176,8 @@ - データをDataGearという単位として扱う - 計算で使用する各DataGearを実際に保存している - ノーマルレベルのCodeGear間を遷移するようにプログラミングする - - ノーマルレベルからはCodeGearを直接操作できない + - ノーマルレベルからはCodeGearを直接操作できず、 メタレベルで操作する - メタ計算中でCodeGearの番号をcontextでディスパッチする - - この間にMetaCodeGearが 実行される - 実際のデータの入手、保存はcontextを触ることが出来るMeta Code Gearが行う --- @@ -182,8 +212,6 @@ - CbCのCodeGearは状態遷移単位での記述に向いている - 状態遷移を基本としたモデルに変換し、HoareLogicなどの形式手法を用いて信頼性を高めたい -- CbCは比較的文法が簡易 - - Agda/Coqなどの定理証明からCbCへのコード変換が可能であると考えている - CbCや定理証明系を用いてアプリケーションとOSを再実装したい - 最初の段階として既存のOSをCbCで再実装する @@ -197,7 +225,7 @@ - 基本的な機能は実装されている - システムコール、 ファイルシステム、 プロセス処理... - Raspberry Pi上で動作を目指したARM用のバージョンも存在する - - やっぱりRaspberryPiで動かしたい + - RaspberryPiで動かしたい - 今回は ARMのバージョンをCbCで再実装する @@ -261,21 +289,121 @@ --- +# システムコール単位での書き換え +- `cbc_fileread` CodeGearなどは複数のCodeGearの集合となっている + - CodeGearの数が書き換えに伴って増えてしまう + - CbCのInterface機能によってAPI単位でCodeGearのモジュール化を行っている + +<img src="assets/readsyscall.svg" alt="" style="padding-left: 20px;"> + +--- + # Basic Block単位での書き換え - Basic Blockとはコンパイラの用語でループやリターンを区切りとするプログラミング単位 - 長くかかるループは間にgotoを挟むことによりメタ計算を間にいれる - 1つのCodeGearにいる間は(論理的に)preemptされないことを保証する - これによりCodeGearを割り込まれない検証の単位とする事ができる + + +--- +# Basic Block単位での書き換え + - 仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている + - `fs.c`や`vm.c`など - CodeGear用のAPIをいきなり設計するのではなく、 段階的に書き換える - 今回はこれらの関数の内容をCodeGearで書き直した - 各関数への呼び出し時にダミーの関数を呼び出すことでCとCbCの相互移動が可能 --- -# メモリ管理部分の書き換え +# ファイルシステム操作の書き換え + +- ファイルシステムのAPIが実装されている`fs.c`のAPIからCodeGearの集合を定義する + - 実装にはCbCのInterfaceを用いる + - 各APIの内部は複数のCodeGearの継続として実装する + +```c +typedef struct fs<Type,Impl> { + __code readsb(Impl* fs, uint dev, struct superblock* sb, __code next(...)); + __code iinit(Impl* fs, __code next(...)); + __code ialloc(Impl* fs, uint dev, short type, __code next(...)); + __code iupdate(Impl* fs, struct inode* ip, __code next(...)); + __code idup(Impl* fs, struct inode* ip, __code next(...)); + __code ilock(Impl* fs, struct inode* ip, __code next(...)); + __code iunlock(Impl* fs, struct inode* ip, __code next(...)); + __code iput(Impl* fs, struct inode* ip, __code next(...)); +.... +} fs; +``` + +--- +# もとのialloc関数 +- inodeのアロケーションを行う`ialloc`関数を書き換えた + +```c +struct inode* ialloc (uint dev, short type) +{ + readsb(dev, &sb); + for (inum = 1; inum < sb.ninodes; inum++) { + bp = bread(dev, IBLOCK(inum)); + dip = (struct dinode*) bp->data + inum % IPB; + + if (dip->type == 0) { // a free inode + memset(dip, 0, sizeof(*dip)); + ... + return iget(dev, inum); + } + brelse(bp); + } + panic("ialloc: no inodes"); +} +``` +--- +# ialloc関数 + +- 対象のデバイスのinodeを一つずつ取り出すループ処理 +- 空のinodeがあれば0で初期化後に`iget`でポインタを返す +- アロケーションができなければpanicする + +```c +struct inode* ialloc (uint dev, short type) +{ + readsb(dev, &sb); + for (inum = 1; inum < sb.ninodes; inum++) { + bp = bread(dev, IBLOCK(inum)); + dip = (struct dinode*) bp->data + inum % IPB; + + if (dip->type == 0) { // a free inode + memset(dip, 0, sizeof(*dip)); + ... + return iget(dev, inum); + } + brelse(bp); + } + panic("ialloc: no inodes"); +} +``` + +--- + +# ループ条件の確認のCodeGear + +- CbCでループ条件の判定を行うCodeGearを実装した + - `for (inum = 1; inum < sb.ninodes; inum++)`に対応する + - ループ条件を満たなかった場合はpanicに移動する + +```c +__code allocinode_loopcheck(struct fs_impl* fs_impl, uint inum, struct superblock* sb, __code next(...)){ + if( inum < sb->ninodes){ + goto allocinode_loop(fs_impl, next(...)); + } + char* msg = "failed allocinode..."; + struct Err* err = createKernelError(&kernel->cbc_context); + goto err->panic(msg); +} +``` --- # まとめ