Mercurial > hg > Gears > GearsAgda

comparison ModelChecking.agda @ 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
comparison
equal deleted inserted replaced
712:64a86fde1f90 713:252e15bcbbb8
21 record AtomicNat : Set where 21 record AtomicNat : Set where
22 field 22 field
23 anid : ℕ -- memory pointer ( unique id of DataGear ) 23 anid : ℕ -- memory pointer ( unique id of DataGear )
24 value : ℕ 24 value : ℕ
25 25
26 init-AtomicNat : AtomicNat
27 init-AtomicNat = record { anid = 0 ; value = 0 }
28
26 -- 29 --
27 -- single process implemenation 30 -- single process implemenation
28 -- 31 --
29 32
30 f_set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t 33 f_set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
32 35
33 record Phil : Set where 36 record Phil : Set where
34 field 37 field
35 pid : ℕ 38 pid : ℕ
36 left right : AtomicNat 39 left right : AtomicNat
40
41 init-Phil : Phil
42 init-Phil = record { pid = 0 ; left = init-AtomicNat ; right = init-AtomicNat }
37 43
38 pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t 44 pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
39 pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t 45 pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
40 eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t 46 eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
41 putdown_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t 47 putdown_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t
57 -- 63 --
58 -- Coda Gear 64 -- Coda Gear
59 -- 65 --
60 66
61 data Code : Set where 67 data Code : Set where
68 C_nop : Code
62 C_cas_int : Code 69 C_cas_int : Code
63 C_putdown_rfork : Code 70 C_putdown_rfork : Code
64 C_putdown_lfork : Code 71 C_putdown_lfork : Code
65 C_thinking : Code 72 C_thinking : Code
66 C_pickup_rfork : Code 73 C_pickup_rfork : Code
67 C_pickup_lfork : Code 74 C_pickup_lfork : Code
68 C_eating : Code 75 C_eating : Code
69 76
70 -- 77 --
71 -- all possible arguments in APIs 78 -- all possible arguments in -APIs
72 -- 79 --
73 record AtomicNatAPI : Set where 80 record AtomicNat-API : Set where
74 field 81 field
75 next : Code 82 next : Code
76 fail : Code 83 fail : Code
77 value : ℕ 84 value : ℕ
78 impl : AtomicNat 85 impl : AtomicNat
79 86
80 record PhilAPI : Set where 87 record Phil-API : Set where
81 field 88 field
82 next : Code 89 next : Code
83 impl : Phil 90 impl : Phil
84 91
92 data Error : Set where
93 E_panic : Error
94 E_cas_fail : Error
95
85 -- 96 --
86 -- Data Gear 97 -- Data Gear
87 -- 98 --
88 data Data : Set where 99 data Data : Set where
89 D_AtomicNat : AtomicNat → Data 100 D_AtomicNat : AtomicNat → Data
90 D_Phil : Phil → Data 101 D_Phil : Phil → Data
91 102 D_Error : Error → Data
92 -- A_AtomicNat : AtomicNatAPI → Data 103
93 -- A_Phil : PhilAPI → Data 104 -- A_AtomicNat : AtomicNat-API → Data
94 105 -- A_Phil : Phil-API → Data
95 data Error : Set where E_cas_fail : Error
96 106
97 open import hoareBinaryTree 107 open import hoareBinaryTree
98 108
99 record Context : Set where 109 record Context : Set where
100 field 110 field
101 next : Code 111 next : Code
102 fail : Code 112 fail : Code
103 113
104 -- API list (frame in Gears Agda ) 114 -- -API list (frame in Gears Agda )
105 c_PhilAPI : PhilAPI 115 c_Phil-API : Phil-API
106 c_AtomicNatAPI : AtomicNatAPI 116 c_AtomicNat-API : AtomicNat-API
107 117
108 mbase : ℕ 118 mbase : ℕ
109 memory : bt Data 119 memory : bt Data
110 error : Data 120 error : Data
111 fail_next : Code 121 fail_next : Code
121 -- 131 --
122 AtomicInt_cas_stub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t 132 AtomicInt_cas_stub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
123 AtomicInt_cas_stub {_} {t} c next = updateTree (Context.memory c) (AtomicNat.anid ai) ( D_AtomicNat (record ai { value = AtomicNat.value ai } )) 133 AtomicInt_cas_stub {_} {t} c next = updateTree (Context.memory c) (AtomicNat.anid ai) ( D_AtomicNat (record ai { value = AtomicNat.value ai } ))
124 ( λ bt → next ( Context.fail c ) c ) -- segmentation fault ( null pointer ) 134 ( λ bt → next ( Context.fail c ) c ) -- segmentation fault ( null pointer )
125 $ λ now bt → f_cas ai (AtomicNat.value ai) now bt where 135 $ λ now bt → f_cas ai (AtomicNat.value ai) now bt where
126 api : AtomicNatAPI 136 api : AtomicNat-API
127 api = Context.c_AtomicNatAPI c 137 api = Context.c_AtomicNat-API c
128 ai : AtomicNat 138 ai : AtomicNat
129 ai = AtomicNatAPI.impl api 139 ai = AtomicNat-API.impl api
130 f_cas : AtomicNat → (old : ℕ ) → Data → bt Data → t 140 f_cas : AtomicNat → (old : ℕ ) → Data → bt Data → t
131 f_cas a old (D_AtomicNat now) bt with <-cmp old ( AtomicNat.value now ) 141 f_cas a old (D_AtomicNat now) bt with <-cmp old ( AtomicNat.value now )
132 ... | tri≈ ¬a b ¬c = next (AtomicNatAPI.fail api) ( record c { memory = bt ; c_AtomicNatAPI = record api { impl = a } } ) -- update memory 142 ... | tri≈ ¬a b ¬c = next (AtomicNat-API.fail api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = a } } ) -- update memory
133 ... | tri< a₁ ¬b ¬c = next (AtomicNatAPI.fail api) c 143 ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c
134 ... | tri> ¬a ¬b _ = next (AtomicNatAPI.fail api) c 144 ... | tri> ¬a ¬b _ = next (AtomicNat-API.fail api) c
135 f_cas a old _ bt = next ( Context.fail c ) c -- type error 145 f_cas a old _ bt = next ( Context.fail c ) c -- type error
136 146
137 147
138 Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t 148 Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
139 Phil_putdown_rfork_sub c next = next C_cas_int record c { 149 Phil_putdown_rfork_sub c next = next C_cas_int record c {
140 c_AtomicNatAPI = record { impl = Phil.right phil ; value = Phil.pid phil ; fail = C_putdown_lfork ; next = C_putdown_lfork } } where 150 c_AtomicNat-API = record { impl = Phil.right phil ; value = Phil.pid phil ; fail = C_putdown_lfork ; next = C_putdown_lfork } } where
141 phil : Phil 151 phil : Phil
142 phil = PhilAPI.impl ( Context.c_PhilAPI c ) 152 phil = Phil-API.impl ( Context.c_Phil-API c )
143 153
144 Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t 154 Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
145 Phil_putdown_lfork_sub c next = next C_cas_int record c { 155 Phil_putdown_lfork_sub c next = next C_cas_int record c {
146 c_AtomicNatAPI = record { impl = Phil.left phil ; value = Phil.pid phil ; fail = C_thinking ; next = C_thinking } } where 156 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.pid phil ; fail = C_thinking ; next = C_thinking } } where
147 phil : Phil 157 phil : Phil
148 phil = PhilAPI.impl ( Context.c_PhilAPI c ) 158 phil = Phil-API.impl ( Context.c_Phil-API c )
149 159
150 Phil_thiking : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t 160 Phil_thiking : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
151 Phil_thiking c next = next C_pickup_rfork c 161 Phil_thiking c next = next C_pickup_rfork c
152 162
153 Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t 163 Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
154 Phil_pickup_lfork_sub c next = next C_cas_int record c { 164 Phil_pickup_lfork_sub c next = next C_cas_int record c {
155 c_AtomicNatAPI = record { impl = Phil.left phil ; value = Phil.pid phil ; fail = C_pickup_rfork ; next = C_pickup_lfork } } where 165 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.pid phil ; fail = C_pickup_rfork ; next = C_pickup_lfork } } where
156 phil : Phil 166 phil : Phil
157 phil = PhilAPI.impl ( Context.c_PhilAPI c ) 167 phil = Phil-API.impl ( Context.c_Phil-API c )
158 168
159 Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t 169 Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
160 Phil_pickup_rfork_sub c next = next C_cas_int record c { 170 Phil_pickup_rfork_sub c next = next C_cas_int record c {
161 c_AtomicNatAPI = record { impl = Phil.left phil ; value = Phil.pid phil ; fail = C_pickup_lfork ; next = C_eating } } where 171 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.pid phil ; fail = C_pickup_lfork ; next = C_eating } } where
162 phil : Phil 172 phil : Phil
163 phil = PhilAPI.impl ( Context.c_PhilAPI c ) 173 phil = Phil-API.impl ( Context.c_Phil-API c )
164 174
165 Phil_eating_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t 175 Phil_eating_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t
166 Phil_eating_sub c next = next C_putdown_rfork c 176 Phil_eating_sub c next = next C_putdown_rfork c
167 177
168 code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t 178 code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t
179 code_table C_nop = λ c next → next C_nop c
169 code_table C_cas_int = AtomicInt_cas_stub 180 code_table C_cas_int = AtomicInt_cas_stub
170 code_table C_putdown_rfork = Phil_putdown_rfork_sub 181 code_table C_putdown_rfork = Phil_putdown_rfork_sub
171 code_table C_putdown_lfork = Phil_putdown_lfork_sub 182 code_table C_putdown_lfork = Phil_putdown_lfork_sub
172 code_table C_thinking = Phil_thiking 183 code_table C_thinking = Phil_thiking
173 code_table C_pickup_rfork = Phil_pickup_lfork_sub 184 code_table C_pickup_rfork = Phil_pickup_lfork_sub
174 code_table C_pickup_lfork = Phil_pickup_rfork_sub 185 code_table C_pickup_lfork = Phil_pickup_rfork_sub
175 code_table C_eating = Phil_eating_sub 186 code_table C_eating = Phil_eating_sub
176 187
177 open Context 188 open Context
178 189
190 new : {n : Level} {t : Set n} → ( c : Context ) → Data → ( Context → ℕ → t ) → t
191 new c1 d next = alloc-data c1 ( λ c1 n → update-data c1 n d (λ c2 → next c2 n ))
192
179 step : {n : Level} {t : Set n} → List Context → (List Context → t) → t 193 step : {n : Level} {t : Set n} → List Context → (List Context → t) → t
180 step {n} {t} [] next0 = next0 [] 194 step {n} {t} [] next0 = next0 []
181 step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (ps ++ ( record np { next = code } ∷ [] ))) 195 step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (ps ++ ( record np { next = code } ∷ [] )))
182 196
197 init-context : Context
198 init-context = record {
199 next = C_nop
200 ; fail = C_nop
201 ; c_Phil-API = record { next = C_nop ; impl = init-Phil }
202 ; c_AtomicNat-API = record { next = C_nop ; fail = C_nop ; value = 0 ; impl = init-AtomicNat }
203 ; mbase = 0
204 ; memory = leaf
205 ; error = D_Error E_panic
206 ; fail_next = C_nop
207 }
208
209 init-phil-1 : (pid : ℕ ) → (left right : AtomicNat ) → List Context
210 init-phil-1 pid left right = c ∷ [] where
211 c : Context
212 c = record init-context { c_Phil-API = record { next = C_thinking ; impl = record init-Phil { pid = pid ; left = left ; right = right } } }
213
183 test : List Context 214 test : List Context
184 test = step {!!} ( λ ps → ps ) 215 test = step {!!} ( λ ps → ps )
185 216
186 test1 : List Context 217 test1 : List Context
187 test1 = step {!!} 218 test1 = step {!!}
188 $ λ ps → step ps $ λ ps → ps 219 $ λ ps → step ps $ λ ps → ps
189 220