Mercurial > hg > Members > Moririn

changeset 716:a36147bb596d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix context
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 10 May 2022 18:44:46 +0900
parents 8f8f136f2162
children 52938e8a54a2
files ModelChecking.agda hoareBinaryTree.agda
diffstat 2 files changed, 52 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/ModelChecking.agda	Sat May 07 20:01:07 2022 +0900
+++ b/ModelChecking.agda	Tue May 10 18:44:46 2022 +0900
@@ -48,8 +48,6 @@
 putdown_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
 thinking : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
 
--- pickup_rfork p next = f_set (Phil.right p) (Phil.ptr p) ( λ f → goto C_pickup_lfork record p { right = f } next )
-
 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
@@ -58,7 +56,7 @@
 thinking p next = next p
 
 run : Phil
-run = pickup_rfork record { ptr = 1 ; left = record { ptr = 1 ; value = 0 } ; right = record { ptr = 2 ; value = 0 } } $ λ p → p
+run = pickup_rfork record { ptr = 1 ; left = record { ptr = 2 ; value = 0 } ; right = record { ptr = 3 ; value = 0 } } $ λ p → p
 
 --
 -- Coda Gear
@@ -125,39 +123,43 @@
       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 ) ) 
+alloc-data {n} {t} c next = next record c { mbase = mnext } mnext  where
+     mnext = suc ( Context.mbase c )
 
 new-data : {n : Level} {t : Set n} → ( c : Context ) → (ℕ → Data ) → ( Context → ℕ → t ) → t
-new-data  c x next  = alloc-data c $ λ c n → insertTree (Context.memory c) n (x n) ( λ bt → next record c { memory = bt } n )
+new-data  c x next  = alloc-data c $ λ c1 n → insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n )
 
 --
 -- second level stub
 --
 AtomicInt_cas_stub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
-AtomicInt_cas_stub {_} {t} c next = updateTree (Context.memory c) (AtomicNat.ptr ai) ( D_AtomicNat (record ai { value = AtomicNat.value ai } ))
+AtomicInt_cas_stub {_} {t} c next = updateTree (Context.memory c) (AtomicNat.ptr ai) ( D_AtomicNat (record ai { value = AtomicNat-API.value api } ))
      ( λ bt → next ( Context.fail c ) c  ) -- segmentation fault ( null pointer )
-     $ λ now bt → f_cas ai  (AtomicNat.value ai) now bt  where
+     $ λ prev bt → f_cas prev bt  where
     api : AtomicNat-API
     api = Context.c_AtomicNat-API c
     ai : AtomicNat
     ai = AtomicNat-API.impl api
-    f_cas : AtomicNat → (old : ℕ ) → Data  → bt Data  → t
-    f_cas a old (D_AtomicNat now) bt with <-cmp old ( AtomicNat.value now )
-    ... | tri≈ ¬a b ¬c  = next (AtomicNat-API.fail api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = a } }  ) -- update memory
+    f_cas : Data  → bt Data  → t
+    f_cas (D_AtomicNat prev) bt with <-cmp ( AtomicNat.value  ai ) ( AtomicNat.value prev )
+    ... | tri≈ ¬a b ¬c  = next (AtomicNat-API.next api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = prev } }  ) -- update memory
     ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c   --- cleaer API
     ... | tri> ¬a ¬b _  = next (AtomicNat-API.fail api) c
-    f_cas a old _ bt    = next ( Context.fail c ) c       -- type error
+    f_cas a bt    = next ( Context.fail c ) c       -- type error / panic
+
 
 
+-- putdown_rfork p next = f_set (Phil.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
+--               goto p->cas( 0 , putdown_lfork )
 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 =  Phil.ptr phil ; fail = C_putdown_lfork ; next = C_putdown_lfork } }  where
+    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 )
 
 Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
 Phil_putdown_lfork_sub c next = next C_cas_int record c { 
-    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_thinking ; next = C_thinking } }  where
+    c_AtomicNat-API = record { impl = Phil.left phil ; value =  0 ; fail = C_thinking ; next = C_thinking } }  where
     phil : Phil
     phil = Phil-API.impl ( Context.c_Phil-API c )
 
@@ -166,13 +168,13 @@
 
 Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
 Phil_pickup_lfork_sub c next = next C_cas_int record c { 
-    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_pickup_rfork ; next = C_pickup_lfork } }  where
+    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_pickup_lfork ; next = C_pickup_rfork } }  where
     phil : Phil
     phil = Phil-API.impl ( Context.c_Phil-API c )
 
 Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
 Phil_pickup_rfork_sub c next = next C_cas_int record c { 
-    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_pickup_lfork ; next = C_eating } }  where
+    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_pickup_rfork ; next = C_eating } }  where
     phil : Phil
     phil = Phil-API.impl ( Context.c_Phil-API c )
 
