# HG changeset patch # User Shinji KONO # Date 1683962051 -32400 # Node ID cedf88ea18b964d59a022446897fd96d8740672b # Parent 9e85fa1cc6a815b2050498933e511ae8c3200c5e ... diff -r 9e85fa1cc6a8 -r cedf88ea18b9 presen.ind --- 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 -