Mercurial > hg > Gears > GearsAgda

changeset 709:6a805c8c1e53

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 Tue, 03 May 2022 18:34:47 +0900
parents 4761b08c4bd6
children c588b77bc197
files ModelChecking.agda Todo.txt
diffstat 2 files changed, 143 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/ModelChecking.agda	Tue Apr 19 19:39:29 2022 +0900
+++ b/ModelChecking.agda	Tue May 03 18:34:47 2022 +0900
@@ -8,6 +8,7 @@
 -- open import Data.Maybe.Properties
 open import Data.Empty
 open import Data.List
+open import Data.Tree.Binary
 open import Data.Product
 open import Function as F hiding (const)
 open import Relation.Binary
@@ -19,33 +20,41 @@
 
 record AtomicNat : Set where
    field
+      anid : ℕ
       value : ℕ
 
+--
+-- single process implemenation
+--
+
 set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
-set a v next = next record { value = v }
+set a v next = next record a { value = v }
 
 record Phils  : 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_rfork p next = set (Phils.right p) 0 ( λ f → next record p { right = f } )
-
 putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-putdown_lfork p next = set (Phils.left p) 0 ( λ f → next record p { left = f } )
-
 thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-thinking p next = next p 
 
-pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → next record p { right = f } )
+pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → pickup_lfork record p { right = f } next )
+pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → eating record p { left = f } next )
+eating p next = putdown_rfork p next
+putdown_rfork p next = set (Phils.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
+putdown_lfork p next = set (Phils.left p) 0 ( λ f → thinking record p { left = f } next )
+thinking p next = next p
 
-pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } )
+run : Phils
+run = pickup_rfork record { pid = 1 ; left = record { anid = 1 ; value = 0 } ; right = record { anid = 2 ; value = 0 } } $ λ p → p
 
-eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
-eating p next = next  p 
+--
+-- goto version
+--
 
 data Code : Set  where
    C_set : Code
@@ -56,37 +65,117 @@
    C_pickup_lfork : Code 
    C_eating : Code 
 
-record Process : Set  where
+--
+-- all possible arguments in APIs
+--
+record AtomicNatAPI : Set where
    field
-      phil : Phils
-      next_code : Code 
+      next : Code
+      value : ℕ
+      old : ℕ
+      impl : AtomicNat
+
+record PhilsAPI : Set  where
+   field 
+      next : Code
+      impl : Phils
+
+data Data : Set where
+   D_Phils : ℕ → Phils → Data
+   D_AtomicNat : ℕ → AtomicNat → Data
+
+record Context  : Set  where
+   field
+      next :      Code 
+      fail :      Code
+      phil :      PhilsAPI
+      atomicNat : AtomicNatAPI
+      memory :    Tree Data Data
+      error :     Data
+      fail_next :      Code
+
+g_set : {n : Level} {t : Set n} → Context  → AtomicNat → ( Code → Context → t ) → t
+g_set {_} {t} c a next = f a ( AtomicNatAPI.value api   )
+         $ λ a → next ( AtomicNatAPI.next api  ) record c { atomicNat = record api   { impl = a } }   where
+    api : AtomicNatAPI
+    api = Context.atomicNat c
+    f : AtomicNat → ℕ  → ( AtomicNat → t ) → t
+    f a n next = next record a { value = n }
 
-putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
-putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )
+g_cas : {n : Level} {t : Set n} → Context  → AtomicNat → ( Code → Context → t ) → t
+g_cas {n} {t} c a next = f a ( AtomicNatAPI.old api   )( AtomicNat.value a ) ( AtomicNatAPI.value api   )
+         $ λ a → next ( AtomicNatAPI.next api  ) record c { atomicNat = record api   { impl = a } }   where
+    api : AtomicNatAPI
+    api = Context.atomicNat c
+    f : AtomicNat → (old now new : ℕ ) → ( AtomicNat → t ) → t
+    f a old now new next1 with <-cmp old now 
+    ... | tri≈ ¬a b ¬c = next1 record a { value = new }
+    ... | tri< a₁ ¬b ¬c = next ( Context.fail c) c
+    ... | tri> ¬a ¬b _ = next ( Context.fail c) c
+
+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 { 
+    atomicNat = {!!} }
+
+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 { 
+    atomicNat = {!!} }
+
+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 {
+    atomicNat = {!!} }
 
-putdown_lfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
-putdown_lfork_stub p next = putdown_lfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_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 {
+    atomicNat = {!!} }
+
+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 p next = set {!!} {!!} ( λ ph → 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 } )
 
-code_table :  {n : Level} {t : Set n} → Code → Process → ( Process → t) → t
-code_table C_set  = {!!}
+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 } )
+
+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 } )
+
+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 } )
+
+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 = {!!}
-code_table C_pickup_rfork = {!!}
-code_table C_pickup_lfork = {!!}
-code_table C_eating = {!!}
+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 Process
+open Context
 
-step : {n : Level} {t : Set n} → List Process → (List Process → t) → t
+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 (next_code p) p ( λ np → next0 (ps ++ ( np ∷ [] ) )) 
+step {n} {t} (p ∷ ps) next0 = code_table {!!} p ( λ np → next0 (ps ++ ( np ∷ [] ) )) 
 
-test : List Process
-test = step ( record { phil = record { pid = 1 ; left = record { value = 1 }  ; right = record { value = 1 }  } ; next_code = C_putdown_rfork } ∷ [] ) ( λ ps → ps )
+test : List Context
+test = step {!!} ( λ ps → ps )
 
-test1 : List Process
-test1 = step ( record { phil = record { pid = 1 ; left = record { value = 1 }  ; right = record { value = 1 }  } ; next_code = C_putdown_rfork } ∷ [] )
+test1 : List Context
+test1 = step {!!}
   $ λ ps → step ps $ λ ps → ps
 
 -- loop exexution
--- a/Todo.txt	Tue Apr 19 19:39:29 2022 +0900
+++ b/Todo.txt	Tue May 03 18:34:47 2022 +0900
@@ -1,4 +1,25 @@
-<<<<<<< working copy
+Sun May  1 15:04:57 JST 2022
+
+    Model checking
+
+    goto 先の番号を stub に書くのは変
+
+　　process : context が別々
+　　thread  : context 一緒、goto 先が異なる
+              context は共有 実行は codeGear は atomic
+    shared    file descriptor など
+
+    single phils    direct connection single thread
+                    no shared data
+
+    multi process phils    separate process
+                           shared context
+
+    multi threaded phils   shared process
+                           serate next
+                           atomic codeGear execution
+　　
+
 Thu May 17 15:26:56 JST 2018
 
     findNode -> replaceNode -> getRedBlackTree だが
@@ -7,11 +28,6 @@
 
    という形で証明しても良い。一挙に証明するのは,可能だろうけど、良くないはず。
 
-||||||| base
-=======
-
-
->>>>>>> destination
 Sun May  6 17:54:50 JST 2018
 
     do1 a $ \b ->  do2 b next を、do1 と do2  に分離することはできる?