Mercurial > hg > Papers > 2022 > soto-sigos

changeset 14:ba98083f9853 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FIX
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 27 May 2022 12:31:39 +0900
parents 517b22769bf7
children
files slide/slide.md slide/slide.pdf
diffstat 2 files changed, 113 insertions(+), 55 deletions(-) [+]
line wrap: on
line diff
--- a/slide/slide.md	Thu May 26 22:39:23 2022 +0900
+++ b/slide/slide.md	Fri May 27 12:31:39 2022 +0900
@@ -58,42 +58,37 @@
 <!-- class: slide -->
 
 <!-- 研究目的 -->
-- 思い思いにプログラムを書くと、冗長なコードができてしまい、実行時間も遅い場合がある。この場合にコードに対してアルゴリズムを適応すると、一般的に良いコードが作成できる。
-
-- しかし、世の中にはすでに大量のアルゴリズムが存在するため、これを一人のプログラマーが全て覚え、適応できる場面を思いつくというのは初学者には難しい。そのため、人が書いたコードに対してアルゴリズムを使用するコードに自動的に変換できるようにしたい。
-
-- この際、アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。このアルゴリズム適応前後の処理の恒等性を検証するため、Gears Agda を用いる。
-
-# Gears Agda と CbC
-- Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のこと
-- 通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。この際メインルーチンで使用していた変数などの環境はスタックされ、サブルーチンが終了した際にメインルーチンに戻り、スタックしていた変数をもとに戻す流れとなる。
-- CbCの場合はサブルーチンコールの際にアセンブラでいうjmpで関数遷移を行うことができ、スタックを持たず環境を保持しない。更に遷移後にメインルーチンに戻ることもない。つまり関数の実行では暗黙な環境が存在せず、関数が受け取った引数のみを使用する。
-- これにより限定的な実行条件を作成でき、検証がしやすくなる。
+<!-- 思い思いにプログラムを書くと冗長なコードができてしまい、実行時間も遅い場合がある。この場合にコードに対して他のアルゴリズムを適応すると、一般的に良いコードが作成できる。-->
+- コードの改良の繰り返しで開発していきたい
+- 改良はアルゴリズムの変更を含む
+- 変更前と変更後の動作が一致することを検証したい
+- プログラムをGears Agdaで記述し、Agdaによるモデル検査により検証する
+- Agda Curry-Howard対応に基づく関数型言語、定理証明支援系
+- CbC Cの下位言語で軽量継続gotoで記述する
+- Gears Agda Agdaにより記述されたCbCプログラム
 
 # Gears Agda でのアルゴリズム入れ替え判定
-- 現在、アルゴリズムの適応可否は以下の方法を考えている。
-
-  - あらかじめ、アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく
-
-  - 書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき、満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える
-
-- この際、実装が仕様を満たしているか検証する手法には、定理証明やモデル検査などが挙げられる。
+- gears Agdaでアルゴリズムの記述とアルゴリズムの証明(invariant)を同時に記述する
+- invariantを変換できればアルゴリズムを置換できる
+- 変換はAgdaでの証明で行う
+- 非決定的な実行が存在する場合は可能な実行を網羅する(モデル検査)
+- AgdaでGears Agdaのモデル検査の定式化を行う
 
 # Gears Agda でのモデル検査
-- アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い、アルゴリズムの仕様がコードに適応できるか検証するのが妥当だと考えている
-
-- 思い思いに書いたコードに対して定理証明を行うのはコストが高く、適応するものの内部動作が一致しない場合定理証明を行っても使えないためである
-
-- アルゴリズムの入れ替え可否をモデル検査で判定し、入れ替えたあとに適応前後で同じ処理をしていることを定理証明で検証することを目標としている
-
-- この Gears Agda でのモデル検査の先駆けとして今回は Dining Philosophers Program のモデル検査をboundedで行っている
+- 非決定的な実行の例として並列実行がある
+- 5人の哲学者が共有されたフォークを取り合う例題 Dining Philosophers Program 
+- Live Lock と Dead Lockの検出を行う
+- Gears Agda の実行を複数のContext(プロセス)でemurationする
+- 5人のtep実行のshuffring
+- 可能な状態の網羅のためのDataBase
+- とりあえずboundedで実装した
 
 # CbC について
 - CbCとは当研究室で開発しているC言語の下位言語
-  - 継続呼び出しは引数付き goto 文で表現される。
+  - 継続呼び出しは引数付き goto 文で表現される
     - 関数呼び出し時にスタックの操作を行わずjmp命令で次の処理に移動する
   - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
-- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。
+- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う
 
 
 # Agda の基本 
@@ -104,29 +99,19 @@
 - 関数の定義は = を用いて行う
   - 関数名の後ろの行で、 = の前で受け取る引数を記述、=の後ろで実装を記述する
 
-<!--
-curry-Houerd対応
-```
-sample1 : (A : Set ) → Set
-sample1 a = a
-
-sample2 : (A : Set ) → (B : Set ) → Set
-sample2 a b = b
-```
--->
-
 
 # Gears Agda の記法
-<!-- plusのほうがいい予感 -->
 Gears Agda では CbC と対応させるためにすべてLoopで記述する
 loopは`→ t`の形式で表現する
 再帰呼び出しは使わない(構文的には禁止していないので注意が必要)
 ```
-{-# TERMINATING #-}
-whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
-whileLoop env next with lt 0 (varn env)
-whileLoop env next | false = next env
-whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+init-table : {n : Level} {t : Set n} → ℕ → (exit : Env → t) → t
+init-table n exit = init-table-loop n 0 (record {table = [] ; ph = []}) exit where
+  init-table-loop : {n : Level} {t : Set n} → (redu inc : ℕ) → Env → (exit : Env → t) → t
+  init-table-loop zero ind env exit = exit env
+  init-table-loop (suc redu) ind env exit = init-table-loop redu (suc ind) record env{
+    table = 0 ∷ (table env)
+    ; ph = record {pid = redu ; left-hand = false ; right-hand = false ; next-code = C_thinking } ∷ (ph env) } exit
 ```
 - t を返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
 - tail call により light weight continuation を定義している
