Mercurial > hg > Members > Moririn

changeset 714:75da5f6de47e

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 Fri, 06 May 2022 10:11:31 +0900
parents 252e15bcbbb8
children 8f8f136f2162
files ModelChecking.agda
diffstat 1 files changed, 32 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/ModelChecking.agda	Thu May 05 21:02:07 2022 +0900
+++ b/ModelChecking.agda	Fri May 06 10:11:31 2022 +0900
@@ -20,11 +20,11 @@
 
 record AtomicNat : Set where
    field
-      anid : ℕ       -- memory pointer ( unique id of DataGear )
+      ptr : ℕ       -- memory pointer ( unique id of DataGear )
       value : ℕ
 
 init-AtomicNat : AtomicNat
-init-AtomicNat = record { anid = 0 ; value = 0 }
+init-AtomicNat = record { ptr = 0 ; value = 0 }
 
 --
 -- single process implemenation
@@ -35,11 +35,11 @@
 
 record Phil  : Set  where
    field 
-      pid : ℕ
+      ptr : ℕ
       left right : AtomicNat
 
 init-Phil : Phil
-init-Phil = record { pid = 0 ; left = init-AtomicNat ; right = init-AtomicNat }
+init-Phil = record { ptr = 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
@@ -48,17 +48,17 @@
 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.pid p) ( λ f → goto C_pickup_lfork record p { right = f } next )
+-- 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.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 )
+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
 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 : Phil
-run = pickup_rfork record { pid = 1 ; left = record { anid = 1 ; value = 0 } ; right = record { anid = 2 ; value = 0 } } $ λ p → p
+run = pickup_rfork record { ptr = 1 ; left = record { ptr = 1 ; value = 0 } ; right = record { ptr = 2 ; value = 0 } } $ λ p → p
 
 --
 -- Coda Gear
@@ -123,14 +123,14 @@
 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 } )
+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 )
 
 --
 -- 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.anid 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.value ai } ))
      ( λ bt → next ( Context.fail c ) c  ) -- segmentation fault ( null pointer )
      $ λ now bt → f_cas ai  (AtomicNat.value ai) now bt  where
     api : AtomicNat-API
@@ -147,13 +147,13 @@
 
 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.pid phil ; fail = C_putdown_lfork ; next = C_putdown_lfork } }  where
+    c_AtomicNat-API = record { impl = Phil.right phil ; value =  Phil.ptr phil ; 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.pid phil ; fail = C_thinking ; next = C_thinking } }  where
+    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_thinking ; next = C_thinking } }  where
     phil : Phil
     phil = Phil-API.impl ( Context.c_Phil-API c )
 
@@ -162,13 +162,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.pid 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_rfork ; next = C_pickup_lfork } }  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.pid phil ; fail = C_pickup_lfork ; next = C_eating } }  where
+    c_AtomicNat-API = record { impl = Phil.left phil ; value =  Phil.ptr phil ; fail = C_pickup_lfork ; next = C_eating } }  where
     phil : Phil
     phil = Phil-API.impl ( Context.c_Phil-API c )
 
@@ -187,9 +187,6 @@
 
 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 } ∷ [] ))) 
@@ -206,17 +203,25 @@
     ; 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 }  } } 
+init-Phil-1 : (ps : List Context) → (left right : AtomicNat ) → List Context
+init-Phil-1 ps left right = new-data (c1 ps) ( λ ptr → D_Phil (p ptr) )  $ λ c ptr → record c { c_Phil-API = record { next = C_thinking ; impl = p ptr }} ∷ ps where
+    p : ℕ → Phil
+    p ptr = record  init-Phil { ptr = ptr ; left = left ; right = right }  
+    c1 :  List Context → Context
+    c1 [] =  init-context
+    c1 (c2 ∷ ct) =  c2
 
-test : List Context
-test = step {!!} ( λ ps → ps ) 
+init-AtomicNat-n :  {n : Level} {t : Set n} → Context  → ( Context →  AtomicNat → t ) → t
+init-AtomicNat-n c1  next = new-data c1  ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) where
+    a : ℕ → AtomicNat
+    a ptr = record { ptr = ptr ; value = 0 }
 
-test1 : List Context
-test1 = step {!!}
-  $ λ ps → step ps $ λ ps → ps
+test : List Context 
+test = init-AtomicNat-n init-context $ λ c left → init-AtomicNat-n c $ λ c1 right → step (init-Phil-1 (c1 ∷ []) left right) (λ ps → ps )
+
+-- test1 : List Context
+-- test1 = step {!!}
+--   $ λ ps → step ps $ λ ps → ps
 
 -- loop exexution