Mercurial > hg > Gears > GearsAgda
annotate DPP.agda @ 949:057d3309ed9d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 04 Aug 2024 13:05:12 +0900 |
| parents | ModelChecking.agda@f2a3f5707075 |
| children |
| rev | line source |
|---|---|
| 949 | 1 {-# OPTIONS --cubical-compatible #-} |
| 2 -- {-# OPTIONS --cubical-compatible --safe #-} | |
| 3 module DPP where | |
| 635 | 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 | |
| 710 | 13 -- open import Data.Tree.Binary |
| 14 -- open import Data.Product | |
| 635 | 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 | |
| 933 | 20 open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_) |
| 635 | 21 open import Relation.Binary.Definitions |
| 22 | |
| 949 | 23 open import ModelChecking |
| 635 | 24 |
| 713 | 25 |
| 709 | 26 -- |
| 27 -- single process implemenation | |
| 28 -- | |
| 29 | |
| 635 | 30 |
| 712 | 31 record Phil : Set where |
| 635 | 32 field |
| 714 | 33 ptr : ℕ |
| 635 | 34 left right : AtomicNat |
| 35 | |
| 713 | 36 init-Phil : Phil |
| 714 | 37 init-Phil = record { ptr = 0 ; left = init-AtomicNat ; right = init-AtomicNat } |
| 713 | 38 |
| 712 | 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 | |
| 635 | 45 |
| 714 | 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 ) | |
| 709 | 48 eating p next = putdown_rfork p next |
| 712 | 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 ) | |
| 709 | 51 thinking p next = next p |
| 635 | 52 |
| 712 | 53 run : Phil |
| 716 | 54 run = pickup_rfork record { ptr = 1 ; left = record { ptr = 2 ; value = 0 } ; right = record { ptr = 3 ; value = 0 } } $ λ p → p |
| 635 | 55 |
| 709 | 56 -- |
| 711 | 57 -- Coda Gear |
| 709 | 58 -- |
| 635 | 59 |
| 636 | 60 data Code : Set where |
| 713 | 61 C_nop : Code |
| 711 | 62 C_cas_int : Code |
| 636 | 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 -- |
| 713 | 71 -- all possible arguments in -APIs |
| 709 | 72 -- |
| 73 | |
| 713 | 74 record Phil-API : Set where |
| 709 | 75 field |
| 76 next : Code | |
| 712 | 77 impl : Phil |
| 709 | 78 |
| 711 | 79 -- |
| 80 -- Data Gear | |
| 81 -- | |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
82 -- waiting / pointer / available |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
83 -- |
| 709 | 84 data Data : Set where |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
85 -- D_AtomicNat : AtomicNat → ℕ → Data |
| 710 | 86 D_AtomicNat : AtomicNat → Data |
| 712 | 87 D_Phil : Phil → Data |
| 713 | 88 D_Error : Error → Data |
| 710 | 89 |
|
715
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
90 -- data API : Set where |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
91 -- A_AtomicNat : AtomicNat-API → API |
|
8f8f136f2162
insertTree have some bug
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
714
diff
changeset
|
92 -- A_Phil : Phil-API → API |
| 710 | 93 |
| 949 | 94 -- open import hoareBinaryTree |
| 709 | 95 |
| 949 | 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 | |
| 711 | 100 |
| 949 | 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 = ? | |
| 711 | 103 |
| 949 | 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 | |
| 709 | 107 |
| 710 | 108 -- |
| 109 -- second level stub | |
| 110 -- | |
| 716 | 111 |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
112 -- 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
|
113 -- putdown_rfork p next = goto p->lfork->cas( 0 , putdown_lfork, putdown_lfork ) , next |
| 709 | 114 |
| 712 | 115 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
|
116 Phil_putdown_rfork_sub c next = next C_cas_int record c { |
| 716 | 117 c_AtomicNat-API = record { impl = Phil.right phil ; value = 0 ; fail = C_putdown_lfork ; next = C_putdown_lfork } } where |
| 712 | 118 phil : Phil |
| 713 | 119 phil = Phil-API.impl ( Context.c_Phil-API c ) |
| 709 | 120 |
| 712 | 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 { | |
| 716 | 123 c_AtomicNat-API = record { impl = Phil.left phil ; value = 0 ; fail = C_thinking ; next = C_thinking } } where |
| 712 | 124 phil : Phil |
| 713 | 125 phil = Phil-API.impl ( Context.c_Phil-API c ) |
| 709 | 126 |
| 712 | 127 Phil_thiking : {n : Level} {t : Set n} → Context → ( Code → Context → t ) → t |
| 128 Phil_thiking c next = next C_pickup_rfork c | |
| 709 | 129 |
| 712 | 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 { | |
| 716 | 132 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_lfork ; next = C_pickup_rfork } } where |
| 712 | 133 phil : Phil |
| 713 | 134 phil = Phil-API.impl ( Context.c_Phil-API c ) |
| 709 | 135 |
| 712 | 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 { | |
| 716 | 138 c_AtomicNat-API = record { impl = Phil.left phil ; value = Phil.ptr phil ; fail = C_pickup_rfork ; next = C_eating } } where |
| 712 | 139 phil : Phil |
| 713 | 140 phil = Phil-API.impl ( Context.c_Phil-API c ) |
| 709 | 141 |
| 712 | 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 | |
| 709 | 144 |
| 711 | 145 code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t |
| 713 | 146 code_table C_nop = λ c next → next C_nop c |
| 712 | 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 | |
| 636 | 154 |
|
720
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
155 |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
156 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
|
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 |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
158 p : ℕ → Phil |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
159 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
|
160 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
|
161 c1 [] = init-context |
|
e9d781c38629
Ok this is a termination bug og agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
719
diff
changeset
|
162 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
|
163 |
| 718 | 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 | |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
169 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
|
170 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
|
171 n : ℕ |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
172 n = Context.mbase c1 |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
173 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
|
174 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
|
175 mem : bt Data |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
176 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
|
177 $ λ t → t |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
178 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
|
179 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
|
180 $ λ t → t |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
181 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
|
182 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
|
183 $ λ t → t |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
184 |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
185 test-i0 : bt Data |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
186 test-i0 = Context.memory (init-Phil-1 init-context) |
| 718 | 187 |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
188 make-phil : ℕ → Context |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
189 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
|
190 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
|
191 |
|
721
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
192 test-i5 : bt Data |
|
2abfce56523a
init 5 phils done without infinite loop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
720
diff
changeset
|
193 test-i5 = Context.memory (make-phil 5) |
| 708 | 194 |
| 195 -- loop exexution | |
| 196 | |
| 197 -- concurrnt execution | |
| 198 | |
| 199 -- state db ( binary tree of processes ) | |
| 200 | |
| 722 | 201 -- depth first execution |
| 708 | 202 |
| 203 -- verify temporal logic poroerries | |
| 636 | 204 |
| 205 | |
| 206 |