Mercurial > hg > Gears > GearsAgda

changeset 711:9be22bce3abd

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 Thu, 05 May 2022 18:37:10 +0900
parents c588b77bc197
children 64a86fde1f90
files ModelChecking.agda
diffstat 1 files changed, 40 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/ModelChecking.agda	Thu May 05 14:23:49 2022 +0900
+++ b/ModelChecking.agda	Thu May 05 18:37:10 2022 +0900
@@ -20,7 +20,7 @@
 
 record AtomicNat : Set where
    field
-      anid : ℕ
+      anid : ℕ       -- memory pointer ( unique id of DataGear )
       value : ℕ
 
 --
@@ -55,11 +55,11 @@
 run = pickup_rfork record { pid = 1 ; left = record { anid = 1 ; value = 0 } ; right = record { anid = 2 ; value = 0 } } $ λ p → p
 
 --
--- goto version
+-- Coda Gear
 --
 
 data Code : Set  where
-   C_set : Code
+   C_cas_int : Code
    C_putdown_rfork : Code 
    C_putdown_lfork : Code 
    C_thinking : Code 
@@ -73,8 +73,8 @@
 record AtomicNatAPI : Set where
    field
       next : Code
+      fail : Code
       value : ℕ
-      old : ℕ
       impl : AtomicNat
 
 record PhilsAPI : Set  where
@@ -82,14 +82,17 @@
       next : Code
       impl : Phils
 
+--
+-- Data Gear
+--
 data Data : Set where
    D_AtomicNat :  AtomicNat → Data
    D_Phils :      Phils → Data
-   A_AtomicNat :  AtomicNatAPI → Data
-   A_Phils :      PhilsAPI → Data
 
-data Error : Set where
-   E_cas_fail : Error
+   -- A_AtomicNat :  AtomicNatAPI → Data
+   -- A_Phils :      PhilsAPI → Data
+
+data Error : Set where E_cas_fail : Error
 
 open import hoareBinaryTree
 
@@ -97,8 +100,11 @@
    field
       next :      Code 
       fail :      Code
+
+      --  API list (frame in Gears Agda )
       phil :      PhilsAPI
       atomicNat : AtomicNatAPI
+
       mbase :     ℕ
       memory :    bt Data
       error :     Data
@@ -110,55 +116,50 @@
 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_set a ( AtomicNatAPI.value api   ) 
-         $ λ a → next ( AtomicNatAPI.next api  ) record c { atomicNat = record api   { impl = a } }   where
+g_cas : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
+g_cas {_} {t} c next = updateTree (Context.memory c) (AtomicNat.anid ai) ( D_AtomicNat (record ai { value = AtomicNat.value ai } ))
+     ( λ bt → next ( Context.fail c ) c  ) -- segmentation fault ( null pointer )
+     $ λ now bt → f_cas ai  (AtomicNat.value ai) now bt  where
     api : AtomicNatAPI
     api = Context.atomicNat c
+    ai : AtomicNat
+    ai = AtomicNatAPI.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 (AtomicNatAPI.fail api) ( record c { memory = bt ; atomicNat = record api { impl = a } }  ) -- update memory
+    ... | tri< a₁ ¬b ¬c = next (AtomicNatAPI.fail api) c
+    ... | tri> ¬a ¬b _  = next (AtomicNatAPI.fail api) c
+    f_cas a old _ bt    = next ( Context.fail c ) c       -- type error
 
-g_cas : {n : Level} {t : Set n} → Context  → AtomicNat → ( Code → Context → t ) → t
-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
 
+-- g_putdown_rfork : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
 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 { 
+g_putdown_rfork c p next = next C_cas_int record c { 
     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 { 
+g_putdown_lfork c p next = next C_cas_int record c { 
     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 {
+g_pickup_rfork c p next = next C_cas_int record c {
     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 {
+g_pickup_lfork c p next = next C_cas_int record c {
     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 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 {!!} {!!} {!!} {!!} {!!}
+set_stub c next = {!!} -- gset c (Context.atomicNat c) next
 
 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 } )
@@ -178,14 +179,14 @@
 eating_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
 eating_stub p next = {!!} -- g_pickup_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_rfork } )
 
-code_table :  {n : Level} {t : Set n} → Code → Context → ( Context → t) → t
-code_table C_set  = set_stub
-code_table C_putdown_rfork = putdown_rfork_stub
-code_table C_putdown_lfork = putdown_lfork_stub
-code_table C_thinking = thinking_stub
-code_table C_pickup_rfork = pickup_rfork_stub
-code_table C_pickup_lfork = pickup_lfork_stub
-code_table C_eating = eating_stub
+code_table :  {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t
+code_table C_cas_int  = g_cas
+code_table C_putdown_rfork = ? -- putdown_rfork_stub
+code_table C_putdown_lfork = ? -- putdown_lfork_stub
+code_table C_thinking = ? -- thinking_stub
+code_table C_pickup_rfork = ? -- pickup_rfork_stub
+code_table C_pickup_lfork = ? -- pickup_lfork_stub
+code_table C_eating = ? -- eating_stub
 
 open Context