@@ -193,7 +195,10 @@
 
 step : {n : Level} {t : Set n} → List Context → (List Context → t) → t
 step {n} {t} [] next0 = next0 []
-step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (ps ++ ( record np { next = code } ∷ [] ))) 
+step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (update-context ps np ++ ( record np { next = code } ∷ [] )))  where
+    update-context : List Context → Context  → List Context 
+    update-context [] _ = []
+    update-context (c1 ∷ t) np = record c1 { memory = Context.memory np  ; mbase = Context.mbase np } ∷ t
 
 init-context : Context
 init-context = record {
@@ -228,6 +233,13 @@
 test0 : List Context 
 test0 = init-AtomicNat1 init-context $ λ c left → c ∷ []
 
+test01 : bt Data 
+test01  = alloc-data init-context  $ λ c1 n → insertTree (Context.memory c1) n (D_AtomicNat (a n)) ( λ bt → next1 bt record c1 { memory = bt } n ) where
+    a : ℕ → AtomicNat
+    a ptr = record { ptr = ptr ; value = 0 }
+    next1 :  bt Data → Context  → ℕ → bt Data
+    next1 t c1 n = t
+
 test2 : List Context 
 test2 = init-AtomicNat1 init-context $  λ c left → alloc-data c
  $ λ c n → insertTree (Context.memory c) n  (D_AtomicNat (a n))
@@ -235,12 +247,17 @@
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
 
-test21 : List (bt Data )
-test21 = init-AtomicNat1 init-context $  λ c left → alloc-data c
- $ λ c n → find-loop n (Context.memory c) ( (Context.memory c) ∷ [] ) $ λ t st → st where
+test21 : ℕ ∧ Maybe (List (bt Data))
+test21 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
+ $ λ c n → find n (Context.memory c) (Context.memory c ∷ [])  (λ d st → ⟪ n , just st ⟫ ) $ λ t st → ⟪ n , nothing ⟫  where
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
 
+test22 : ℕ ∧ (Maybe (List (bt Data)))
+test22 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
+ $ λ c n → find n (Context.memory c) (Context.memory c ∷ []) (λ t st → find n t st (λ t st → ⟪ 1 , tail st ⟫) (λ t st → ⟪ 2 , just st ⟫))  $ λ t st → ⟪ 0 , tail st ⟫  where
+    a : ℕ → AtomicNat
+    a ptr = record { ptr = ptr ; value = 0 }
 
 test : List Context 
 test = init-AtomicNat1 init-context $ λ c left → init-AtomicNat1 c $ λ c1 right → init-Phil-1 (c1 ∷ []) left right
--- a/hoareBinaryTree.agda	Sat May 07 20:01:07 2022 +0900
+++ b/hoareBinaryTree.agda	Tue May 10 18:44:46 2022 +0900
@@ -45,19 +45,28 @@
 bt-depth leaf = 0
 bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ ))
 
-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
+find' : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
            → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
-find key leaf st _ exit = exit leaf st
+find' key leaf st _ exit = exit leaf st
+find' key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
+find' key n st _ exit | tri≈ ¬a b ¬c = exit n st
+find' key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
+find' key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
+
+find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
+           → (next : (tree1 : bt A) → (stack : List (bt A)) → t)
+           → (exit : (tree1 : bt A) → (stack : List (bt A)) → t) → t
+find key leaf st _ exit = exit leaf st 
 find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
-find key n st _ exit | tri≈ ¬a b ¬c = exit n st
-find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
-find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
+find key n st _ exit | tri≈ ¬a refl ¬c = exit n st 
+find {n} {_} {A} key (node key₁ v1 tree tree₁) st  next _ | tri< a ¬b ¬c = next tree (tree ∷ st) 
+find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) 
 
 {-# TERMINATING #-}
 find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A)  → (exit : bt A → List (bt A) → t) → t
 find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where
     find-loop1 : bt A → List (bt A) → t
-    find-loop1 tree st = find key tree st find-loop1  exit
+    find-loop1 tree st = find key tree st find-loop1 exit
 
 replaceNode : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → (bt A → t) → t
 replaceNode k v1 leaf next = next (node k v1 leaf leaf)
@@ -70,7 +79,7 @@
 ... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) 
 ... | tri≈ ¬a b ¬c = exit (node key₁ value  left right ) 
 ... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) 
-replace key value repl (leaf ∷ st) next exit = next key value repl st    
+replace key value repl (leaf ∷ st) next exit = next key value repl st
 replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st