Mercurial > hg > Gears > GearsAgda

changeset 712:64a86fde1f90

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 19:23:26 +0900
parents 9be22bce3abd
children 252e15bcbbb8
files ModelChecking.agda
diffstat 1 files changed, 55 insertions(+), 69 deletions(-) [+]
line wrap: on
line diff
--- a/ModelChecking.agda	Thu May 05 18:37:10 2022 +0900
+++ b/ModelChecking.agda	Thu May 05 19:23:26 2022 +0900
@@ -30,28 +30,28 @@
 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
+record Phil  : Set  where
    field 
       pid : ℕ
       left right : AtomicNat
 
-pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
+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
+putdown_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
+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 (Phils.right p) (Phils.pid p) ( λ f → goto C_pickup_lfork record p { right = f } next )
+-- pickup_rfork p next = f_set (Phil.right p) (Phil.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 )
+pickup_rfork p next = f_set (Phil.right p) (Phil.pid p) ( λ f → pickup_lfork record p { right = f } next )
+pickup_lfork p next = f_set (Phil.left p) (Phil.pid p) ( λ f → eating record p { left = f } next )
 eating p next = putdown_rfork p 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 )
+putdown_rfork p next = f_set (Phil.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
+putdown_lfork p next = f_set (Phil.left p) 0 ( λ f → thinking record p { left = f } next )
 thinking p next = next p
 
-run : Phils
+run : Phil
 run = pickup_rfork record { pid = 1 ; left = record { anid = 1 ; value = 0 } ; right = record { anid = 2 ; value = 0 } } $ λ p → p
 
 --
@@ -77,20 +77,20 @@
       value : ℕ
       impl : AtomicNat
 
-record PhilsAPI : Set  where
+record PhilAPI : Set  where
    field 
       next : Code
-      impl : Phils
+      impl : Phil
 
 --
 -- Data Gear
 --
 data Data : Set where
    D_AtomicNat :  AtomicNat → Data
-   D_Phils :      Phils → Data
+   D_Phil :      Phil → Data
 
    -- A_AtomicNat :  AtomicNatAPI → Data
-   -- A_Phils :      PhilsAPI → Data
+   -- A_Phil :      PhilAPI → Data
 
 data Error : Set where E_cas_fail : Error
 
@@ -102,8 +102,8 @@
       fail :      Code
 
       --  API list (frame in Gears Agda )
-      phil :      PhilsAPI
-      atomicNat : AtomicNatAPI
+      c_PhilAPI :     PhilAPI
+      c_AtomicNatAPI : AtomicNatAPI
 
       mbase :     ℕ
       memory :    bt Data
@@ -119,80 +119,66 @@
 --
 -- second level stub
 --
-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 } ))
+AtomicInt_cas_stub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
+AtomicInt_cas_stub {_} {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
+    api = Context.c_AtomicNatAPI 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) ( record c { memory = bt ; c_AtomicNatAPI = 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_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_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_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 } }
+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_AtomicNatAPI = record { impl = Phil.right phil ; value =  Phil.pid phil ; fail = C_putdown_lfork ; next = C_putdown_lfork } }  where
+    phil : Phil
+    phil = PhilAPI.impl ( Context.c_PhilAPI c )
 
-g_thinking : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
-g_thinking c p next = next C_pickup_rfork 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_AtomicNatAPI = record { impl = Phil.left phil ; value =  Phil.pid phil ; fail = C_thinking ; next = C_thinking } }  where
+    phil : Phil
+    phil = PhilAPI.impl ( Context.c_PhilAPI c )
 
-g_pickup_rfork : {n : Level} {t : Set n} → Context  → Phils → ( Code → Context → t ) → t
-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_cas_int record c {
-    atomicNat = record (Context.atomicNat c) { impl = Phils.left p ; value = 0 ; old = AtomicNat.value (Phils.left p ) ; next = C_eating } }
+Phil_thiking : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
+Phil_thiking c next = next C_pickup_rfork c  
 
-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 = {!!} -- 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 } )
-
-putdown_lfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
-putdown_lfork_stub p next = {!!} -- g_putdown_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_thinking } )
+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_AtomicNatAPI = record { impl = Phil.left phil ; value =  Phil.pid phil ; fail = C_pickup_rfork ; next = C_pickup_lfork } }  where
+    phil : Phil
+    phil = PhilAPI.impl ( Context.c_PhilAPI c )
 
-thinking_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
-thinking_stub p next = {!!} -- g_thinking ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_pickup_rfork } )
-
-pickup_rfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
-pickup_rfork_stub p next = {!!} -- g_pickup_rfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_pickup_lfork } )
+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_AtomicNatAPI = record { impl = Phil.left phil ; value =  Phil.pid phil ; fail = C_pickup_lfork ; next = C_eating } }  where
+    phil : Phil
+    phil = PhilAPI.impl ( Context.c_PhilAPI c )
 
-pickup_lfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
-pickup_lfork_stub p next = {!!} -- g_pickup_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_eating } )
-
-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 } )
+Phil_eating_sub : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
+Phil_eating_sub c next =  next C_putdown_rfork c 
 
 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
+code_table C_cas_int  = AtomicInt_cas_stub
+code_table C_putdown_rfork = Phil_putdown_rfork_sub
+code_table C_putdown_lfork = Phil_putdown_lfork_sub
+code_table C_thinking = Phil_thiking
+code_table C_pickup_rfork = Phil_pickup_lfork_sub
+code_table C_pickup_lfork = Phil_pickup_rfork_sub
+code_table C_eating = Phil_eating_sub
 
 open Context
 
 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 {!!} p ( λ np → next0 (ps ++ ( np ∷ [] ) )) 
+step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (ps ++ ( record np { next = code } ∷ [] ))) 
 
 test : List Context
 test = step {!!} ( λ ps → ps )