Mercurial > hg > Gears > GearsAgda
annotate ModelChecking.agda @ 726:e545646e5f64
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 10 Apr 2023 17:57:26 +0900 |
| parents | b088fa199d3d |
| children | 0b791ae19543 |
| rev | line source |
|---|---|
| 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 | |
| 714 | 23 ptr : ℕ -- memory pointer ( unique id of DataGear ) |
| 635 | 24 value : ℕ |
| 25 | |
| 713 | 26 init-AtomicNat : AtomicNat |
| 714 | 27 init-AtomicNat = record { ptr = 0 ; value = 0 } |
| 713 | 28 |
| 709 | 29 -- |
| 30 -- single process implemenation | |
| 31 -- | |
| 32 | |
| 710 | 33 f_set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t |
| 34 f_set a v next = next record a { value = v } | |
| 635 | 35 |
| 712 | 36 record Phil : Set where |
| 635 | 37 field |
| 714 | 38 ptr : ℕ |
| 635 | 39 left right : AtomicNat |
| 40 | |
| 713 | 41 init-Phil : Phil |
| 714 | 42 init-Phil = record { ptr = 0 ; left = init-AtomicNat ; right = init-AtomicNat } |
| 713 | 43 |
| 712 | 44 pickup_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t |
| 45 pickup_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t | |
| 46 eating : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t | |
| 47 putdown_rfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t | |
| 48 putdown_lfork : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t | |
| 49 thinking : {n : Level} {t : Set n} → Phil → ( Phil → t ) → t | |
| 635 | 50 |
| 714 | 51 pickup_rfork p next = f_set (Phil.right p) (Phil.ptr p) ( λ f → pickup_lfork record p { right = f } next ) |
| 52 pickup_lfork p next = f_set (Phil.left p) (Phil.ptr p) ( λ f → eating record p { left = f } next ) | |
| 709 | 53 eating p next = putdown_rfork p next |
| 712 | 54 putdown_rfork p next = f_set (Phil.right p) 0 ( λ f → putdown_lfork record p { right = f } next ) |
| 55 putdown_lfork p next = f_set (Phil.left p) 0 ( λ f → thinking record p { left = f } next ) | |
| 709 | 56 thinking p next = next p |
| 635 | 57 |
| 712 | 58 run : Phil |
| 716 | 59 run = pickup_rfork record { ptr = 1 ; left = record { ptr = 2 ; value = 0 } ; right = record { ptr = 3 ; value = 0 } } $ λ p → p |
| 635 | 60 |
| 709 | 61 -- |
| 711 | 62 -- Coda Gear |
| 709 | 63 -- |
| 635 | 64 |
| 636 | 65 data Code : Set where |
| 713 | 66 C_nop : Code |
| 711 | 67 C_cas_int : Code |
| 636 | 68 C_putdown_rfork : Code |
| 69 C_putdown_lfork : Code | |
| 70 C_thinking : Code | |
| 71 C_pickup_rfork : Code | |
| 72 C_pickup_lfork : Code | |
| 73 C_eating : Code | |
| 74 | |
| 709 | 75 -- |
| 713 | 76 -- all possible arguments in -APIs |
| 709 | 77 -- |
| 713 | 78 record AtomicNat-API : Set where |
| 636 | 79 field |
| 709 | 80 next : Code |
| 711 | 81 fail : Code |
| 709 | 82 value : ℕ |
| 83 impl : AtomicNat | |
| 84 | |
| 713 | 85 record Phil-API : Set where |
| 709 | 86 field |
| 87 next : Code | |
| 712 | 88 impl : Phil |
| 709 | 89 |
| 713 | 90 data Error : Set where |
| 91 E_panic : Error | |
| 92 E_cas_fail : Error | |
| 93 | |
| 711 | 94 -- |
| 95 -- Data Gear | |
| 96 -- | |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
97 -- waiting / pointer / available |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
98 -- |
| 709 | 99 data Data : Set where |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
100 -- D_AtomicNat : AtomicNat → ℕ → Data |
| 710 | 101 D_AtomicNat : AtomicNat → Data |
| 712 | 102 D_Phil : Phil → Data |
| 713 | 103 D_Error : Error → Data |
| 710 | 104 |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
105 -- data API : Set where |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
106 -- A_AtomicNat : AtomicNat-API → API |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
107 -- A_Phil : Phil-API → API |
| 710 | 108 |
| 109 open import hoareBinaryTree | |
| 709 | 110 |
| 111 record Context : Set where | |
| 112 field | |
| 113 next : Code | |
| 114 fail : Code | |
| 711 | 115 |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
116 -- -API list (frame in Gears Agda ) --- a Data of API |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
117 -- api : List API |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
118 -- c_Phil-API : Maybe Phil-API |
| 713 | 119 c_Phil-API : Phil-API |
| 120 c_AtomicNat-API : AtomicNat-API | |
| 711 | 121 |
| 710 | 122 mbase : ℕ |
| 123 memory : bt Data | |
| 709 | 124 error : Data |
| 125 fail_next : Code | |
| 126 | |
| 710 | 127 -- |
| 128 -- second level stub | |
| 129 -- | |
| 712 | 130 AtomicInt_cas_stub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
| 716 | 131 AtomicInt_cas_stub {_} {t} c next = updateTree (Context.memory c) (AtomicNat.ptr ai) ( D_AtomicNat (record ai { value = AtomicNat-API.value api } )) |
| 711 | 132 ( λ bt → next ( Context.fail c ) c ) -- segmentation fault ( null pointer ) |
| 716 | 133 $ λ prev bt → f_cas prev bt where |
| 713 | 134 api : AtomicNat-API |
| 135 api = Context.c_AtomicNat-API c | |
| 711 | 136 ai : AtomicNat |
| 713 | 137 ai = AtomicNat-API.impl api |
| 716 | 138 f_cas : Data → bt Data → t |
| 139 f_cas (D_AtomicNat prev) bt with <-cmp ( AtomicNat.value ai ) ( AtomicNat.value prev ) | |
| 140 ... | tri≈ ¬a b ¬c = next (AtomicNat-API.next api) ( record c { memory = bt ; c_AtomicNat-API = record api { impl = prev } } ) -- update memory | |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
141 ... | tri< a₁ ¬b ¬c = next (AtomicNat-API.fail api) c --- cleaer API |
| 713 | 142 ... | tri> ¬a ¬b _ = next (AtomicNat-API.fail api) c |
| 716 | 143 f_cas a bt = next ( Context.fail c ) c -- type error / panic |
| 144 | |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
145 -- putdown_rfork : Phil → (? → t) → t |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
146 -- putdown_rfork p next = goto p->lfork->cas( 0 , putdown_lfork, putdown_lfork ) , next |
| 709 | 147 |
| 712 | 148 Phil_putdown_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
149 Phil_putdown_rfork_sub c next = next C_cas_int record c { |
| 716 | 150 c_AtomicNat-API = record { impl = Phil.right phil ; value = 0 ; fail = C_putdown_lfork ; next = C_putdown_lfork } } where |
| 712 | 151 phil : Phil |
| 713 | 152 phil = Phil-API.impl ( Context.c_Phil-API c ) |
| 709 | 153 |
| 712 | 154 Phil_putdown_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
| 155 Phil_putdown_lfork_sub c next = next C_cas_int record c { | |
| 716 | 156 c_AtomicNat-API = record { impl = Phil.left phil ; value = 0 ; fail = C_thinking ; next = C_thinking } } where |
| 712 | 157 phil : Phil |
| 713 | 158 phil = Phil-API.impl ( Context.c_Phil-API c ) |
| 709 | 159 |
| 712 | 160 Phil_thiking : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
| 161 Phil_thiking c next = next C_pickup_rfork c | |
| 709 | 162 |
| 712 | 163 Phil_pickup_lfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
| 164 Phil_pickup_lfork_sub c next = next C_cas_int record c { | |
| 716 | 165 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_lfork ; next = C_pickup_rfork } } where |
| 712 | 166 phil : Phil |
| 713 | 167 phil = Phil-API.impl ( Context.c_Phil-API c ) |
| 709 | 168 |
| 712 | 169 Phil_pickup_rfork_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
| 170 Phil_pickup_rfork_sub c next = next C_cas_int record c { | |
| 716 | 171 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_rfork ; next = C_eating } } where |
| 712 | 172 phil : Phil |
| 713 | 173 phil = Phil-API.impl ( Context.c_Phil-API c ) |
| 709 | 174 |
| 712 | 175 Phil_eating_sub : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
| 176 Phil_eating_sub c next = next C_putdown_rfork c | |
| 709 | 177 |
| 711 | 178 code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t |
| 713 | 179 code_table C_nop = λ c next → next C_nop c |
| 712 | 180 code_table C_cas_int = AtomicInt_cas_stub |
| 181 code_table C_putdown_rfork = Phil_putdown_rfork_sub | |
| 182 code_table C_putdown_lfork = Phil_putdown_lfork_sub | |
| 183 code_table C_thinking = Phil_thiking | |
| 184 code_table C_pickup_rfork = Phil_pickup_lfork_sub | |
| 185 code_table C_pickup_lfork = Phil_pickup_rfork_sub | |
| 186 code_table C_eating = Phil_eating_sub | |
| 636 | 187 |
| 709 | 188 step : {n : Level} {t : Set n} → List Context → (List Context → t) → t |
| 708 | 189 step {n} {t} [] next0 = next0 [] |
| 716 | 190 step {n} {t} (p ∷ ps) next0 = code_table (Context.next p) p ( λ code np → next0 (update-context ps np ++ ( record np { next = code } ∷ [] ))) where |
| 191 update-context : List Context → Context → List Context | |
| 192 update-context [] _ = [] | |
| 193 update-context (c1 ∷ t) np = record c1 { memory = Context.memory np ; mbase = Context.mbase np } ∷ t | |
| 708 | 194 |
| 713 | 195 init-context : Context |
| 196 init-context = record { | |
| 197 next = C_nop | |
| 198 ; fail = C_nop | |
| 199 ; c_Phil-API = record { next = C_nop ; impl = init-Phil } | |
| 200 ; c_AtomicNat-API = record { next = C_nop ; fail = C_nop ; value = 0 ; impl = init-AtomicNat } | |
| 201 ; mbase = 0 | |
| 202 ; memory = leaf | |
| 203 ; error = D_Error E_panic | |
| 204 ; fail_next = C_nop | |
| 205 } | |
| 206 | |
| 718 | 207 alloc-data : {n : Level} {t : Set n} → ( c : Context ) → ( Context → ℕ → t ) → t |
| 208 alloc-data {n} {t} c next = next record c { mbase = suc ( Context.mbase c ) } mnext where | |
| 209 mnext = suc ( Context.mbase c ) | |
| 210 | |
| 211 new-data : {n : Level} {t : Set n} → ( c : Context ) → (ℕ → Data ) → ( Context → ℕ → t ) → t | |
| 212 new-data c x next = alloc-data c $ λ c1 n → insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n ) | |
| 213 | |
|
720
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
214 init-AtomicNat0 : {n : Level} {t : Set n} → Context → ( Context → ℕ → t ) → t |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
215 init-AtomicNat0 c1 next = new-data c1 ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 ptr where |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
216 a : ℕ → AtomicNat |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
217 a ptr = record { ptr = ptr ; value = 0 } |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
218 |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
219 init-Phil-0 : (ps : List Context) → (left right : AtomicNat ) → List Context |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
220 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 |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
221 p : ℕ → Phil |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
222 p ptr = record init-Phil { ptr = ptr ; left = left ; right = right } |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
223 c1 : List Context → Context |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
224 c1 [] = init-context |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
225 c1 (c2 ∷ ct) = c2 |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
226 |
| 718 | 227 init-AtomicNat1 : {n : Level} {t : Set n} → Context → ( Context → AtomicNat → t ) → t |
| 228 init-AtomicNat1 c1 next = new-data c1 ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) where | |
| 229 a : ℕ → AtomicNat | |
| 230 a ptr = record { ptr = ptr ; value = 0 } | |
| 231 | |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
232 init-Phil-1 : (c1 : Context) → Context |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
233 init-Phil-1 c1 = record c1 { memory = mem2 $ mem1 $ mem ; mbase = n + 3 } where |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
234 n : ℕ |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
235 n = Context.mbase c1 |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
236 left = record { ptr = suc n ; value = 0} |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
237 right = record { ptr = suc (suc n) ; value = 0} |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
238 mem : bt Data |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
239 mem = insertTree ( Context.memory c1) (suc n) (D_AtomicNat left) |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
240 $ λ t → t |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
241 mem1 : bt Data → bt Data |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
242 mem1 t = insertTree t (suc (suc n)) (D_AtomicNat right ) |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
243 $ λ t → t |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
244 mem2 : bt Data → bt Data |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
245 mem2 t = insertTree t (n + 3) (D_Phil record { ptr = n + 3 ; left = left ; right = right }) |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
246 $ λ t → t |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
247 |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
248 test-i0 : bt Data |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
249 test-i0 = Context.memory (init-Phil-1 init-context) |
| 718 | 250 |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
251 make-phil : ℕ → Context |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
252 make-phil zero = init-context |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
253 make-phil (suc n) = init-Phil-1 ( make-phil n ) |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
254 |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
255 test-i5 : bt Data |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
256 test-i5 = Context.memory (make-phil 5) |
| 708 | 257 |
| 258 -- loop exexution | |
| 259 | |
| 260 -- concurrnt execution | |
| 261 | |
| 262 -- state db ( binary tree of processes ) | |
| 263 | |
| 722 | 264 -- depth first execution |
| 708 | 265 |
| 266 -- verify temporal logic poroerries | |
| 636 | 267 |
| 268 | |
| 269 |