|
635
|
1 module ModelChecking where
|
|
|
2
|
|
|
3 open import Level renaming (zero to Z ; suc to succ)
|
|
|
4
|
|
|
5 open import Data.Nat hiding (compare)
|
|
|
6 open import Data.Nat.Properties as NatProp
|
|
|
7 open import Data.Maybe
|
|
|
8 -- open import Data.Maybe.Properties
|
|
|
9 open import Data.Empty
|
|
|
10 open import Data.List
|
|
710
|
11 -- open import Data.Tree.Binary
|
|
|
12 -- open import Data.Product
|
|
635
|
13 open import Function as F hiding (const)
|
|
|
14 open import Relation.Binary
|
|
|
15 open import Relation.Binary.PropositionalEquality
|
|
|
16 open import Relation.Nullary
|
|
|
17 open import logic
|
|
|
18 open import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_)
|
|
|
19 open import Relation.Binary.Definitions
|
|
|
20
|
|
|
21 record AtomicNat : Set where
|
|
|
22 field
|
|
709
|
23 anid : ℕ
|
|
635
|
24 value : ℕ
|
|
|
25
|
|
709
|
26 --
|
|
|
27 -- single process implemenation
|
|
|
28 --
|
|
|
29
|
|
710
|
30 f_set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
|
|
|
31 f_set a v next = next record a { value = v }
|
|
635
|
32
|
|
|
33 record Phils : Set where
|
|
|
34 field
|
|
|
35 pid : ℕ
|
|
|
36 left right : AtomicNat
|
|
|
37
|
|
709
|
38 pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
39 pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
40 eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
635
|
41 putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
42 putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
43 thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
44
|
|
710
|
45 -- pickup_rfork p next = f_set (Phils.right p) (Phils.pid p) ( λ f → goto C_pickup_lfork record p { right = f } next )
|
|
|
46
|
|
|
47 pickup_rfork p next = f_set (Phils.right p) (Phils.pid p) ( λ f → pickup_lfork record p { right = f } next )
|
|
|
48 pickup_lfork p next = f_set (Phils.left p) (Phils.pid p) ( λ f → eating record p { left = f } next )
|
|
709
|
49 eating p next = putdown_rfork p next
|
|
710
|
50 putdown_rfork p next = f_set (Phils.right p) 0 ( λ f → putdown_lfork record p { right = f } next )
|
|
|
51 putdown_lfork p next = f_set (Phils.left p) 0 ( λ f → thinking record p { left = f } next )
|
|
709
|
52 thinking p next = next p
|
|
635
|
53
|
|
709
|
54 run : Phils
|
|
|
55 run = pickup_rfork record { pid = 1 ; left = record { anid = 1 ; value = 0 } ; right = record { anid = 2 ; value = 0 } } $ λ p → p
|
|
635
|
56
|
|
709
|
57 --
|
|
|
58 -- goto version
|
|
|
59 --
|
|
635
|
60
|
|
636
|
61 data Code : Set where
|
|
|
62 C_set : 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
|
|
709
|
70 --
|
|
|
71 -- all possible arguments in APIs
|
|
|
72 --
|
|
|
73 record AtomicNatAPI : Set where
|
|
636
|
74 field
|
|
709
|
75 next : Code
|
|
|
76 value : ℕ
|
|
|
77 old : ℕ
|
|
|
78 impl : AtomicNat
|
|
|
79
|
|
|
80 record PhilsAPI : Set where
|
|
|
81 field
|
|
|
82 next : Code
|
|
|
83 impl : Phils
|
|
|
84
|
|
|
85 data Data : Set where
|
|
710
|
86 D_AtomicNat : AtomicNat → Data
|
|
|
87 D_Phils : Phils → Data
|
|
|
88 A_AtomicNat : AtomicNatAPI → Data
|
|
|
89 A_Phils : PhilsAPI → Data
|
|
|
90
|
|
|
91 data Error : Set where
|
|
|
92 E_cas_fail : Error
|
|
|
93
|
|
|
94 open import hoareBinaryTree
|
|
709
|
95
|
|
|
96 record Context : Set where
|
|
|
97 field
|
|
|
98 next : Code
|
|
|
99 fail : Code
|
|
|
100 phil : PhilsAPI
|
|
|
101 atomicNat : AtomicNatAPI
|
|
710
|
102 mbase : ℕ
|
|
|
103 memory : bt Data
|
|
709
|
104 error : Data
|
|
|
105 fail_next : Code
|
|
|
106
|
|
710
|
107 alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t
|
|
|
108 alloc-data {n} {t} c next = next record c { mbase = ( suc ( Context.mbase c ) ) } ( suc ( Context.mbase c ) )
|
|
|
109
|
|
|
110 update-data : {n : Level} {t : Set n} → ( c : Context ) → ℕ → Data → ( Context → t ) → t
|
|
|
111 update-data c n x next = insertTree (Context.memory c) n x ( λ bt → next record c { memory = bt } )
|
|
|
112
|
|
|
113 f_cas : {n : Level} {t : Set n} → AtomicNat → (old now new : ℕ ) → ( Error → t) → ( AtomicNat → t ) → t
|
|
|
114 f_cas a old now new error next with <-cmp old now
|
|
|
115 ... | tri≈ ¬a b ¬c = next record a { value = new }
|
|
|
116 ... | tri< a₁ ¬b ¬c = error E_cas_fail
|
|
|
117 ... | tri> ¬a ¬b _ = error E_cas_fail
|
|
|
118
|
|
|
119 --
|
|
|
120 -- second level stub
|
|
|
121 --
|
|
709
|
122 g_set : {n : Level} {t : Set n} → Context → AtomicNat → ( Code → Context → t ) → t
|
|
710
|
123 g_set {_} {t} c a next = f_set a ( AtomicNatAPI.value api )
|
|
709
|
124 $ λ a → next ( AtomicNatAPI.next api ) record c { atomicNat = record api { impl = a } } where
|
|
|
125 api : AtomicNatAPI
|
|
|
126 api = Context.atomicNat c
|
|
636
|
127
|
|
709
|
128 g_cas : {n : Level} {t : Set n} → Context → AtomicNat → ( Code → Context → t ) → t
|
|
710
|
129 g_cas {n} {t} c a next = f_cas a ( AtomicNatAPI.old api )( AtomicNat.value a ) ( AtomicNatAPI.value api ) ( λ e → next (Context.fail_next c) c )
|
|
709
|
130 $ λ a → next ( AtomicNatAPI.next api ) record c { atomicNat = record api { impl = a } } where
|
|
|
131 api : AtomicNatAPI
|
|
|
132 api = Context.atomicNat c
|
|
|
133
|
|
|
134 g_putdown_rfork : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t
|
|
|
135 g_putdown_rfork c p next = next C_set record c {
|
|
710
|
136 atomicNat = record (Context.atomicNat c) { impl = Phils.right p ; value = Phils.pid p ; old = AtomicNat.value (Phils.right p ) ; next = C_putdown_lfork } }
|
|
709
|
137
|
|
|
138 g_putdown_lfork : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t
|
|
|
139 g_putdown_lfork c p next = next C_set record c {
|
|
710
|
140 atomicNat = record (Context.atomicNat c) { impl = Phils.left p ; value = Phils.pid p ; old = AtomicNat.value (Phils.left p ) ; next = C_thinking } }
|
|
709
|
141
|
|
|
142 g_thinking : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t
|
|
|
143 g_thinking c p next = next C_pickup_rfork c
|
|
|
144
|
|
|
145 g_pickup_rfork : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t
|
|
|
146 g_pickup_rfork c p next = next C_set record c {
|
|
710
|
147 atomicNat = record (Context.atomicNat c) { impl = Phils.right p ; value = 0 ; old = AtomicNat.value (Phils.right p ) ; next = C_pickup_lfork } }
|
|
708
|
148
|
|
709
|
149 g_pickup_lfork : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t
|
|
|
150 g_pickup_lfork c p next = next C_set record c {
|
|
710
|
151 atomicNat = record (Context.atomicNat c) { impl = Phils.left p ; value = 0 ; old = AtomicNat.value (Phils.left p ) ; next = C_eating } }
|
|
709
|
152
|
|
|
153 g_eating : {n : Level} {t : Set n} → Context → Phils → ( Code → Context → t ) → t
|
|
|
154 g_eating c p next = next C_putdown_rfork c
|
|
|
155
|
|
|
156 set_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
|
|
710
|
157 set_stub c next = f_cas (AtomicNatAPI.impl api) (AtomicNatAPI.old api) {!!} (AtomicNatAPI.value api) {!!} ( λ ai → next {!!} ) where
|
|
|
158 api : AtomicNatAPI
|
|
|
159 api = Context.atomicNat c
|
|
|
160 ai : {!!}
|
|
|
161 ai = updateTree {!!} {!!} {!!} {!!} {!!}
|
|
709
|
162
|
|
|
163 putdown_rfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
|
|
|
164 putdown_rfork_stub p next = {!!} -- g_putdown_rfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )
|
|
636
|
165
|
|
709
|
166 putdown_lfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
|
|
|
167 putdown_lfork_stub p next = {!!} -- g_putdown_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_thinking } )
|
|
|
168
|
|
|
169 thinking_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
|
|
|
170 thinking_stub p next = {!!} -- g_thinking ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_pickup_rfork } )
|
|
|
171
|
|
|
172 pickup_rfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
|
|
|
173 pickup_rfork_stub p next = {!!} -- g_pickup_rfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_pickup_lfork } )
|
|
|
174
|
|
|
175 pickup_lfork_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
|
|
|
176 pickup_lfork_stub p next = {!!} -- g_pickup_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_eating } )
|
|
|
177
|
|
|
178 eating_stub : {n : Level} {t : Set n} → Context → ( Context → t) → t
|
|
|
179 eating_stub p next = {!!} -- g_pickup_lfork ( Context.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_rfork } )
|
|
|
180
|
|
|
181 code_table : {n : Level} {t : Set n} → Code → Context → ( Context → t) → t
|
|
|
182 code_table C_set = set_stub
|
|
636
|
183 code_table C_putdown_rfork = putdown_rfork_stub
|
|
708
|
184 code_table C_putdown_lfork = putdown_lfork_stub
|
|
709
|
185 code_table C_thinking = thinking_stub
|
|
|
186 code_table C_pickup_rfork = pickup_rfork_stub
|
|
|
187 code_table C_pickup_lfork = pickup_lfork_stub
|
|
|
188 code_table C_eating = eating_stub
|
|
636
|
189
|
|
709
|
190 open Context
|
|
708
|
191
|
|
709
|
192 step : {n : Level} {t : Set n} → List Context → (List Context → t) → t
|
|
708
|
193 step {n} {t} [] next0 = next0 []
|
|
709
|
194 step {n} {t} (p ∷ ps) next0 = code_table {!!} p ( λ np → next0 (ps ++ ( np ∷ [] ) ))
|
|
708
|
195
|
|
709
|
196 test : List Context
|
|
|
197 test = step {!!} ( λ ps → ps )
|
|
708
|
198
|
|
709
|
199 test1 : List Context
|
|
|
200 test1 = step {!!}
|
|
708
|
201 $ λ ps → step ps $ λ ps → ps
|
|
|
202
|
|
|
203 -- loop exexution
|
|
|
204
|
|
|
205 -- concurrnt execution
|
|
|
206
|
|
|
207 -- state db ( binary tree of processes )
|
|
|
208
|
|
|
209 -- depth first ececution
|
|
|
210
|
|
|
211 -- verify temporal logic poroerries
|
|
636
|
212
|
|
|
213
|
|
|
214
|