@@ -147,9 +132,9 @@
 <!-- 今回はここでモデル検査の処理を行う -->
 
 # Normal level と Meta Level の対応
-![height:400px](meta-ca-dg.jpg)
+![height:400px](meta-cg-dg.jpg)
 
-# Dining Philosophers Program の説明
+# Dining Philosophers Program
 ![height:500px](DPP.jpg)
 
 # モデル検査と定理証明の説明
@@ -157,26 +142,99 @@
 - 入力を無限に検証することはできないため、定理証明と比べると完全な検証にならない
 - 定理証明に比べてコストが低い
 
-# Dining Philosophers Program の記述
+# Dining Philosophers Program の実装
 - DPPはマルチプロセスの同期問題である
   - しかし、Agdaでは並列実行をサポートしていないため、step実行毎に一つづつ処理することで並列実行を表現している
 - 加えて、哲学者が思考中に食事をし始めるのか、食事中に思考に戻ろうとするのかで分岐が発生する
   - 今回はその状態に対して網羅することでモデル検査をboundedに行っている
 
+# Dining Philosophers Program の実装
+Gears Agdaで使用するData Gearを以下のように定義した
+```
+record Phi : Set where
+  field
+    pid : ℕ
+    right-hand : Bool
+    left-hand : Bool
+    next-code : Code
+open Phi
+```
+```
+record Env : Set where
+  field
+    table : List ℕ
+    ph : List Phi
+open Env
+```
+
+# Dining Philosophers Program の実装
+```
+data Code : Set  where
+   C_putdown_rfork : Code
+   C_putdown_lfork : Code
+   C_thinking : Code
+   C_pickup_rfork : Code
+   C_pickup_lfork : Code
+   C_eating : Code
+```
+
+```
+code_table : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t
+code_table C_putdown_rfork = putdown-rfork-c
+code_table C_putdown_lfork = putdown-lfork-c
+code_table C_thinking = thinking-c
+code_table C_pickup_rfork = pickup-rfork-c
+code_table C_pickup_lfork = pickup-lfork-c
+code_table C_eating = eating-c
+```
+
+# Dining Philosophers Program の実装
+以下が哲学者の動作の実装の一つ
+```
+pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
+pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where
+  pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
+  pickup-lfork-p zero f [] p env exit with table env
+  ... | [] = exit env
+  ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ;
+         next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)}
+  ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])}
+  pickup-lfork-p zero f (0 ∷ ts) p env exit = exit record env{
+    ph = ((ph env) ++ (record p{left-hand = true ;
+         next-code = C_eating} ∷ [])); table = (f ++ ((pid p) ∷ ts))}
+```
+
 # モデル検査でのデッドロック検知
 - 現在は探索する深さを指定している(boundedなモデル検査)
-- デッドロックとは全てのプロセスが他のプロセスの実行待ちの状態となり実行が進まなくなること
-- 今回Gears Agda でのデッドロックの定義として、以下2つを満たすものとした
+- 今回Gears Agdaでのデッドロックの定義として、以下2つを設定した
   - 網羅で分岐が作れない
   - 実行時に状態に変動がない
-- これでプログラムがデッドロックしているのか検知するところまではできるようになった
+- これでプログラムがdead Lockしているのか検知するところまではできた
+
+# モデル検査でのデッドロック検知
+網羅には以下のMetaCodeGearを実装した(一部抜粋)
+```
+brute-force-search : {n : Level} {t : Set n} 
+  → Env → (exit : List Env → t) → t
+brute-force-search env exit = make-state-list 
+  1 [] (ph env) env (env ∷ []) exit where
+  make-state-list : {n : Level} {t : Set n} 
+    → ℕ → List Bool → List Phi 
+    → Env → (List Env) → (exit : List Env → t) → t
+  make-state-list redu state (x ∷ pl) env envl exit with next-code x
+  ... | C_thinking = make-state-list (redu + redu) 
+    (state ++ (false ∷ [])) pl env envl exit
+  ... | C_eating = make-state-list (redu + redu)
+    (state ++ (false ∷ [])) pl env envl exit
+  ... | _ = make-state-list redu state pl env envl exit
+  make-state-list redu state [] env envl exit = 
+    bit-force-search redu [] state env envl exit where
+```
 
 # まとめと今後の研究方針
-- 今回は Gears Agda にて Dining Philosophers Program を記述し、モデル検査にてデッドロックをboundedに検知できるようになった
-  - unboundedなデッドロック検知ができるように
-  - 今回のモデル検査を一般化し、自動でモデル検査を実行できるように
-  - さらにプログラムの仕様を渡し、これを満たしているかモデル検査で検証
+- 今回は Gears Agda にて Dining Philosophers Program を記述し、モデル検査にてデッドロックをboundedに検知できた
+  - unboundedなデッドロック検知
+  - プログラムの仕様(invariant)を渡し、これを満たしているかモデル検査で検証
     - 仕様にLTLを使えるように
 - アルゴリズムの自動適応にて、モデル検査で仕様を満たしている場合に入れ替えて同じ動作をしているかを定理証明で証明できるようにしたい
 
-<!-- 英語版も欲しい -->
Binary file slide/slide.pdf has changed