mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
Revising before class, including with an optimization to the model-checking engine
This commit is contained in:
parent
c607913898
commit
69de20dec8
4 changed files with 53 additions and 45 deletions
|
@ -318,22 +318,8 @@ Ltac closure :=
|
||||||
repeat (apply oneStepClosure_empty
|
repeat (apply oneStepClosure_empty
|
||||||
|| (apply oneStepClosure_split; [ model_check_invert; try equality; solve [ singletoner ] | ])).
|
|| (apply oneStepClosure_split; [ model_check_invert; try equality; solve [ singletoner ] | ])).
|
||||||
|
|
||||||
Ltac model_check_done :=
|
Ltac model_check_done := apply MscDone.
|
||||||
apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].
|
Ltac model_check_step := eapply MscStep; [ closure | simplify ].
|
||||||
|
|
||||||
Ltac model_check_step0 :=
|
|
||||||
eapply MscStep; [ closure | simplify ].
|
|
||||||
|
|
||||||
Ltac model_check_step :=
|
|
||||||
match goal with
|
|
||||||
| [ |- multiStepClosure _ ?inv1 _ _ ] =>
|
|
||||||
model_check_step0;
|
|
||||||
match goal with
|
|
||||||
| [ |- multiStepClosure _ ?inv2 _ _ ] =>
|
|
||||||
(assert (inv1 = inv2) by compare_sets; fail 3)
|
|
||||||
|| idtac
|
|
||||||
end
|
|
||||||
end.
|
|
||||||
|
|
||||||
Ltac model_check_steps1 := model_check_step || model_check_done.
|
Ltac model_check_steps1 := model_check_step || model_check_done.
|
||||||
Ltac model_check_steps := repeat model_check_steps1.
|
Ltac model_check_steps := repeat model_check_steps1.
|
||||||
|
|
56
ModelCheck.v
56
ModelCheck.v
|
@ -1,4 +1,4 @@
|
||||||
Require Import Invariant Relations Sets.
|
Require Import Invariant Relations Sets Classical.
|
||||||
|
|
||||||
Set Implicit Arguments.
|
Set Implicit Arguments.
|
||||||
|
|
||||||
|
@ -27,35 +27,57 @@ Proof.
|
||||||
unfold oneStepClosure; tauto.
|
unfold oneStepClosure; tauto.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Theorem oneStepClosure_done : forall state (sys : trsys state) (invariant : state -> Prop),
|
|
||||||
(forall st, sys.(Initial) st -> invariant st)
|
|
||||||
-> oneStepClosure sys invariant invariant
|
|
||||||
-> invariantFor sys invariant.
|
|
||||||
Proof.
|
|
||||||
unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new.
|
|
||||||
intuition eauto using invariant_induction.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Inductive multiStepClosure {state} (sys : trsys state)
|
Inductive multiStepClosure {state} (sys : trsys state)
|
||||||
: (state -> Prop) -> (state -> Prop) -> (state -> Prop) -> Prop :=
|
: (state -> Prop) -> (state -> Prop) -> (state -> Prop) -> Prop :=
|
||||||
| MscDone : forall inv worklist,
|
| MscDone : forall inv,
|
||||||
oneStepClosure sys inv inv
|
multiStepClosure sys inv (constant nil) inv
|
||||||
-> multiStepClosure sys inv worklist inv
|
|
||||||
| MscStep : forall inv worklist inv' inv'',
|
| MscStep : forall inv worklist inv' inv'',
|
||||||
oneStepClosure sys worklist inv'
|
oneStepClosure sys worklist inv'
|
||||||
-> multiStepClosure sys (inv \cup inv') (inv' \setminus inv) inv''
|
-> multiStepClosure sys (inv \cup inv') (inv' \setminus inv) inv''
|
||||||
-> multiStepClosure sys inv worklist inv''.
|
-> multiStepClosure sys inv worklist inv''.
|
||||||
|
|
||||||
|
Lemma adding_irrelevant : forall A (s : A) inv inv',
|
||||||
|
s \in (inv \cup inv') \setminus (inv' \setminus inv)
|
||||||
|
-> s \in inv.
|
||||||
|
Proof.
|
||||||
|
sets idtac.
|
||||||
|
destruct (classic (inv s)); tauto.
|
||||||
|
Qed.
|
||||||
|
|
||||||
Lemma multiStepClosure_ok' : forall state (sys : trsys state) (inv worklist inv' : state -> Prop),
|
Lemma multiStepClosure_ok' : forall state (sys : trsys state) (inv worklist inv' : state -> Prop),
|
||||||
multiStepClosure sys inv worklist inv'
|
multiStepClosure sys inv worklist inv'
|
||||||
-> (forall st, sys.(Initial) st -> inv st)
|
-> (forall st, sys.(Initial) st -> inv st)
|
||||||
|
-> worklist \subseteq inv
|
||||||
|
-> (forall s, s \in inv \setminus worklist
|
||||||
|
-> forall s', sys.(Step) s s'
|
||||||
|
-> s' \in inv)
|
||||||
-> invariantFor sys inv'.
|
-> invariantFor sys inv'.
|
||||||
Proof.
|
Proof.
|
||||||
induction 1; simpl; intuition eauto using oneStepClosure_done.
|
induction 1; simpl; intuition.
|
||||||
|
|
||||||
apply IHmultiStepClosure.
|
apply invariant_induction; simpl; intuition.
|
||||||
|
eapply H1.
|
||||||
|
red.
|
||||||
|
unfold minus.
|
||||||
|
split; eauto.
|
||||||
|
assumption.
|
||||||
|
|
||||||
|
apply IHmultiStepClosure; clear IHmultiStepClosure.
|
||||||
intuition.
|
intuition.
|
||||||
apply H1 in H2.
|
apply H1 in H4.
|
||||||
|
sets idtac.
|
||||||
|
sets idtac.
|
||||||
|
intuition.
|
||||||
|
apply adding_irrelevant in H4.
|
||||||
|
destruct (classic (s \in worklist)).
|
||||||
|
destruct H.
|
||||||
|
red in H7.
|
||||||
|
eapply H7 in H6.
|
||||||
|
right; eassumption.
|
||||||
|
assumption.
|
||||||
|
left.
|
||||||
|
eapply H3.
|
||||||
|
2: eassumption.
|
||||||
sets idtac.
|
sets idtac.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
@ -63,7 +85,7 @@ Theorem multiStepClosure_ok : forall state (sys : trsys state) (inv : state -> P
|
||||||
multiStepClosure sys sys.(Initial) sys.(Initial) inv
|
multiStepClosure sys sys.(Initial) sys.(Initial) inv
|
||||||
-> invariantFor sys inv.
|
-> invariantFor sys inv.
|
||||||
Proof.
|
Proof.
|
||||||
eauto using multiStepClosure_ok'.
|
intros; eapply multiStepClosure_ok'; eauto; sets idtac.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Theorem oneStepClosure_empty : forall state (sys : trsys state),
|
Theorem oneStepClosure_empty : forall state (sys : trsys state),
|
||||||
|
|
|
@ -149,6 +149,7 @@ Proof.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
|
model_check_step.
|
||||||
model_check_done.
|
model_check_done.
|
||||||
|
|
||||||
simplify.
|
simplify.
|
||||||
|
@ -383,6 +384,7 @@ Proof.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
|
model_check_step.
|
||||||
model_check_done.
|
model_check_done.
|
||||||
|
|
||||||
simplify.
|
simplify.
|
||||||
|
@ -433,6 +435,7 @@ Proof.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
model_check_step.
|
model_check_step.
|
||||||
|
model_check_step.
|
||||||
model_check_done.
|
model_check_done.
|
||||||
|
|
||||||
simplify.
|
simplify.
|
||||||
|
@ -540,7 +543,7 @@ Inductive stepC (s : summary) : heap * locks * cmd -> heap * locks * cmd -> Pro
|
||||||
* with [c0]. *)
|
* with [c0]. *)
|
||||||
|
|
||||||
-> step (h, l, c1) (h'', l'', c1'')
|
-> step (h, l, c1) (h'', l'', c1'')
|
||||||
(* Finaly, [c] is actually enabled to run, which
|
(* Finally, [c] is actually enabled to run, which
|
||||||
* might not be the case if [c0] is a locking
|
* might not be the case if [c0] is a locking
|
||||||
* command. *)
|
* command. *)
|
||||||
|
|
||||||
|
@ -1371,11 +1374,8 @@ Ltac por_closure :=
|
||||||
repeat (apply oneStepClosure_empty
|
repeat (apply oneStepClosure_empty
|
||||||
|| (apply oneStepClosure_split; [ por_invert; try equality; solve [ singletoner ] | ])).
|
|| (apply oneStepClosure_split; [ por_invert; try equality; solve [ singletoner ] | ])).
|
||||||
|
|
||||||
Ltac por_step :=
|
Ltac por_step := eapply MscStep; [ por_closure | simplify ].
|
||||||
eapply MscStep; [ por_closure | simplify ].
|
Ltac por_done := apply MscDone.
|
||||||
|
|
||||||
Ltac por_done :=
|
|
||||||
apply MscDone; eapply oneStepClosure_solve; [ por_closure | simplify; solve [ sets ] ].
|
|
||||||
|
|
||||||
(* OK, ready to return to our last example! This time we will see state-space
|
(* OK, ready to return to our last example! This time we will see state-space
|
||||||
* exploration that steps a single thread at a time, where the final invariant
|
* exploration that steps a single thread at a time, where the final invariant
|
||||||
|
@ -1405,7 +1405,7 @@ Proof.
|
||||||
por_step.
|
por_step.
|
||||||
por_step.
|
por_step.
|
||||||
por_step.
|
por_step.
|
||||||
|
por_step.
|
||||||
por_done.
|
por_done.
|
||||||
|
|
||||||
sets.
|
sets.
|
||||||
|
|
|
@ -4533,9 +4533,9 @@ $$\infer{\summ{\mt{Lock} \; a}{(r, w, \ell)}}{
|
||||||
a \in \ell
|
a \in \ell
|
||||||
}$$
|
}$$
|
||||||
|
|
||||||
$$\infer{\summ{c_1 || c_2}{(r, w, \ell)}}{
|
$$\infer{\summ{c_1 || c_2}{s}}{
|
||||||
\summ{c_1}{(r, w, \ell)}
|
\summ{c_1}{s}
|
||||||
& \summ{c_1}{(r, w, \ell)}
|
& \summ{c_2}{s}
|
||||||
}$$
|
}$$
|
||||||
|
|
||||||
\newcommand{\na}[1]{\mt{nextAction}(#1)}
|
\newcommand{\na}[1]{\mt{nextAction}(#1)}
|
||||||
|
@ -4684,7 +4684,7 @@ The key insights of the prior section can be adapted to prove soundness of a who
|
||||||
In general, we apply the optimization to remove edges from a state-space graph, whose nodes are states and whose edges are labeled with \emph{actions} $\alpha$.
|
In general, we apply the optimization to remove edges from a state-space graph, whose nodes are states and whose edges are labeled with \emph{actions} $\alpha$.
|
||||||
In our setting, $\alpha$ is the identifier of the thread scheduled to run next.
|
In our setting, $\alpha$ is the identifier of the thread scheduled to run next.
|
||||||
To do model checking, the graph need not be materialized in memory in one go.
|
To do model checking, the graph need not be materialized in memory in one go.
|
||||||
Instead, as an optimization, the graph tends to be constructed on the fly, during state-space exploration.
|
Instead, as an optimization, the graph tends to be constructed on-the-fly, during state-space exploration.
|
||||||
|
|
||||||
The proofs from the last two sections only apply to check the invariant that no thread is about to fail.
|
The proofs from the last two sections only apply to check the invariant that no thread is about to fail.
|
||||||
However, the results easily generalize to arbitrary \emph{safety properties}\index{safety properties}, which can be expressed as decidable invariants on states.
|
However, the results easily generalize to arbitrary \emph{safety properties}\index{safety properties}, which can be expressed as decidable invariants on states.
|
||||||
|
@ -4721,7 +4721,7 @@ What happens if we add them back in?
|
||||||
Consider this program:
|
Consider this program:
|
||||||
$$(\mt{while} \; (\mt{true}) \; \{ \; \mt{Write} \; 0 \; 0 \; \}) \; || \; (n \leftarrow \mt{Read} \; 1; \mt{Fail})$$
|
$$(\mt{while} \; (\mt{true}) \; \{ \; \mt{Write} \; 0 \; 0 \; \}) \; || \; (n \leftarrow \mt{Read} \; 1; \mt{Fail})$$
|
||||||
An optimization in the spirit of our original from the prior section would happily decree that it is safe always to pick the first thread to run.
|
An optimization in the spirit of our original from the prior section would happily decree that it is safe always to pick the first thread to run.
|
||||||
This reduced state transition system never gets around to running the second thread, so exploring the state space never finds the failure!
|
This reduced state-transition system never gets around to running the second thread, so exploring the state space never finds the failure!
|
||||||
To plug this soundness hole, we add a final condition on the ample sets.
|
To plug this soundness hole, we add a final condition on the ample sets.
|
||||||
|
|
||||||
\begin{description}
|
\begin{description}
|
||||||
|
|
Loading…
Reference in a new issue