Mercurial > hg > Gears > GearsAgda

changeset 713:252e15bcbbb8

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 21:02:07 +0900
parents 64a86fde1f90
children 75da5f6de47e
files ModelChecking.agda
diffstat 1 files changed, 56 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/ModelChecking.agda	Thu May 05 19:23:26 2022 +0900
+++ b/ModelChecking.agda	Thu May 05 21:02:07 2022 +0900
@@ -23,6 +23,9 @@
       anid : ℕ       -- memory pointer ( unique id of DataGear )
       value : ℕ
 
+init-AtomicNat : AtomicNat
+init-AtomicNat = record { anid = 0 ; value = 0 }
+
 --
 -- single process implemenation
 --
@@ -35,6 +38,9 @@
       pid : ℕ
       left right : AtomicNat
 
+init-Phil : Phil
+init-Phil = record { pid = 0 ; left = init-AtomicNat ; right = init-AtomicNat }
+
 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
@@ -59,6 +65,7 @@
 --
 
 data Code : Set  where
+   C_nop : Code
    C_cas_int : Code
    C_putdown_rfork : Code 
    C_putdown_lfork : Code 
@@ -68,31 +75,34 @@
    C_eating : Code 
 
 --
--- all possible arguments in APIs
+-- all possible arguments in -APIs
 --
-record AtomicNatAPI : Set where
+record AtomicNat-API : Set where
    field
       next : Code
       fail : Code
       value : ℕ
       impl : AtomicNat
 
-record PhilAPI : Set  where
+record Phil-API : Set  where
    field 
       next : Code
       impl : Phil
 
+data Error : Set where
+   E_panic : Error
+   E_cas_fail : Error
+
 --
 -- Data Gear
 --
 data Data : Set where
    D_AtomicNat :  AtomicNat → Data
    D_Phil :      Phil → Data
+   D_Error :      Error → Data
 
-   -- A_AtomicNat :  AtomicNatAPI → Data
-   -- A_Phil :      PhilAPI → Data
-
-data Error : Set where E_cas_fail : Error
+   -- A_AtomicNat :  AtomicNat-API → Data
+   -- A_Phil :      Phil-API → Data
 
 open import hoareBinaryTree
 
@@ -101,9 +111,9 @@
       next :      Code 
       fail :      Code
 
-      --  API list (frame in Gears Agda )
-      c_PhilAPI :     PhilAPI
-      c_AtomicNatAPI : AtomicNatAPI
+      --  -API list (frame in Gears Agda )
+      c_Phil-API :     Phil-API
+      c_AtomicNat-API : AtomicNat-API
 
       mbase :     ℕ
       memory :    bt Data
@@ -123,49 +133,50 @@
 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.c_AtomicNatAPI c
+    api : AtomicNat-API
+    api = Context.c_AtomicNat-API c
     ai : AtomicNat
-    ai = AtomicNatAPI.impl api
+    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 (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
+    ... | tri≈ ¬a b ¬c  = next (AtomicNat-API.fail api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = a } }  ) -- update memory
+    ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c
+    ... | tri> ¬a ¬b _  = next (AtomicNat-API.fail api) c
     f_cas a old _ bt    = next ( Context.fail c ) c       -- type error
 
 
 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
+    c_AtomicNat-API = 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 )
+    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_AtomicNatAPI = record { impl = Phil.left phil ; value =  Phil.pid phil ; fail = C_thinking ; next = C_thinking } }  where
+    c_AtomicNat-API = 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 )
+    phil = Phil-API.impl ( Context.c_Phil-API c )
 
 Phil_thiking : {n : Level} {t : Set n} → Context  → ( Code → Context → t ) → t
 Phil_thiking c next = next C_pickup_rfork c  
 
 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
+    c_AtomicNat-API = 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 )
+    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_AtomicNatAPI = record { impl = Phil.left phil ; value =  Phil.pid phil ; fail = C_pickup_lfork ; next = C_eating } }  where
+    c_AtomicNat-API = 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 )
+    phil = Phil-API.impl ( Context.c_Phil-API c )
 
 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_nop  = λ c  next  → next C_nop c
 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
@@ -176,12 +187,32 @@
 
 open Context
 
+new :   {n : Level} {t : Set n} →  ( c : Context ) → Data → ( Context → ℕ → t ) → t
+new c1 d next =  alloc-data c1 ( λ c1 n → update-data c1  n d (λ c2 → next c2 n ))
+
 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 } ∷ [] ))) 
 
+init-context : Context
+init-context = record {
+      next = C_nop
+    ; fail = C_nop
+    ; c_Phil-API = record { next = C_nop ; impl = init-Phil } 
+    ; c_AtomicNat-API = record { next = C_nop ; fail = C_nop ; value = 0 ; impl = init-AtomicNat } 
+    ; mbase = 0
+    ; memory = leaf
+    ; error = D_Error E_panic
+    ; fail_next = C_nop
+  }
+
+init-phil-1 : (pid : ℕ ) → (left right : AtomicNat ) → List Context
+init-phil-1 pid left right = c ∷ [] where
+   c : Context
+   c = record init-context { c_Phil-API = record { next = C_thinking ; impl = record  init-Phil { pid = pid ; left = left ; right = right }  } } 
+
 test : List Context
-test = step {!!} ( λ ps → ps )
+test = step {!!} ( λ ps → ps ) 
 
 test1 : List Context
 test1 = step {!!}