weaken : Dec {_:6598} -> Bool
Weaken a Dec to a Bool.
Totality: total
Visibility: public exportdata 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 {_:6693} = SKIP)
(Sts : Type) -> Uninhabited (DOT {_:6718} {_:6717} = SKIP)
(Sts : Type) -> Uninhabited (DO {_:6746} = SKIP)
(Sts : Type) -> Uninhabited (UPDATE {_:6769} = SKIP)
Pred : Type -> Type
A predicate
Totality: total
Visibility: public exportrecord 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 {_:6693} = SKIP)
(Sts : Type) -> Uninhabited (DO {_:6746} = SKIP)
.g : (Sts : Type) -> GUARD -> Pred
The check to confirm
Totality: total
Visibility: public exportg : (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 exportx : (Sts : Type) -> GUARD -> GCL
The current state
Totality: total
Visibility: public exportisSkip : (Sts : Type) -> (l : GCL) -> Dec (l = SKIP)
Prove that the given program terminated (i.e. reached a `SKIP`).
Totality: total
Visibility: public exportops' : (Sts : Type) -> GCL -> Sts -> List (GCL, Sts)
Operational semantics of GCL.
(curried version to pass the termination checker)
Totality: total
Visibility: public exportops : (Sts : Type) -> (GCL, Sts) -> List (GCL, Sts)
Operational semantics of GCL.
Totality: total
Visibility: public exportgclToDiag : (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 exportwhile : (Sts : Type) -> Pred -> GCL -> GCL
While loops are GCL do loops with a single guard.
Totality: total
Visibility: public exportawait : (Sts : Type) -> Pred -> GCL
Await halts progress unless the predicate is satisfied.
Totality: total
Visibility: public exportifThenElse : (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 exportrecord 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 exportCS2 : GCL
Second critical section
Totality: total
Visibility: public exportpetersons1 : GCL
First Peterson's algorithm process
Totality: total
Visibility: public exportpetersons2 : GCL
Second Peterson's algorithm process
Totality: total
Visibility: public exportpetersons : Diagram (GCL, GCL) State
The parallel composition of the two Peterson's processes, to be
model-checked.
Totality: total
Visibility: public exportIsTT : (b : Bool) -> Dec (So b)
Type-level decider for booleans.
Totality: total
Visibility: public exportMutex : Formula
Mutual exclusion, i.e. both critical sections not simultaneously active.
Totality: total
Visibility: public exportcheckMutex : MC Mutex
Model-check (search) whether the mutex condition is satisfied.
Totality: total
Visibility: public exportSF : Formula
Starvation freedom
Totality: total
Visibility: public exportcheckSF : MC SF
Model-check (search) whether starvation freedom holds.
Totality: total
Visibility: public exportTermination : Formula
Deadlock freedom, aka. termination for all possible paths/traces
Totality: total
Visibility: public exportcheckTermination : MC Termination
Model-check (search) whether termination holds.
Totality: total
Visibility: public exportinit : State
Initial state for model-checking Peterson's algorithm.
Totality: total
Visibility: public exporttree : CT
The computational tree for the two Peterson's processes.
Totality: total
Visibility: public exportCSP : 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 exportcheckPetersons : 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 exportdekkers1 : GCL
First Dekker's algorithm process
Totality: total
Visibility: public exportdekkers2 : GCL
First Dekker's algorithm process
Totality: total
Visibility: public exportdekkers : Diagram (GCL, GCL) State
The parallel composition of the two Dekker's processes, to be model-checked.
Totality: total
Visibility: public exportcheckDekkers : 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