Mercurial > hg > Gears > GearsAgda

comparison DPP.agda @ 949:057d3309ed9d

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 Sun, 04 Aug 2024 13:05:12 +0900
parents ModelChecking.agda@f2a3f5707075
children
comparison
equal deleted inserted replaced
948:e5288029f850 949:057d3309ed9d
1 {-# OPTIONS --cubical-compatible #-}
2 -- {-# OPTIONS --cubical-compatible --safe #-}
3 module DPP where
4
5 open import Level renaming (zero to Z ; suc to succ)
6
7 open import Data.Nat hiding (compare)
8 open import Data.Nat.Properties as NatProp
9 open import Data.Maybe
10 -- open import Data.Maybe.Properties
11 open import Data.Empty
12 open import Data.List
13 -- open import Data.Tree.Binary
14 -- open import Data.Product
15 open import Function as F hiding (const)
16 open import Relation.Binary
17 open import Relation.Binary.PropositionalEquality
18 open import Relation.Nullary
19 open import logic
20 open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_)
21 open import Relation.Binary.Definitions
22
23 open import ModelChecking
24
25
26 --
27 -- single process implemenation
28 --
29
30
31 record Phil : Set where
32 field
33 ptr : ℕ
34 left right : AtomicNat
35
36 init-Phil : Phil
37 init-Phil = record { ptr = 0 ; left = init-AtomicNat ; right = init-AtomicNat }
38
39 pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
40 pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
41 eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
42 putdown_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
43 putdown_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
44 thinking : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
45
46 pickup_rfork p next = f_set (Phil.right p) (Phil.ptr p) ( λ f → pickup_lfork record p { right = f } next )
47 pickup_lfork p next = f_set (Phil.left p) (Phil.ptr p) ( λ f → eating record p { left = f } next )
48 eating p next = putdown_rfork p next
49 putdown_rfork p next = f_set (Phil.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
50 putdown_lfork p next = f_set (Phil.left p) 0 ( λ f → thinking record p { left = f } next )
51 thinking p next = next p
52
53 run : Phil
54 run = pickup_rfork record { ptr = 1 ; left = record { ptr = 2 ; value = 0 } ; right = record { ptr = 3 ; value = 0 } } $ λ p → p
55
56 --
57 -- Coda Gear
58 --
59
60 data Code : Set where
61 C_nop : Code
62 C_cas_int : Code
63 C_putdown_rfork : Code
64 C_putdown_lfork : Code
65 C_thinking : Code
66 C_pickup_rfork : Code
67 C_pickup_lfork : Code
68 C_eating : Code
69
70 --
71 -- all possible arguments in -APIs
72 --
73
74 record Phil-API : Set where
75 field
76 next : Code
77 impl : Phil
78
79 --
80 -- Data Gear
81 --
82 -- waiting / pointer / available
83 --
84 data Data : Set where
85 -- D_AtomicNat : AtomicNat → ℕ → Data
86 D_AtomicNat : AtomicNat → Data
87 D_Phil : Phil → Data
88 D_Error : Error → Data
89
90 -- data API : Set where
91 -- A_AtomicNat : AtomicNat-API → API
92 -- A_Phil : Phil-API → API
93
94 -- open import hoareBinaryTree
95
96 data bt {n : Level} (A : Set n) : Set n where
97 leaf : bt A
98 node : (key : ℕ) → (value : A) →
99 (left : bt A ) → (right : bt A ) → bt A
100
101 updateTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (empty : bt A → t ) → (next : A → bt A → t ) → t
102 updateTree = ?
103
104 insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t
105 insertTree = ?
106
107
108 --
109 -- second level stub
110 --
111
112 -- putdown_rfork : Phil → (? → t) → t
113 -- putdown_rfork p next = goto p->lfork->cas( 0 , putdown_lfork, putdown_lfork ) , next
114
115 Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
116 Phil_putdown_rfork_sub c next = next C_cas_int record c {
117 c_AtomicNat-API = record { impl = Phil.right phil ; value = 0 ; fail = C_putdown_lfork ; next = C_putdown_lfork } } where
118 phil : Phil
119 phil = Phil-API.impl ( Context.c_Phil-API c )
120
121 Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
122 Phil_putdown_lfork_sub c next = next C_cas_int record c {
123 c_AtomicNat-API = record { impl = Phil.left phil ; value = 0 ; fail = C_thinking ; next = C_thinking } } where
124 phil : Phil
125 phil = Phil-API.impl ( Context.c_Phil-API c )
126
127 Phil_thiking : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
128 Phil_thiking c next = next C_pickup_rfork c
129
130 Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
131 Phil_pickup_lfork_sub c next = next C_cas_int record c {
132 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_lfork ; next = C_pickup_rfork } } where
133 phil : Phil
134 phil = Phil-API.impl ( Context.c_Phil-API c )
135
136 Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
137 Phil_pickup_rfork_sub c next = next C_cas_int record c {
138 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_rfork ; next = C_eating } } where
139 phil : Phil
140 phil = Phil-API.impl ( Context.c_Phil-API c )
141
142 Phil_eating_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
143 Phil_eating_sub c next = next C_putdown_rfork c
144
145 code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t
146 code_table C_nop = λ c next → next C_nop c
147 code_table C_cas_int = AtomicInt_cas_stub
148 code_table C_putdown_rfork = Phil_putdown_rfork_sub
149 code_table C_putdown_lfork = Phil_putdown_lfork_sub
150 code_table C_thinking = Phil_thiking
151 code_table C_pickup_rfork = Phil_pickup_lfork_sub
152 code_table C_pickup_lfork = Phil_pickup_rfork_sub
153 code_table C_eating = Phil_eating_sub
154
155
156 init-Phil-0 : (ps : List Context) → (left right : AtomicNat ) → List Context
157 init-Phil-0 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
158 p : ℕ → Phil
159 p ptr = record init-Phil { ptr = ptr ; left = left ; right = right }
160 c1 : List Context → Context
161 c1 [] = init-context
162 c1 (c2 ∷ ct) = c2
163
164 init-AtomicNat1 : {n : Level} {t : Set n} → Context → ( Context → AtomicNat → t ) → t
165 init-AtomicNat1 c1 next = new-data c1 ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) where
166 a : ℕ → AtomicNat
167 a ptr = record { ptr = ptr ; value = 0 }
168
169 init-Phil-1 : (c1 : Context) → Context
170 init-Phil-1 c1 = record c1 { memory = mem2 $ mem1 $ mem ; mbase = n + 3 } where
171 n : ℕ
172 n = Context.mbase c1
173 left = record { ptr = suc n ; value = 0}
174 right = record { ptr = suc (suc n) ; value = 0}
175 mem : bt Data
176 mem = insertTree ( Context.memory c1) (suc n) (D_AtomicNat left)
177 $ λ t → t
178 mem1 : bt Data → bt Data
179 mem1 t = insertTree t (suc (suc n)) (D_AtomicNat right )
180 $ λ t → t
181 mem2 : bt Data → bt Data
182 mem2 t = insertTree t (n + 3) (D_Phil record { ptr = n + 3 ; left = left ; right = right })
183 $ λ t → t
184
185 test-i0 : bt Data
186 test-i0 = Context.memory (init-Phil-1 init-context)
187
188 make-phil : ℕ → Context
189 make-phil zero = init-context
190 make-phil (suc n) = init-Phil-1 ( make-phil n )
191
192 test-i5 : bt Data
193 test-i5 = Context.memory (make-phil 5)
194
195 -- loop exexution
196
197 -- concurrnt execution
198
199 -- state db ( binary tree of processes )
200
201 -- depth first execution
202
203 -- verify temporal logic poroerries
204
205
206