Mercurial > hg > Members > Moririn
changeset 710:c588b77bc197
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 05 May 2022 14:23:49 +0900 |
| parents | 6a805c8c1e53 |
| children | 9be22bce3abd |
| files | ModelChecking.agda Todo.txt hoareBinaryTree.agda |
| diffstat | 3 files changed, 99 insertions(+), 62 deletions(-) [+] |
line wrap: on
line diff
--- a/ModelChecking.agda Tue May 03 18:34:47 2022 +0900 +++ b/ModelChecking.agda Thu May 05 14:23:49 2022 +0900 @@ -8,8 +8,8 @@ -- open import Data.Maybe.Properties open import Data.Empty open import Data.List -open import Data.Tree.Binary -open import Data.Product +-- open import Data.Tree.Binary +-- open import Data.Product open import Function as F hiding (const) open import Relation.Binary open import Relation.Binary.PropositionalEquality @@ -27,8 +27,8 @@ -- single process implemenation -- -set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t -set a v next = next record a { value = v } +f_set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t +f_set a v next = next record a { value = v } record Phils : Set where field @@ -42,11 +42,13 @@ putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t -pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → pickup_lfork record p { right = f } next ) -pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → eating record p { left = f } next ) +-- pickup_rfork p next = f_set (Phils.right p) (Phils.pid p) ( λ f → goto C_pickup_lfork record p { right = f } next ) + +pickup_rfork p next = f_set (Phils.right p) (Phils.pid p) ( λ f → pickup_lfork record p { right = f } next ) +pickup_lfork p next = f_set (Phils.left p) (Phils.pid p) ( λ f → eating record p { left = f } next ) eating p next = putdown_rfork p next -putdown_rfork p next = set (Phils.right p) 0 ( λ f → putdown_lfork record p { right = f } next ) -putdown_lfork p next = set (Phils.left p) 0 ( λ f → thinking record p { left = f } next ) +putdown_rfork p next = f_set (Phils.right p) 0 ( λ f → putdown_lfork record p { right = f } next ) +putdown_lfork p next = f_set (Phils.left p) 0 ( λ f → thinking record p { left = f } next ) thinking p next = next p run : Phils @@ -81,8 +83,15 @@ impl : Phils data Data : Set where - D_Phils : ℕ → Phils → Data - D_AtomicNat : ℕ → AtomicNat → Data + D_AtomicNat : AtomicNat → Data + D_Phils : Phils → Data + A_AtomicNat : AtomicNatAPI → Data + A_Phils : PhilsAPI → Data + +data Error : Set where + E_cas_fail : Error + +open import hoareBinaryTree record Context : Set where field @@ -90,53 +99,66 @@ fail : Code phil : PhilsAPI atomicNat : AtomicNatAPI - memory : Tree Data Data + mbase : ℕ + memory : bt Data error : Data fail_next : Code +alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t +alloc-data {n} {t} c next = next record c { mbase = ( suc ( Context.mbase c ) ) } ( suc ( Context.mbase c ) ) + +update-data : {n : Level} {t : Set n} → ( c : Context ) → ℕ → Data → ( Context → t ) → t +update-data c n x next = insertTree (Context.memory c) n x ( λ bt → next record c { memory = bt } ) + +f_cas : {n : Level} {t : Set n} → AtomicNat → (old now new : ℕ ) → ( Error → t) → ( AtomicNat → t ) → t +f_cas a old now new error next with <-cmp old now +... | tri≈ ¬a b ¬c = next record a { value = new } +... | tri< a₁ ¬b ¬c = error E_cas_fail +... | tri> ¬a ¬b _ = error E_cas_fail + +-- +-- second level stub +-- g_set : {n : Level} {t : Set n} → Context → AtomicNat → ( Code → Context → t ) → t -g_set {_} {t} c a next = f a ( AtomicNatAPI.value api ) +g_set {_} {t} c a next = f_set a ( AtomicNatAPI.value api ) $ λ a → next ( AtomicNatAPI.next api ) record c { atomicNat = record api { impl = a } } where api : AtomicNatAPI api = Context.atomicNat c - f : AtomicNat → ℕ → ( AtomicNat → t ) → t - f a n next = next record a { value = n } g_cas : {n : Level} {t : Set n} → Context → AtomicNat → ( Code → Context → t ) → t -g_cas {n} {t} c a next = f a ( AtomicNatAPI.old api )( AtomicNat.value a ) ( AtomicNatAPI.value api ) +g_cas {n} {t} c a next = f_cas a ( AtomicNatAPI.old api )( AtomicNat.value a ) ( AtomicNatAPI.value api ) ( λ e → next (Context.fail_next c) c ) $ λ a → next ( AtomicNatAPI.next api ) record c { atomicNat = record api { impl = a } } where api : AtomicNatAPI api = Context.atomicNat c - f : AtomicNat → (old now new : ℕ ) → ( AtomicNat → t ) → t - f a old now new next1 with <-cmp old now - ... | tri≈ ¬a b ¬c = next1 record a { value = new } - ... | tri< a₁ ¬b ¬c = next ( Context.fail c) c - ... | tri> ¬a ¬b _ = next ( Context.fail c) c g_putdown_rfork : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t g_putdown_rfork c p next = next C_set record c { - atomicNat = {!!} } + atomicNat = record (Context.atomicNat c) { impl = Phils.right p ; value = Phils.pid p ; old = AtomicNat.value (Phils.right p ) ; next = C_putdown_lfork } } g_putdown_lfork : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t g_putdown_lfork c p next = next C_set record c { - atomicNat = {!!} } + atomicNat = record (Context.atomicNat c) { impl = Phils.left p ; value = Phils.pid p ; old = AtomicNat.value (Phils.left p ) ; next = C_thinking } } g_thinking : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t g_thinking c p next = next C_pickup_rfork c g_pickup_rfork : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t g_pickup_rfork c p next = next C_set record c { - atomicNat = {!!} } + atomicNat = record (Context.atomicNat c) { impl = Phils.right p ; value = 0 ; old = AtomicNat.value (Phils.right p ) ; next = C_pickup_lfork } } g_pickup_lfork : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t g_pickup_lfork c p next = next C_set record c { - atomicNat = {!!} } + atomicNat = record (Context.atomicNat c) { impl = Phils.left p ; value = 0 ; old = AtomicNat.value (Phils.left p ) ; next = C_eating } } g_eating : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t g_eating c p next = next C_putdown_rfork c set_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t -set_stub p next = set {!!} {!!} ( λ ph → next {!!} ) +set_stub c next = f_cas (AtomicNatAPI.impl api) (AtomicNatAPI.old api) {!!} (AtomicNatAPI.value api) {!!} ( λ ai → next {!!} ) where + api : AtomicNatAPI + api = Context.atomicNat c + ai : {!!} + ai = updateTree {!!} {!!} {!!} {!!} {!!} putdown_rfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t putdown_rfork_stub p next = {!!} -- g_putdown_rfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )
--- a/Todo.txt Tue May 03 18:34:47 2022 +0900 +++ b/Todo.txt Thu May 05 14:23:49 2022 +0900 @@ -1,3 +1,10 @@ +Wed May 4 22:07:32 JST 2022 + + Context memory に DataGear を Binary Tree で入れる。List で良いのだが + Libaryの Data.Tree.Binary には insert はない ( まぁ、alloc / read / update くらいで map で書けるとか?) + 共有データは、memory に入れる + free はしない(?) + Sun May 1 15:04:57 JST 2022 Model checking
--- a/hoareBinaryTree.agda Tue May 03 18:34:47 2022 +0900 +++ b/hoareBinaryTree.agda Thu May 05 14:23:49 2022 +0900 @@ -90,6 +90,14 @@ insertTest3 = insertTree insertTest2 3 2 (λ x → x ) insertTest4 = insertTree insertTest3 2 2 (λ x → x ) -- this is wrong +updateTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (empty : bt A → t ) → (next : A → bt A → t ) → t +updateTree {_} {_} {A} {t} tree key value empty next = find-loop key tree ( tree ∷ [] ) + $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st (found? st) where + found? : List (bt A) → bt A → t + found? [] tree = empty tree -- can't happen + found? (leaf ∷ st) tree = empty tree + found? (node key value x x₁ ∷ st) tree = next value tree + open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where @@ -539,43 +547,43 @@ rd : (r1 : Index) → reduce r1 < reduce r ci : C -- data continuation -TerminatingLoopC : {l n : Level} {t : Set l} (Index : Set n ) → {C : Set n } → ( reduce : Index → ℕ) - → (r : Index) → (P : LoopTermination r C ) - → (loop : (r : Index) → LoopTermination {_} {_} {reduce} r C → (next : (r1 : Index) → LoopTermination r1 C → t ) → t) → t -TerminatingLoopC {_} {_} {t} Index {C} reduce r P loop with <-cmp 0 (reduce r) -... | tri≈ ¬a b ¬c = loop r P (λ r1 p1 → ⊥-elim (lemma3 b (LoopTermination.rd P r1))) -... | tri< a ¬b ¬c = loop r P (λ r1 p1 → TerminatingLoop1 (reduce r) r r1 (≤-step (LoopTermination.rd P r1)) p1 (LoopTermination.rd P r1)) where - TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → {!!} → reduce r1 < reduce r → t - TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 {!!} (λ r2 P1 → ⊥-elim (lemma5 n≤j (LoopTermination.rd P1 r2))) - TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) - ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt - ... | tri≈ ¬a b ¬c = loop r1 {!!} (λ r2 p2 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b {!!} ) p2 {!!} ) - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) - -record ReplCond {n : Level} {A : Set n} (C : ℕ → bt A → List (bt A) → Set n) : Set (Level.suc n) where - field - c1 : (key : ℕ) → (repl : bt A) → (stack : List (bt A)) → C key repl stack - -replaceP0 : {n m : Level} {A : Set n} {t : Set m} - → (key : ℕ) → (value : A) → ( repl : bt A) - → (stack : List (bt A)) - → {C : ℕ → (repl : bt A ) → List (bt A) → Set n} → C key repl stack → ReplCond C - → (next : ℕ → A → (repl : bt A) → (stack1 : List (bt A)) - → C key repl stack → length stack1 < length stack → t) - → (exit : (repl : bt A) → C key repl [] → t) → t -replaceP0 key value repl [] Pre _ next exit = exit repl {!!} -replaceP0 key value repl (leaf ∷ []) Pre _ next exit = exit (node key value leaf leaf) {!!} -replaceP0 key value repl (node key₁ value₁ left right ∷ []) Pre e next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) {!!} -... | tri≈ ¬a b ¬c = exit repl {!!} -... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) {!!} -replaceP0 {n} {_} {A} key value repl (leaf ∷ st@(tree1 ∷ st1)) Pre e next exit = next key value repl st {!!} ≤-refl -replaceP0 {n} {_} {A} key value repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre e next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl -... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st {!!} ≤-refl -... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st {!!} ≤-refl - - +-- TerminatingLoopC : {l n : Level} {t : Set l} (Index : Set n ) → {C : Set n } → ( reduce : Index → ℕ) +-- → (r : Index) → (P : LoopTermination r C ) +-- → (loop : (r : Index) → LoopTermination {_} {_} {reduce} r C → (next : (r1 : Index) → LoopTermination r1 C → t ) → t) → t +-- TerminatingLoopC {_} {_} {t} Index {C} reduce r P loop with <-cmp 0 (reduce r) +-- ... | tri≈ ¬a b ¬c = loop r P (λ r1 p1 → ⊥-elim (lemma3 b (LoopTermination.rd P r1))) +-- ... | tri< a ¬b ¬c = loop r P (λ r1 p1 → TerminatingLoop1 (reduce r) r r1 (≤-step (LoopTermination.rd P r1)) p1 (LoopTermination.rd P r1)) where +-- TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → {!!} → reduce r1 < reduce r → t +-- TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 {!!} (λ r2 P1 → ⊥-elim (lemma5 n≤j (LoopTermination.rd P1 r2))) +-- TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) +-- ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt +-- ... | tri≈ ¬a b ¬c = loop r1 {!!} (λ r2 p2 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b {!!} ) p2 {!!} ) +-- ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) +-- +-- record ReplCond {n : Level} {A : Set n} (C : ℕ → bt A → List (bt A) → Set n) : Set (Level.suc n) where +-- field +-- c1 : (key : ℕ) → (repl : bt A) → (stack : List (bt A)) → C key repl stack +-- +-- replaceP0 : {n m : Level} {A : Set n} {t : Set m} +-- → (key : ℕ) → (value : A) → ( repl : bt A) +-- → (stack : List (bt A)) +-- → {C : ℕ → (repl : bt A ) → List (bt A) → Set n} → C key repl stack → ReplCond C +-- → (next : ℕ → A → (repl : bt A) → (stack1 : List (bt A)) +-- → C key repl stack → length stack1 < length stack → t) +-- → (exit : (repl : bt A) → C key repl [] → t) → t +-- replaceP0 key value repl [] Pre _ next exit = exit repl {!!} +-- replaceP0 key value repl (leaf ∷ []) Pre _ next exit = exit (node key value leaf leaf) {!!} +-- replaceP0 key value repl (node key₁ value₁ left right ∷ []) Pre e next exit with <-cmp key key₁ +-- ... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) {!!} +-- ... | tri≈ ¬a b ¬c = exit repl {!!} +-- ... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) {!!} +-- replaceP0 {n} {_} {A} key value repl (leaf ∷ st@(tree1 ∷ st1)) Pre e next exit = next key value repl st {!!} ≤-refl +-- replaceP0 {n} {_} {A} key value repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre e next exit with <-cmp key key₁ +-- ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl +-- ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st {!!} ≤-refl +-- ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st {!!} ≤-refl +-- +-- open _∧_ RTtoTI0 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree