Mercurial > hg > Papers > 2018 > nozomi-master

comparison presentation/slide.pdf.html @ 121:137aae675a94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slide
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 14 Feb 2017 15:03:04 +0900
parents 8a84cda440f3
children c195713cf7d7
comparison
equal deleted inserted replaced
120:8a84cda440f3 121:137aae675a94
68 68
69 <div class='slide '> 69 <div class='slide '>
70 <!-- === begin markdown block === 70 <!-- === begin markdown block ===
71 71
72 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16] 72 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
73 on 2017-02-14 11:30:47 +0900 with Markdown engine kramdown (1.13.0) 73 on 2017-02-14 15:02:42 +0900 with Markdown engine kramdown (1.13.0)
74 using options {} 74 using options {}
75 --> 75 -->
76 76
77 <!-- _S9SLIDE_ --> 77 <!-- _S9SLIDE_ -->
78 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1> 78 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1>
128 </div> 128 </div>
129 <div class='slide '> 129 <div class='slide '>
130 <!-- _S9SLIDE_ --> 130 <!-- _S9SLIDE_ -->
131 <h1 id="section-3">モデル検査的アプローチについての流れ</h1> 131 <h1 id="section-3">モデル検査的アプローチについての流れ</h1>
132 <ul> 132 <ul>
133 <li>既存のモデル検査器について</li>
133 <li>Continuation based C (CbC) 言語について</li> 134 <li>Continuation based C (CbC) 言語について</li>
134 <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li> 135 <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li>
135 <li>CbC とメタ計算について</li> 136 <li>CbC とメタ計算について</li>
136 <li>CbC で記述された GearsOS とそのデータ構造である赤黒木</li> 137 <li>CbC で記述された GearsOS とそのデータ構造である赤黒木</li>
137 <li>赤黒木の仕様の定義とその検証手法</li> 138 <li>赤黒木の仕様の定義とその検証手法</li>
138 </ul>
139
140
141 </div>
142 <div class='slide '>
143 <!-- _S9SLIDE_ -->
144 <h1 id="continuation-based-c">Continuation based C</h1>
145 <ul>
146 <li>当研究室で開発しているプログラミング言語</li>
147 <li>アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語</li>
148 <li>OS や組み込みソフトウェアなどを対象にしている</li>
149 <li>CodeSegment と DataSegment という単位を用いてプログラミングする</li>
150 <li>両検証手法をメタ計算として利用可能</li>
151 </ul>
152
153
154 </div>
155 <div class='slide '>
156 <!-- _S9SLIDE_ -->
157 <h1 id="codesegment">CodeSegment</h1>
158 <ul>
159 <li>CodeSegment とは
160 <ul>
161 <li>処理の単位であり、入力と出力を持つ</li>
162 <li>結合や分割が容易</li>
163 </ul>
164 </li>
165 <li>CodeSegment どうしを接続することによりプログラム全体を作る
166 <ul>
167 <li>関数呼び出しと違って戻ってこない(goto)</li>
168 </ul>
169 </li>
170 </ul>
171
172 <p><img src="./images/cs.svg" alt="cs" width="50%" /></p>
173
174 <pre><code>__code cs0(int a, int b){
175 goto cs1(a+b);
176 }
177 </code></pre>
178
179
180 </div>
181 <div class='slide '>
182 <!-- _S9SLIDE_ -->
183 <h1 id="datasegment">DataSegment</h1>
184 <ul>
185 <li>DataSegment とは
186 <ul>
187 <li>データの単位</li>
188 <li>CodeSegment の入出力にあたる</li>
189 <li>接続元の Output DataSegment は接続先の Input DataSegment</li>
190 </ul>
191 </li>
192 </ul>
193
194 <p><img src="./images/ds.svg" alt="ds" width="50%" /></p>
195
196 <pre><code>__code cs0(int a, int b){
197 goto cs1(a+b);
198 }
199 </code></pre>
200
201
202 </div>
203 <div class='slide '>
204 <!-- _S9SLIDE_ -->
205 <h1 id="section-4">メタ計算</h1>
206 <ul>
207 <li>とある計算を実現するための計算</li>
208 <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
209 <li>CbC は通常レベルの計算とメタ計算を分離して考える
210 <ul>
211 <li>通常レベルではポインタは出てこない、など</li>
212 </ul>
213 </li>
214 <li>CodeSegment の接続部分に処理を追加することで実現</li>
215 </ul>
216
217 <p><img src="./images/meta.svg" alt="meta" width="50%" /></p>
218
219
220 </div>
221 <div class='slide '>
222 <!-- _S9SLIDE_ -->
223 <h1 id="meta-codesegment">Meta CodeSegment</h1>
224 <ul>
225 <li>メタ計算を行なう CodeSegment</li>
226 <li>通常の CodeSegment どうしの接続の間に入る</li>
227 </ul>
228
229 <p><img src="./images/mcs.svg" alt="mcs" width="50%" /></p>
230
231
232 </div>
233 <div class='slide '>
234 <!-- _S9SLIDE_ -->
235 <h1 id="meta-datasegment">Meta DataSegment</h1>
236 <ul>
237 <li>メタ計算用の DataSegment</li>
238 <li>通常の DataSegment を含むような DataSegment</li>
239 </ul>
240
241 <p><img src="./images/mds.svg" alt="mds" width="50%" /></p>
242
243
244 </div>
245 <div class='slide '>
246 <!-- _S9SLIDE_ -->
247 <h1 id="gearsos">並列に信頼性高く動作する GearsOS</h1>
248 <ul>
249 <li>CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある</li>
250 <li>並列実行やモデル検査をメタ計算として提供する</li>
251 <li>現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み</li>
252 <li>今回はこの非破壊赤黒木の検証を行なう</li>
253 </ul>
254
255
256 </div>
257 <div class='slide '>
258 <!-- _S9SLIDE_ -->
259 <h1 id="section-5">赤黒木</h1>
260 <ul>
261 <li>データの保存に用いる二分木</li>
262 <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
263 <ul>
264 <li>ルートノードと葉ノードの色は黒</li>
265 <li>赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)</li>
266 <li>ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定</li>
267 </ul>
268 </li>
269 </ul>
270
271 <p><img src="./images/rbtree.svg" alt="rbtree" width="35%" /></p>
272
273
274 </div>
275 <div class='slide '>
276 <!-- _S9SLIDE_ -->
277 <h1 id="gearsos-">GearsOS における赤黒木の利用例(ノードの挿入)</h1>
278 <ul>
279 <li>挿入したい要素を DataSegment に格納して次の CodeSegment へ goto</li>
280 <li>goto する前に Meta CodeSegment が実行されて木に挿入する</li>
281 <li>GearsOS では木の実装のためにスタックを用いて経路情報を保持している</li>
282 </ul>
283
284 <p><img src="./images/put.svg" alt="put" width="50%" /></p>
285
286 <pre><code>goto meta(context, Put);
287 </code></pre>
288
289
290 </div>
291 <div class='slide '>
292 <!-- _S9SLIDE_ -->
293 <h1 id="section-6">仕様の記述とその確認</h1>
294 <ul>
295 <li>「バランスが取れている」とは何かを表現できる必要がある
296 <ul>
297 <li>実行可能な CbC の式を使った assert になる</li>
298 </ul>
299 </li>
300 <li>そしてそれを保証したい
301 <ul>
302 <li>プログラムの全ての状態においてこれは常に成り立つのか?</li>
303 </ul>
304 </li>
305 </ul> 139 </ul>
306 140
307 141
308 </div> 142 </div>
309 <div class='slide '> 143 <div class='slide '>
337 <ul> 171 <ul>
338 <li>条件分岐を網羅的に実行</li> 172 <li>条件分岐を網羅的に実行</li>
339 </ul> 173 </ul>
340 </li> 174 </li>
341 <li>仕様は bool になる式を用いた assert</li> 175 <li>仕様は bool になる式を用いた assert</li>
342 <li>有限ステップ検証する有界モデル検査器</li> 176 <li>有限ステップだけ検証する有界モデル検査器</li>
343 </ul> 177 </ul>
344 </li> 178 </li>
345 </ul> 179 </ul>
346 180
347 <pre><code>assert(x &lt; 10); 181 <pre><code>assert(x &lt; 10);
348 </code></pre> 182 </code></pre>
183
184
185 </div>
186 <div class='slide '>
187 <!-- _S9SLIDE_ -->
188 <h1 id="continuation-based-c">Continuation based C</h1>
189 <ul>
190 <li>当研究室で開発しているプログラミング言語</li>
191 <li>アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語</li>
192 <li>OS や組み込みソフトウェアなどを対象にしている</li>
193 <li>CodeSegment と DataSegment という単位を用いてプログラミングする</li>
194 <li>モデル検査と証明の両検証手法をメタ計算として利用可能
195 <ul>
196 <li>CbC で CbC 自身を検証可能</li>
197 </ul>
198 </li>
199 </ul>
200
201
202 </div>
203 <div class='slide '>
204 <!-- _S9SLIDE_ -->
205 <h1 id="codesegment">CodeSegment</h1>
206 <ul>
207 <li>CodeSegment とは
208 <ul>
209 <li>処理の単位であり、入力と出力を持つ</li>
210 <li>結合や分割が容易</li>
211 </ul>
212 </li>
213 <li>CodeSegment どうしを接続することによりプログラム全体を作る
214 <ul>
215 <li>関数呼び出しと違って戻ってこない(goto)</li>
216 </ul>
217 </li>
218 </ul>
219
220 <p><img src="./images/cs.svg" alt="cs" width="50%" /></p>
221
222 <pre><code>__code cs0(int a, int b){
223 goto cs1(a+b);
224 }
225 </code></pre>
226
227
228 </div>
229 <div class='slide '>
230 <!-- _S9SLIDE_ -->
231 <h1 id="datasegment">DataSegment</h1>
232 <ul>
233 <li>DataSegment とは
234 <ul>
235 <li>データの単位</li>
236 <li>CodeSegment の入出力にあたる</li>
237 <li>接続元の Output DataSegment は接続先の Input DataSegment</li>
238 </ul>
239 </li>
240 </ul>
241
242 <p><img src="./images/ds.svg" alt="ds" width="50%" /></p>
243
244 <pre><code>__code cs0(int a, int b){
245 goto cs1(a+b);
246 }
247 </code></pre>
248
249
250 </div>
251 <div class='slide '>
252 <!-- _S9SLIDE_ -->
253 <h1 id="section-4">メタ計算</h1>
254 <ul>
255 <li>とある計算を実現するための計算</li>
256 <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
257 <li>CbC は通常レベルの計算とメタ計算を分離して考える
258 <ul>
259 <li>通常レベルではポインタは出てこない、など</li>
260 </ul>
261 </li>
262 <li>CodeSegment の接続部分に処理を追加することで実現</li>
263 </ul>
264
265 <p><img src="./images/meta.svg" alt="meta" width="50%" /></p>
266
267
268 </div>
269 <div class='slide '>
270 <!-- _S9SLIDE_ -->
271 <h1 id="meta-codesegment">Meta CodeSegment</h1>
272 <ul>
273 <li>メタ計算を行なう CodeSegment</li>
274 <li>通常の CodeSegment どうしの接続の間に入る</li>
275 </ul>
276
277 <p><img src="./images/mcs.svg" alt="mcs" width="75%" /></p>
278
279
280 </div>
281 <div class='slide '>
282 <!-- _S9SLIDE_ -->
283 <h1 id="meta-datasegment">Meta DataSegment</h1>
284 <ul>
285 <li>メタ計算用の DataSegment</li>
286 <li>通常の DataSegment を含むような DataSegment</li>
287 </ul>
288
289 <p><img src="./images/mds.svg" alt="mds" width="75%" /></p>
290
291
292 </div>
293 <div class='slide '>
294 <!-- _S9SLIDE_ -->
295 <h1 id="gearsos">並列に信頼性高く動作する GearsOS</h1>
296 <ul>
297 <li>CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある</li>
298 <li>並列実行やモデル検査をメタ計算として提供する</li>
299 <li>現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み</li>
300 <li>今回はこの非破壊赤黒木の検証を行なう</li>
301 </ul>
302
303
304 </div>
305 <div class='slide '>
306 <!-- _S9SLIDE_ -->
307 <h1 id="section-5">赤黒木</h1>
308 <ul>
309 <li>データの保存に用いる二分木</li>
310 <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
311 <ul>
312 <li>ルートノードと葉ノードの色は黒</li>
313 <li>赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)</li>
314 <li>ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定</li>
315 </ul>
316 </li>
317 </ul>
318
319 <p><img src="./images/rbtree.svg" alt="rbtree" width="35%" /></p>
320
321
322 </div>
323 <div class='slide '>
324 <!-- _S9SLIDE_ -->
325 <h1 id="gearsos-">GearsOS における赤黒木の利用例(ノードの挿入)</h1>
326 <ul>
327 <li>挿入したい要素を DataSegment に格納して次の CodeSegment へ goto</li>
328 <li>goto する前に Meta CodeSegment が実行されて木に挿入する</li>
329 </ul>
330
331 <p><img src="./images/put.svg" alt="put" width="50%" /></p>
332
333 <pre><code>goto meta(context, Put);
334 </code></pre>
335
336
337 </div>
338 <div class='slide '>
339 <!-- _S9SLIDE_ -->
340 <h1 id="section-6">仕様の記述とその確認</h1>
341 <ul>
342 <li>「バランスが取れている」とは何かを表現できる必要がある
343 <ul>
344 <li>実行可能な CbC の条件式を使った assert になる</li>
345 </ul>
346 </li>
347 <li>そしてそれを保証したい
348 <ul>
349 <li>プログラムの全ての状態においてこれは常に成り立つのか?</li>
350 </ul>
351 </li>
352 </ul>
349 353
350 354
351 </div> 355 </div>
352 <div class='slide '> 356 <div class='slide '>
353 <!-- _S9SLIDE_ --> 357 <!-- _S9SLIDE_ -->
389 </ul> 393 </ul>
390 </li> 394 </li>
391 <li>ノーマルレベルのコードを検証用に変更せず検証可能</li> 395 <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
392 </ul> 396 </ul>
393 397
394 <p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p> 398 <p><img src="./images/akashaPut.svg" alt="akashaPut" width="50%" /></p>
395 399
396 400
397 </div> 401 </div>
398 <div class='slide '> 402 <div class='slide '>
399 <!-- _S9SLIDE_ --> 403 <!-- _S9SLIDE_ -->
420 <div class='slide '> 424 <div class='slide '>
421 <!-- _S9SLIDE_ --> 425 <!-- _S9SLIDE_ -->
422 <h1 id="continuation-based-c-">定理証明を Continuation based C へ適用するには</h1> 426 <h1 id="continuation-based-c-">定理証明を Continuation based C へ適用するには</h1>
423 <ul> 427 <ul>
424 <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li> 428 <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li>
425 <li>そのままプログラムの性質を保証してやる</li> 429 <li>直接プログラムの性質を証明</li>
426 <li>Coq, Agda, ATS2 などのプログラミング言語で証明が可能 430 <li>Coq, Agda, ATS2 などのプログラミング言語で証明が可能
427 <ul> 431 <ul>
428 <li>本当は CbC で CbC 自身を証明したい</li> 432 <li>本当は CbC で CbC 自身を証明したい</li>
429 <li>しかし CbC の形式的な定義が無いために今はできない</li> 433 <li>しかし CbC の形式的な定義が無いために今はできない</li>
430 </ul> 434 </ul>
436 </div> 440 </div>
437 <div class='slide '> 441 <div class='slide '>
438 <!-- _S9SLIDE_ --> 442 <!-- _S9SLIDE_ -->
439 <h1 id="agda--datasegment">Agda と DataSegment</h1> 443 <h1 id="agda--datasegment">Agda と DataSegment</h1>
440 <ul> 444 <ul>
441 <li>CbC の DataSegment は Agda のレコード型</li> 445 <li>CbC の DataSegment は Agda のレコード型
446 <ul>
447 <li>名前付きの値が複数ある(C の構造体)</li>
448 </ul>
449 </li>
442 </ul> 450 </ul>
443 451
444 <pre><code>__code cs0(int a, int b){ 452 <pre><code>__code cs0(int a, int b){
445 goto cs1(a+b); 453 goto cs1(a+b);
446 } 454 }
455 </div> 463 </div>
456 <div class='slide '> 464 <div class='slide '>
457 <!-- _S9SLIDE_ --> 465 <!-- _S9SLIDE_ -->
458 <h1 id="agda--codesegment">Agda と CodeSegment</h1> 466 <h1 id="agda--codesegment">Agda と CodeSegment</h1>
459 <ul> 467 <ul>
460 <li>CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)</li> 468 <li>CbC の CodeSegment は、Agda の関数型
469 <ul>
470 <li>Input を取って Output を返す</li>
471 </ul>
472 </li>
461 </ul> 473 </ul>
462 474
463 <pre><code>__code cs0(int a, int b){ 475 <pre><code>__code cs0(int a, int b){
464 goto cs1(a+b); 476 goto cs1(a+b);
465 } 477 }
562 </div> 574 </div>
563 <div class='slide '> 575 <div class='slide '>
564 <!-- _S9SLIDE_ --> 576 <!-- _S9SLIDE_ -->
565 <h1 id="section-10">今後の課題</h1> 577 <h1 id="section-10">今後の課題</h1>
566 <ul> 578 <ul>
579 <li>より大きなサイズの赤黒木の検証</li>
580 <li>赤黒木の挿入に関する性質を証明する</li>
567 <li>部分型を利用してCbCを型付け</li> 581 <li>部分型を利用してCbCを型付け</li>
568 <li>依存型をCbC に導入して自身を証明可能にする</li> 582 <li>依存型をCbC に導入して自身を証明可能にする</li>
569 <li>型情報から stub を自動生成すkる</li> 583 <li>型情報から stub を自動生成すkる</li>
570 <li>赤黒木の挿入に関する性質を証明する</li>
571 </ul> 584 </ul>
572 585
573 586
574 </div> 587 </div>
575 <div class='slide '> 588 <div class='slide '>