Gears/GearsAgda: ModelChecking.agda comparison

comparison ModelChecking.agda @ 721:2abfce56523a

init 5 phils done without infinite loop

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 22 May 2022 19:07:20 +0900
parents	e9d781c38629
children	b088fa199d3d

comparison

equal deleted inserted replaced

-:e9d781c38629
+:2abfce56523a
 E_cas_fail : Error
 --
 -- Data Gear
 --
+--      waiting / pointer / available
+--
 data Data : Set where
 -- D_AtomicNat :  AtomicNat → ℕ → Data
 D_AtomicNat :  AtomicNat → Data
 D_Phil :      Phil → Data
 D_Error :      Error → Data
 ... | 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 bt    = next ( Context.fail c ) c       -- type error / panic
+-- putdown_rfork : Phil → (? → t) → t
+-- putdown_rfork p next = goto p->lfork->cas( 0 , putdown_lfork, putdown_lfork ) , next
--- 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 =  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
 init-AtomicNat1 :  {n : Level} {t : Set n} → Context  → ( Context →  AtomicNat → t ) → t
 init-AtomicNat1 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 }
-init-Phil-1 : (ps : List Context) → (left right : AtomicNat ) → List Context
+init-Phil-1 : (c1 : Context) → 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
+init-Phil-1 c1 = record c1 { memory = mem2 $ mem1 $ mem ; mbase = n + 3 } where
-p : ℕ → Phil
+n : ℕ
-p ptr = record  init-Phil { ptr = ptr ; left = left ; right = right }
+n = Context.mbase c1
-c1 :  List Context → Context
+left  = record { ptr = suc n ; value = 0}
-c1 [] =  init-context
+right = record { ptr = suc (suc n) ; value = 0}
-c1 (c2 ∷ ct) =  c2
+mem : bt Data
+mem = insertTree ( Context.memory c1) (suc n) (D_AtomicNat left)
-test-j0 : {n : Level} {t : Set n} → Context → (Context → AtomicNat → t) → t
+$ λ t →  t
-test-j0 c next = init-AtomicNat1 c next
+mem1 : bt Data → bt Data
+mem1 t = insertTree t (suc (suc n)) (D_AtomicNat right )
-test-j2 : AtomicNat
+$ λ t →  t
-test-j2 = test-j0 init-context (λ c f → f )
+mem2 : bt Data → bt Data
+mem2 t = insertTree t (n + 3) (D_Phil record { ptr = n + 3 ; left = left ; right = right })
-test-i1 : Context → Context
+$ λ t →  t
-test-i1 c = init-AtomicNat1 c $ λ c f → c
+test-i0 : bt Data
-test-i0 : Context
+test-i0 =  Context.memory (init-Phil-1 init-context)
-test-i0 = test-i1 init-context
+make-phil : ℕ → Context
-test-i2 : Context
+make-phil zero = init-context
-test-i2 = test-i1 test-i0
+make-phil (suc n) = init-Phil-1 ( make-phil n )
-test20 : bt (Data)
+test-i5 : bt Data
-test20 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
+test-i5 =  Context.memory (make-phil 5)
-$ λ c n → Context.memory c
--- infinite loop
-test21 : bt (Data)
-test21 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
-$ λ c n → insertTree ( Context.memory c)  2 (D_AtomicNat record { ptr = 2 ; value = 0 }) $ λ t → t
--- Ok
-test212  : bt Data
-test212 = insertTree   (node 1 (D_AtomicNat record { ptr = 1 ; value = 0 }) leaf leaf  ) 2 (D_AtomicNat record { ptr = 2 ; value = 0 })
-$ λ t → t
-open _∧_
-test213 : bt Data
-test213 = insertTree (test20)  2 (D_AtomicNat record { ptr = 2 ; value = 0 }) $ λ t → 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))
-$ λ bt → record c { memory = bt } ∷ [] where
-a : ℕ → AtomicNat
-a ptr = record { ptr = ptr ; value = 0 }
-test-newdata : bt Data
-test-newdata = new-data  init-context ( λ ptr → D_AtomicNat (a ptr) ) $ λ c n → Context.memory c where
-a : ℕ → AtomicNat
-a ptr = record { ptr = ptr ; value = 0 }
-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
-test01-tree : bt Data
-test01-tree = node 1 (D_AtomicNat record { ptr = 1 ; value = 0 } ) leaf leaf
-test01-assert : test01-tree ≡ test01
-test01-assert = refl
-tail1 :  Maybe (List (bt Data)) →  Maybe (List (bt Data))
-tail1 (just x) = tail x
-tail1 nothing = nothing
-test22 : Context
-test22 = init-AtomicNat1 init-context $ λ c left → init-AtomicNat1 c $ λ c1 right → c1
-test : List Context
-test = init-AtomicNat1 init-context $ λ c left → init-AtomicNat1 c $ λ c1 right → init-Phil-1 (c1 ∷ []) left right
-test1 : List Context
-test1 = init-AtomicNat1 init-context $ λ c left → init-AtomicNat1 c $ λ c1 right → step (init-Phil-1 (c1 ∷ []) left right) (λ ps → ps )
 -- loop exexution
 -- concurrnt execution

Mercurial > hg > Gears > GearsAgda

comparison ModelChecking.agda @ 721:2abfce56523a