Search.GCL


   0 | ||| The content of this module is based on the paper
   1 | ||| Applications of Applicative Proof Search
   2 | ||| by Liam O'Connor
   3 | ||| https://doi.org/10.1145/2976022.2976030
   4 | 
   5 | module Search.GCL
   6 | 
   7 | import Data.So
   8 | import Data.Nat
   9 | import Data.Fuel
  10 | import Data.List.Lazy
  11 | import Data.List.Quantifiers
  12 | import Data.List.Lazy.Quantifiers
  13 | import Decidable.Equality
  14 | 
  15 | import public Search.CTL
  16 | 
  17 | %default total
  18 | 
  19 | ||| Weaken a Dec to a Bool.
  20 | public export
  21 | weaken : Dec _ -> Bool
  22 | weaken (Yes _) = True
  23 | weaken (No  _) = False
  24 | 
  25 | parameters (Sts : Type)
  26 | 
  27 |   ------------------------------------------------------------------------
  28 |   -- Types and operational semantics
  29 | 
  30 |   mutual
  31 |     ||| Guarded Command Language
  32 |     public export
  33 |     data GCL : Type where
  34 |       IF : (gs : List GUARD) -> GCL
  35 | 
  36 |       DOT : GCL -> GCL -> GCL
  37 | 
  38 |       DO : (gs : List GUARD) -> GCL
  39 | 
  40 |       UPDATE : (u : Sts -> Sts) -> GCL
  41 | 
  42 |       ||| Termination
  43 |       SKIP : GCL
  44 | 
  45 |     ||| A predicate
  46 |     public export
  47 |     Pred : Type
  48 |     Pred = (st : Sts) -> Bool
  49 | 
  50 |     ||| Guards are checks on the current state
  51 |     public export
  52 |     record GUARD where
  53 |       constructor MkGUARD
  54 |       ||| The check to confirm
  55 |       g : Pred
  56 |       ||| The current state
  57 |       x : GCL
  58 | 
  59 |   public export
  60 |   Uninhabited (IF _ === SKIP) where
  61 |     uninhabited Refl impossible
  62 | 
  63 |   public export
  64 |   Uninhabited (DOT _ _ === SKIP) where
  65 |     uninhabited Refl impossible
  66 | 
  67 |   public export
  68 |   Uninhabited (DO _ === SKIP) where
  69 |     uninhabited Refl impossible
  70 | 
  71 |   public export
  72 |   Uninhabited (UPDATE _ === SKIP) where
  73 |     uninhabited Refl impossible
  74 | 
  75 |   ||| Prove that the given program terminated (i.e. reached a `SKIP`).
  76 |   public export
  77 |   isSkip : (l : GCL) -> Dec (l === SKIP)
  78 |   isSkip (IF xs)     = No absurd
  79 |   isSkip (DOT y z)   = No absurd
  80 |   isSkip (DO xs)     = No absurd
  81 |   isSkip (UPDATE uf) = No absurd
  82 |   isSkip SKIP        = Yes Refl
  83 | 
  84 |   ||| Operational semantics of GCL.
  85 |   ||| (curried version to pass the termination checker)
  86 |   public export
  87 |   ops' : GCL -> Sts -> List (GCL, Sts)
  88 |   ops' SKIP st = []
  89 |   ops' (UPDATE u) st = [(SKIP, u st)]
  90 |   ops' (DOT SKIP y) st = [(y, st)]
  91 |   ops' (DOT x y) st = mapFst (`DOT` y) <$> ops' x st
  92 |   ops' (IF gs) st = map (\ aGuard => (aGuard.x, st)) $
  93 |                     filter (\ aGuard => aGuard.g st) gs
  94 | 
  95 |   ops' (DO gs) st with (map (\ aG => ((DOT aG.x (DO gs)), st)) $
  96 |                         filter (\ aG => aG.g st) gs)
  97 |     _ | [] = [(SKIP, st)]
  98 |     _ | ys = ys
  99 | 
 100 |   ||| Operational semantics of GCL.
 101 |   public export
 102 |   ops : (GCL, Sts) -> List (GCL, Sts)
 103 |   ops (l, st) = ops' l st
 104 | 
 105 |   ||| We can convert a GCL program to a transition digram by using the program
 106 |   ||| as the state and the operational semantics as the transition function.
 107 |   public export
 108 |   gclToDiag : GCL -> Diagram GCL Sts
 109 |   gclToDiag p = TD ops p
 110 | 
 111 | 
 112 |   ------------------------------------------------------------------------
 113 |   -- Control Structures
 114 | 
 115 |   ||| While loops are GCL do loops with a single guard.
 116 |   public export
 117 |   while : Pred -> GCL -> GCL
 118 |   while g x = DO [MkGUARD g x]
 119 | 
 120 |   ||| Await halts progress unless the predicate is satisfied.
 121 |   public export
 122 |   await : Pred -> GCL
 123 |   await g = IF [MkGUARD g SKIP]
 124 | 
 125 |   ||| If statements translate into GCL if statements by having an unmodified and
 126 |   ||| a negated version of the predicate in the list of `IF` GCL statements.
 127 |   public export
 128 |   ifThenElse : (g : Pred) -> (x : GCL) -> (y : GCL) -> GCL
 129 |   ifThenElse g x y = IF [MkGUARD g x, MkGUARD (not . g) y]
 130 | 
 131 | 
 132 | ------------------------------------------------------------------------
 133 | -- Example: Peterson's Algorithm
 134 | 
 135 | public export
 136 | record State where
 137 |   constructor MkState
 138 |   -- shared state: intent1, intent2, and turn
 139 |   intent1, intent2 : Bool
 140 |   turn : Nat
 141 |   -- is the current state in its critical section?
 142 |   inCS1, inCS2 : Bool
 143 | 
 144 | ||| First critical section
 145 | public export
 146 | CS1 : GCL State
 147 | CS1 =
 148 |   DOT State
 149 |     (UPDATE State (\st => { inCS1 := True } st))
 150 |     (DOT State
 151 |       (SKIP State)
 152 |       (UPDATE State (\st => { inCS1 := False } st))
 153 |       )
 154 | 
 155 | ||| Second critical section
 156 | public export
 157 | CS2 : GCL State
 158 | CS2 =
 159 |   DOT State
 160 |     (UPDATE State (\st => { inCS2 := True } st))
 161 |     (DOT State
 162 |       (SKIP State)
 163 |       (UPDATE State (\st => { inCS2 := False } st))
 164 |       )
 165 | 
 166 | ||| First Peterson's algorithm process
 167 | public export
 168 | petersons1 : GCL State
 169 | petersons1 =
 170 |   DOT State
 171 |     (UPDATE State (\st => { intent1 := True } st))
 172 |     (DOT State
 173 |       (UPDATE State (\st => { turn := 1 } st))
 174 |       (DOT State
 175 |         (await State (\st => (not st.intent2) || (weaken (decEq st.turn 0))))
 176 |         (DOT State
 177 |           CS1
 178 |           (UPDATE State (\st => { intent1 := False } st))
 179 |           )))
 180 | 
 181 | ||| Second Peterson's algorithm process
 182 | public export
 183 | petersons2 : GCL State
 184 | petersons2 =
 185 |   DOT State
 186 |     (UPDATE State (\st => { intent2 := True } st))
 187 |     (DOT State
 188 |       (UPDATE State (\st => { turn := 0 } st))
 189 |       (DOT State
 190 |         (await State (\st => (not st.intent1) || (weaken (decEq st.turn 1))))
 191 |         (DOT State
 192 |           CS2
 193 |           (UPDATE State (\st => { intent2 := False } st))
 194 |           )))
 195 | 
 196 | ||| The parallel composition of the two Peterson's processes, to be
 197 | ||| model-checked.
 198 | public export
 199 | petersons : Diagram (GCL State, GCL State) State
 200 | petersons = (gclToDiag State petersons1) `pComp` (gclToDiag State petersons2)
 201 | 
 202 | 
 203 | ------------------------------------------------------------------------
 204 | -- Properties to verify
 205 | 
 206 | ||| Type-level decider for booleans.
 207 | public export
 208 | IsTT : (b : Bool) -> Dec (So b)
 209 | IsTT True = Yes Oh
 210 | IsTT False = No absurd
 211 | 
 212 | 
 213 | ||| Mutual exclusion, i.e. both critical sections not simultaneously active.
 214 | public export
 215 | Mutex : Formula ? ?
 216 | Mutex =
 217 |   AlwaysGlobal (GCL State, GCL State) State
 218 |       (Guarded (GCL State, GCL State) State
 219 |           (\p,_ => So (not (p.inCS1 && p.inCS2))))
 220 | 
 221 | ||| Model-check (search) whether the mutex condition is satisfied.
 222 | public export
 223 | checkMutex : MC (GCL State, GCL State) State Mutex
 224 | checkMutex =
 225 |   agSearch (GCL State, GCL State) State
 226 |       (now (GCL State, GCL State) State
 227 |           (\p,_ => fromDec $ IsTT _))
 228 |                               --  ^ (not (p .inCS1 && (Delay (p .inCS2)))
 229 | 
 230 | ||| Starvation freedom
 231 | public export
 232 | SF : Formula ? ?
 233 | SF =
 234 |   let guardCS1 = Guarded (GCL State, GCL State) State (\p,_ => So (p.inCS1))
 235 |       guardCS2 = Guarded (GCL State, GCL State) State (\p,_ => So (p.inCS2))
 236 |   in AND' (GCL State, GCL State) State
 237 |       (AlwaysFinally (GCL State, GCL State) State guardCS1)
 238 |       (AlwaysFinally (GCL State, GCL State) State guardCS2)
 239 | 
 240 | ||| Model-check (search) whether starvation freedom holds.
 241 | public export
 242 | checkSF : MC (GCL State, GCL State) State SF
 243 | checkSF =
 244 |   let mcAndFst = afSearch (GCL State, GCL State) State
 245 |                      (now (GCL State, GCL State) State
 246 |                         (\p,_ => fromDec $ IsTT _))
 247 |                                      -- p.inCS1 ^
 248 |       mcAndSnd = afSearch (GCL State, GCL State) State
 249 |                      (now (GCL State, GCL State) State
 250 |                         (\p,_ => fromDec $ IsTT _))
 251 |                                      -- p.inCS2 ^
 252 |   in mcAND' (GCL State, GCL State) State mcAndFst mcAndSnd
 253 | 
 254 | 
 255 | ||| Deadlock freedom, aka. termination for all possible paths/traces
 256 | public export
 257 | Termination : Formula ? ?
 258 | Termination =
 259 |   AlwaysFinally (GCL State, GCL State) State
 260 |        (Guarded (GCL State, GCL State) State
 261 |           (\_,l => allSkip l))
 262 |   where
 263 |     allSkip : (l : (GCL State, GCL State)) -> Type
 264 |     allSkip l = (fst l === SKIP State, snd l === SKIP State)
 265 | 
 266 | ||| Model-check (search) whether termination holds.
 267 | public export
 268 | checkTermination : MC (GCL State, GCL State) State Termination
 269 | checkTermination =
 270 |   afSearch (GCL State, GCL State) State
 271 |       (now (GCL State, GCL State) State
 272 |           (\_,l => MkHDec (isTerm l) (sound l)))
 273 |   where
 274 |     -- l should be auto-implicit, but we can't search for that here
 275 |     isTerm : (l : (GCL State, GCL State)) -> Bool
 276 |     isTerm (a, b) =
 277 |       (weaken $ isSkip State a) && (weaken $ isSkip State b)
 278 | 
 279 |     sound :  (l : (GCL State, GCL State))
 280 |           -> So (isTerm l)
 281 |           -> (fst l === SKIP State, snd l === SKIP State)
 282 |     sound (a, b) _ with (isSkip State a) | (isSkip State b)
 283 |       sound (a, b) _  | (Yes p) | (Yes q) = (p, q)
 284 |       sound (a, b) Oh | (Yes p) | (No _)  impossible
 285 |       sound (a, b) Oh | (No _)  | _       impossible
 286 | 
 287 | 
 288 | ||| Initial state for model-checking Peterson's algorithm.
 289 | public export
 290 | init : State
 291 | init = MkState False False 0 False False
 292 |         -- intent1 intent2 turn inCS1 inCS2
 293 | 
 294 | ||| The computational tree for the two Peterson's processes.
 295 | public export
 296 | tree : CT (GCL State, GCL State) State
 297 | tree = model (GCL State, GCL State) State petersons init
 298 | 
 299 | ||| The Critical Section Problem:
 300 | ||| 1) a process's critical section (CS) is only ever accessed by that process
 301 | |||    and no other
 302 | ||| 2) any process which wishes to gain access to its CS eventually
 303 | |||    does so
 304 | ||| 3) the composition of the processes is deadlock free
 305 | |||    (we use a stronger requirement: that all process composition must
 306 | |||    terminate successfully)
 307 | public export
 308 | CSP : Type
 309 | CSP = (arg : Nat **
 310 |         AND' (GCL State, GCL State) State
 311 |           (\depth, tree => Mutex depth tree)              -- mutually exclusive
 312 |           (\depth, tree =>
 313 |             AND' (GCL State, GCL State) State
 314 |               (\depth, tree => SF depth tree)             -- starvation free
 315 |               (\depth, tree => Termination depth tree)    -- completed
 316 |               depth tree)
 317 |         arg GCL.tree)
 318 | 
 319 | ||| A `Prop` (property) containing all the conditions necessary for proving that
 320 | ||| Peterson's Algorithm is a correct solution to the Critical Section Problem.
 321 | ||| When evaluated (e.g. through the `auto` search in a `Properties.check`
 322 | ||| call; specifically `runProp`), it will produce the required proof (which is
 323 | ||| **very** big).
 324 | public export
 325 | checkPetersons : Prop ? CSP
 326 | checkPetersons = exists $
 327 |                   (mcAND' (GCL State, GCL State) State
 328 |                     checkMutex
 329 |                     (mcAND' (GCL State, GCL State) State
 330 |                       checkSF
 331 |                       checkTermination
 332 |                       ))
 333 |                    tree
 334 | 
 335 | 
 336 | {- N.B.: commenting this in causes the type-checking of this file to take ~2
 337 |  -       minutes and ~4 GB of RAM
 338 |  -
 339 | 
 340 | ||| Prove that Peterson's Algorithm is a solution to the Critical Section
 341 | ||| Problem. This evaluates the `checkPetersons` property to obtain a proof (at
 342 | ||| a search depth of 1000!), at which point we can show that it is
 343 | ||| depth-invariant.
 344 | |||
 345 | ||| /!\       CAUTION: THIS IS **EXTREMELY** SLOW + RESOURCE INTENSIVE       /!\
 346 | ||| /!\ Attempt at evaluation did not complete after 3hrs and 57.6 GB of RAM /!\
 347 | public export
 348 | petersonsCorrect : Models ? ?
 349 |                     GCL.tree
 350 |                     (AND' ? ?
 351 |                       Mutex
 352 |                       (AND' ? ?
 353 |                         SF
 354 |                         Termination
 355 |                         ))
 356 | petersonsCorrect =
 357 |   diModels (GCL State, GCL State) State
 358 |            (snd (check @{%search} (limit 1000) checkPetersons @{Oh}))
 359 | 
 360 |  -}
 361 | 
 362 | 
 363 | 
 364 | ------------------------------------------------------------------------
 365 | -- Example: Dekker's Algorithm
 366 | 
 367 | ||| First Dekker's algorithm process
 368 | public export
 369 | dekkers1 : GCL State
 370 | dekkers1 =
 371 |   DOT _
 372 |     (UPDATE _ (\st => { intent1 := True } st))
 373 |     (DOT _
 374 |       (while _ (\st => st.intent2)
 375 |         (IF _ [ (MkGUARD _ (\st => weaken $ decEq st.turn 0) (SKIP _))
 376 |               , (MkGUARD _ (\st => weaken $ decEq st.turn 1)
 377 |                            (DOT _
 378 |                             (UPDATE _ (\st => { intent1 := False } st))
 379 |                             (DOT _
 380 |                               (await _ (\st => weaken $ decEq st.turn 0))
 381 |                               (UPDATE _ (\st => { intent1 := True } st))
 382 |                               )))
 383 |               ]
 384 |         ))
 385 |         (DOT _
 386 |           CS1
 387 |           (DOT _
 388 |             (UPDATE _ (\st => { turn := 1 } st))
 389 |             (UPDATE _ (\st => { intent1 := False } st))
 390 |     )))
 391 | 
 392 | ||| First Dekker's algorithm process
 393 | public export
 394 | dekkers2 : GCL State
 395 | dekkers2 =
 396 |   DOT _
 397 |     (UPDATE _ (\st => { intent2 := True } st))
 398 |     (DOT _
 399 |       (while _ (\st => st.intent1)
 400 |         (IF _ [ (MkGUARD _ (\st => weaken $ decEq st.turn 1) (SKIP _))
 401 |               , (MkGUARD _ (\st => weaken $ decEq st.turn 0)
 402 |                            (DOT _
 403 |                             (UPDATE _ (\st => { intent2 := False } st))
 404 |                             (DOT _
 405 |                               (await _ (\st => weaken $ decEq st.turn 1))
 406 |                               (UPDATE _ (\st => { intent2 := True } st))
 407 |                               )))
 408 |               ]
 409 |         ))
 410 |         (DOT _
 411 |           CS2
 412 |           (DOT _
 413 |             (UPDATE _ (\st => { turn := 0 } st))
 414 |             (UPDATE _ (\st => { intent2 := False } st))
 415 |     )))
 416 | 
 417 | ||| The parallel composition of the two Dekker's processes, to be model-checked.
 418 | public export
 419 | dekkers : Diagram (GCL State, GCL State) State
 420 | dekkers = (gclToDiag _ dekkers1) `pComp` (gclToDiag _ dekkers2)
 421 | 
 422 | ||| An attempt at finding a violation of Mutual Exclusion.
 423 | ||| THIS WILL NOT FIND A PROOF due to the lack of fairness in the unfolding of
 424 | ||| the traces. Dekker's algorithm requires fair scheduling in order to be
 425 | ||| correct, but since we don't have that, we cannot find a proof that no
 426 | ||| violations of mutex exist.
 427 | |||
 428 | ||| /!\ Trying to evaluate this did not finish after 10 minutes /!\
 429 | public export
 430 | checkDekkers : HDec ?
 431 | checkDekkers =
 432 |   efSearch _ _
 433 |     (now _ _ (\p, _ => (fromDec $ IsTT (p.inCS1 && p.inCS2))))
 434 |     (model _ _ dekkers init) 100
 435 | 
 436 |