Idris2Doc : Search.GCL

Search.GCL(source)

The content of this module is based on the paper
Applications of Applicative Proof Search
by Liam O'Connor
https://doi.org/10.1145/2976022.2976030

Reexports

import public Search.CTL

Definitions

weaken : Dec {_:6586} -> Bool
  Weaken a Dec to a Bool.

Totality: total
Visibility: public export
data GCL : Type -> Type
  Guarded Command Language

Totality: total
Visibility: public export
Constructors:
IF : (Sts : Type) -> List GUARD -> GCL
DOT : (Sts : Type) -> GCL -> GCL -> GCL
DO : (Sts : Type) -> List GUARD -> GCL
UPDATE : (Sts : Type) -> (Sts -> Sts) -> GCL
SKIP : (Sts : Type) -> GCL
  Termination

Hints:
(Sts : Type) -> Uninhabited (IF {_:6681} = SKIP)
(Sts : Type) -> Uninhabited (DOT {_:6706} {_:6705} = SKIP)
(Sts : Type) -> Uninhabited (DO {_:6734} = SKIP)
(Sts : Type) -> Uninhabited (UPDATE {_:6757} = SKIP)
Pred : Type -> Type
  A predicate

Totality: total
Visibility: public export
record GUARD : Type -> Type
  Guards are checks on the current state

Totality: total
Visibility: public export
Constructor: 
MkGUARD : (Sts : Type) -> Pred -> GCL -> GUARD

Projections:
.g : (Sts : Type) -> GUARD -> Pred
  The check to confirm
.x : (Sts : Type) -> GUARD -> GCL
  The current state

Hints:
(Sts : Type) -> Uninhabited (IF {_:6681} = SKIP)
(Sts : Type) -> Uninhabited (DO {_:6734} = SKIP)
.g : (Sts : Type) -> GUARD -> Pred
  The check to confirm

Totality: total
Visibility: public export
g : (Sts : Type) -> GUARD -> Pred
  The check to confirm

Totality: total
Visibility: public export
.x : (Sts : Type) -> GUARD -> GCL
  The current state

Totality: total
Visibility: public export
x : (Sts : Type) -> GUARD -> GCL
  The current state

Totality: total
Visibility: public export
isSkip : (Sts : Type) -> (l : GCL) -> Dec (l = SKIP)
  Prove that the given program terminated (i.e. reached a `SKIP`).

Totality: total
Visibility: public export
ops' : (Sts : Type) -> GCL -> Sts -> List (GCL, Sts)
  Operational semantics of GCL.
  (curried version to pass the termination checker)

Totality: total
Visibility: public export
ops : (Sts : Type) -> (GCL, Sts) -> List (GCL, Sts)
  Operational semantics of GCL.

Totality: total
Visibility: public export
gclToDiag : (Sts : Type) -> GCL -> Diagram GCL Sts
  We can convert a GCL program to a transition digram by using the program
  as the state and the operational semantics as the transition function.

Totality: total
Visibility: public export
while : (Sts : Type) -> Pred -> GCL -> GCL
  While loops are GCL do loops with a single guard.

Totality: total
Visibility: public export
await : (Sts : Type) -> Pred -> GCL
  Await halts progress unless the predicate is satisfied.

Totality: total
Visibility: public export
ifThenElse : (Sts : Type) -> Pred -> GCL -> GCL -> GCL
  If statements translate into GCL if statements by having an unmodified and
  a negated version of the predicate in the list of `IF` GCL statements.

Totality: total
Visibility: public export
record State : Type
Totality: total
Visibility: public export
Constructor: 
MkState : Bool -> Bool -> Nat -> Bool -> Bool -> State

Projections:
.inCS1 : State -> Bool
.inCS2 : State -> Bool
.intent1 : State -> Bool
.intent2 : State -> Bool
.turn : State -> Nat
.intent2 : State -> Bool
Totality: total
Visibility: public export
.intent1 : State -> Bool
Totality: total
Visibility: public export
intent2 : State -> Bool
Totality: total
Visibility: public export
intent1 : State -> Bool
Totality: total
Visibility: public export
.turn : State -> Nat
Totality: total
Visibility: public export
turn : State -> Nat
Totality: total
Visibility: public export
.inCS2 : State -> Bool
Totality: total
Visibility: public export
.inCS1 : State -> Bool
Totality: total
Visibility: public export
inCS2 : State -> Bool
Totality: total
Visibility: public export
inCS1 : State -> Bool
Totality: total
Visibility: public export
CS1 : GCL
  First critical section

Totality: total
Visibility: public export
CS2 : GCL
  Second critical section

Totality: total
Visibility: public export
petersons1 : GCL
  First Peterson's algorithm process

Totality: total
Visibility: public export
petersons2 : GCL
  Second Peterson's algorithm process

Totality: total
Visibility: public export
petersons : Diagram (GCL, GCL) State
  The parallel composition of the two Peterson's processes, to be
  model-checked.

Totality: total
Visibility: public export
IsTT : (b : Bool) -> Dec (So b)
  Type-level decider for booleans.

Totality: total
Visibility: public export
Mutex : Formula
  Mutual exclusion, i.e. both critical sections not simultaneously active.

Totality: total
Visibility: public export
checkMutex : MC Mutex
  Model-check (search) whether the mutex condition is satisfied.

Totality: total
Visibility: public export
SF : Formula
  Starvation freedom

Totality: total
Visibility: public export
checkSF : MC SF
  Model-check (search) whether starvation freedom holds.

Totality: total
Visibility: public export
Termination : Formula
  Deadlock freedom, aka. termination for all possible paths/traces

Totality: total
Visibility: public export
checkTermination : MC Termination
  Model-check (search) whether termination holds.

Totality: total
Visibility: public export
init : State
  Initial state for model-checking Peterson's algorithm.

Totality: total
Visibility: public export
tree : CT
  The computational tree for the two Peterson's processes.

Totality: total
Visibility: public export
CSP : Type
  The Critical Section Problem:
  1) a process's critical section (CS) is only ever accessed by that process
     and no other
  2) any process which wishes to gain access to its CS eventually
     does so
  3) the composition of the processes is deadlock free
     (we use a stronger requirement: that all process composition must
     terminate successfully)

Totality: total
Visibility: public export
checkPetersons : Prop (Nat :: Constraints) CSP
  A `Prop` (property) containing all the conditions necessary for proving that
  Peterson's Algorithm is a correct solution to the Critical Section Problem.
  When evaluated (e.g. through the `auto` search in a `Properties.check`
  call; specifically `runProp`), it will produce the required proof (which is
  **very** big).

Totality: total
Visibility: public export
dekkers1 : GCL
  First Dekker's algorithm process

Totality: total
Visibility: public export
dekkers2 : GCL
  First Dekker's algorithm process

Totality: total
Visibility: public export
dekkers : Diagram (GCL, GCL) State
  The parallel composition of the two Dekker's processes, to be model-checked.

Totality: total
Visibility: public export
checkDekkers : HDec (ExistsFinally ?f 100 (model dekkers init))
  An attempt at finding a violation of Mutual Exclusion.
  THIS WILL NOT FIND A PROOF due to the lack of fairness in the unfolding of
  the traces. Dekker's algorithm requires fair scheduling in order to be
  correct, but since we don't have that, we cannot find a proof that no
  violations of mutex exist.
  
  /!\ Trying to evaluate this did not finish after 10 minutes /!\

Totality: total
Visibility: public export