Mercurial > hg > Papers > 2022 > soto-sigos

changeset 10:07afffd7bf05

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
WIP スライドを作成中
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Tue, 24 May 2022 19:32:38 +0900
parents bc8222372b9d
children ae8ea72d5c41
files slide/slide.md slide/slide.pdf
diffstat 2 files changed, 21 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/slide/slide.md	Mon May 23 17:16:09 2022 +0900
+++ b/slide/slide.md	Tue May 24 19:32:38 2022 +0900
@@ -10,7 +10,7 @@
     background-color: #FFFFFF;
     font-size: 28px;
     color: #4b4b4b;
-    font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN";
+    font-family: "Hiragino Maru Gothic ProN";
     background-image: url("logo.svg");
     background-position: right 3% bottom 2%;
     background-repeat: no-repeat;
@@ -49,7 +49,7 @@
 ---
 <!-- headingDivider: 1 -->
 
-# Gears Agda による <br> Left Learning Red Black Tree の検証
+# Gears Agda 上のモデル検査の形式化
 <!-- class: title -->
 
 Uechi Yuto, Shinji Kono 琉球大学
@@ -64,7 +64,7 @@
 
 - この際、アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。このアルゴリズム適応前後の処理の恒等性を検証するため、Gears Agda を用いる。
 
-# Gears Agda と CbCの説明 (いらないかも
+# Gears Agda と CbC
 - Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のこと
 - 通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。この際メインルーチンで使用していた変数などの環境はスタックされ、サブルーチンが終了した際にメインルーチンに戻り、スタックしていた変数をもとに戻す流れとなる。
 - CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ、スタックを持たず環境を保持しない。更に遷移後にメインルーチンに戻ることもない。つまり関数の実行では暗黙な環境が存在せず、関数が受け取った引数のみを使用する。
@@ -147,40 +147,34 @@
 <!-- 今回はここでモデル検査の処理を行う -->
 
 # Normal level と Meta Level の対応
-![height:400px](meta-cg-dg.jpg)
+![height:400px](meta-ca-dg.jpg)
 
 # DPPの説明
-哲学者がいて〜
-フォークがあって〜
+![height:500px](DPP.jpg)
 
 # モデル検査と定理証明の説明
 モデル検査はコストが安いが完全な検証にはならない
 定理証明はコスト高いが完全な検証になる
 
 # DPPの記述
-DPPをこんな感じで書いて行くよ的な
+- DPPはマルチプロセスの同期問題である
+  - しかし、Agdaでは並列実行をサポートしていないため、step実行毎に一つづつ処理することで並列実行を表現している
 
-# モデル検査
-ビット全探索を今回は行った
-
-# モデル検査
-デッドロック検知
+- 加えて、哲学者が思考中に食事をし始めるのか、食事中に思考に戻ろうとするのかで分岐が発生する
+  - これを網羅するために今回はその状態に対してビット全探索を行った
 
-# 今後の研究方針
-- Deleteの実装
-- Red Black Tree の実装
-  - 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
-- Contextを用いた並列実行時のプログラムの正しさの証明
-  - synchronized queue
-  - concurrent tree
-- xv.6への適用
-- モデル検査
+# モデル検査でのデッドロック検知
+- デッドロックとは全てのプロセスが他のプロセスの実行待ちの状態となり実行が進まなくなること
+- 今回Gears Agda でのデッドロックの定義として、以下2つを満たすものとした
+  - ビット全探索で分岐が作れない
+  - 実行時に状態に変動がない
+- これでプログラムがデッドロックしているのか検知するところまではできるようになった
 
-# まとめ
-- Gears Agda にて Binary Tree を検証することができた
-  - Gears Agda における Termination を使用しない実装の仕方を確立した
-  - Hoare Logic による検証もできるようになった
-  - 今後は Red Black Tree の検証をすすめる
-- モデル検査をしたい
+# まとめと今後の研究方針
+- 今回は Gears Agda にてDPPを記述し、モデル検査にてデッドロックを検知できるようになった
+  - 今回のモデル検査を一般化し、自動でモデル検査を実行できるようにしたい
+  - さらにプログラムの仕様を渡し、これを満たしているかモデル検査で検証したい
+    - 仕様にLTLを使えるようにもしたい
+- アルゴリズムの自動適応にて、モデル検査で仕様を満たしている場合に入れ替えて同じ動作をしているかを定理証明で証明できるようにしたい
 
 <!-- 英語版も欲しい -->
Binary file slide/slide.pdf has changed