Mercurial > hg > Papers > 2023 > moririn-sigos

changeset 7:cedf88ea18b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 13 May 2023 16:14:11 +0900
parents 9e85fa1cc6a8
children 2514493ae067
files presen.ind
diffstat 1 files changed, 160 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/presen.ind	Sat May 13 14:49:30 2023 +0900
+++ b/presen.ind	Sat May 13 16:14:11 2023 +0900
@@ -218,29 +218,176 @@
   並列実行単位は codeGear
   非決定性は Monad だが、定義された meta levelのスケジューラで決まる
 
+--Invariant
 
------story
+ data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
+    t-leaf : treeInvariant leaf 
+    t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf) 
+    t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} 
+       → key < key₁ → treeInvariant (node key₁ value₁ t₁ t₂)
+       → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) 
+    t-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} 
+       → key < key₁ → treeInvariant (node key value t₁ t₂)
+       → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) 
+    t-node  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} 
+       → key < key₁ → key₁ < key₂
+       → treeInvariant (node key value t₁ t₂) 
+       → treeInvariant (node key₂ value₂ t₃ t₄)
+       → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 
+
+割と当たり前。Invariant だが
+
+　　可能な順序のある二分木全部の集合
+
+に相当する。つまり、Invariant というよりは表示的意味論になってる。
+
+--停止条件
+
+証明は(項として)有限である必要があるので、停止条件が必要になる
+
+    TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } 
+       → ( reduce : Index → ℕ)
+       → (r : Index) → (p : Invraiant r)  
+       → (loop : (r : Index)  → Invraiant r 
+           → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t) → t
+
+これは Indexが自然数で減少するならループが停止する命題である。これは Agda で証明されている
+(それほどながくない)
+
+これは、codeGear の loop connector になっている
+
+リンカは単純にリンクするのではなく、停止条件も接続する必要がある
+
+呼び出し方の例
+
+insertTreeP {n} {m} {A} {t} tree key value P0 exit =
+   TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } 
+          (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫  ⟪ P0 , s-nil ⟫
+       $ λ p P loop → findP key (proj1 p)  tree (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt ) 
+       $ λ t s P C → replaceNodeP key value t C (proj1 P) ...
+
+loop で接続されているのがわかる。⟪ P0 , s-nil ⟫などで実際に証明を渡している。
+
+--何を証明しているのか?
+
+insertTreeP なら、exit で抜けた時に、treeinvariant と、元の木の値が変わっているinvariantが得られる
+
+ここから必要な性質は全部証明できる
+
+--Red Black Tree の invariant (leaf / single )
+
+data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → (bd : ℕ) → Set n where
+    rb-leaf     : RBtreeInvariant leaf 0
+    rb-single : (key : ℕ) → (value : A) →  RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) 1
+
+--Red Black Tree の invariant (leaf case )
+
+    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} 
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 1
+       → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) 1
+    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color}
+       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
+       → RBtreeInvariant (node key  ⟪ Black , value  ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) 1
+    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} 
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 1
+       → RBtreeInvariant (node key₁  ⟪ Red ,   value  ⟫ (node key ⟪ Black , value₁ ⟫ t t₁) leaf ) 1
+    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color}
+       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
+       → RBtreeInvariant (node key₁  ⟪ Black , value  ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) 1
+
+--Red Black Tree の invariant (intermidiate node)
 
-------simple while program
+    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → (d : ℕ)
+       → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) d
+       → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) d
+       → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) d
+    rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → (d : ℕ)
+       → {c c₁ : Color}
+       → RBtreeInvariant (node key  ⟪ c  , value  ⟫ t₁ t₂) d
+       → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) d
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) (suc d)
+
+そこそこ複雑だが、treeInvariant と直交して書ける
+
+--invariant
+
+red black tree は rotate を含むので結構複雑
+
+record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) 
+      (orig repl : bt (Color ∧ A) ) 
+      (stack : List (bt (Color ∧ A)))  : Set n where
+   field
+       od d rd : ℕ
+       tree rot : bt (Color ∧ A)
+       origti : treeInvariant orig 
+       origrb : RBtreeInvariant orig od
+       treerb : RBtreeInvariant tree d
+       replrb : RBtreeInvariant repl rd
+       d=rd : ( d ≡ rd ) ∨ ( (suc d ≡ rd ) ∧ (color tree ≡ Red))
+       si : stackInvariant key tree orig stack
+       rotated : rotatedTree tree rot
+       ri : replacedRBTree key value (child-replaced key rot ) repl
+
+--concurrency (Dining Philosopher)
+
+普通に GearsAgdaでプロセスを記述する
+
+    pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
+    pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
+    eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
+
+    pickup_rfork p next = f_set (Phil.right p) (Phil.ptr p) ( λ f → pickup_lfork record p { right = f } next )
+    pickup_lfork p next = f_set (Phil.left p) (Phil.ptr p) ( λ f → eating record p { left = f } next )
+    eating p next = putdown_rfork p next
+
+--meta level での記述
+
+    Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
+    Phil_putdown_rfork_sub c next = next C_cas_int record c {
+        c_AtomicNat-API = record { impl = Phil.right phil ; value =  0 
+          ; fail = C_putdown_lfork ; next = C_putdown_lfork } }  where
+        phil : Phil
+        phil = Phil-API.impl ( Context.c_Phil-API c )
+
+メタレベルからは、Code と Context しか見えない
+
+    Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
+
+実際の接続は stub で行われる
+
+--meta level でのscheduler
+
+schedulerは Code と Context しか見ない
+
+共有は scheduler level のmetaGearで処理される
+
+-- Concurrency で証明したいこと
+
+    redBlackTree の transaction
+    redBlackTree の 大きさ制限 (メモリ管理)
+    redBlackTree の格納領域と、backup / commit
+
+--証明は実用的なの?
+
+Toy OS level での証明は可能になっている
+
+GearsAgda では、まだ、いろいろできてない
+
+invariant が決まれば、証明は割と機械的 (AI support?)
 
 
-------binary tree
+
 
--------invariant
+
 
--------tree
+
 
--------stac
 
--------replace
 
-------concurrency
+
 
-------meta gear
+
 
-------context
+
 
-------red black tree
 
-------red black tree invariant
-