diff --git a/ModelChecking_sol.v b/ModelChecking_sol.v new file mode 100644 index 0000000..68a50ea --- /dev/null +++ b/ModelChecking_sol.v @@ -0,0 +1,82 @@ +Theorem factorial_ok_2 : + invariantFor (factorial_sys 2) (fact_correct 2). +Proof. + simplify. + eapply invariant_weaken. + (* We begin like in last chapter, by strengthening to an inductive + * invariant. *) + + apply multiStepClosure_ok. + (* The difference is that we will use multi-step closure to find the invariant + * automatically. Note that the invariant appears as an existential variable, + * whose name begins with a question mark. *) + simplify. + rewrite fact_init_is. + (* It's important to phrase the current candidate invariant explicitly as a + * finite set, before continuing. Otherwise, it won't be obvious how to take + * the one-step closure. *) + + (* Compute which states are reachable after one step. *) + eapply MscStep. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_empty. + simplify. + + (* Compute which states are reachable after two steps. *) + eapply MscStep. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_empty. + simplify. + + (* Compute which states are reachable after three steps. *) + eapply MscStep. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_split; simplify. + invert H; simplify. + apply singleton_in. + apply oneStepClosure_empty. + simplify. + + (* Now the candidate invariatn is closed under single steps. Let's prove + * it. *) + apply MscDone. + apply prove_oneStepClosure; simplify. + propositional. + propositional; invert H0; try equality. + invert H; equality. + invert H1; equality. + + (* Finally, we prove that our new invariant implies the simpler, noninductive + * one that we started with. *) + simplify. + propositional; subst; simplify; propositional. + (* [subst]: remove all hypotheses like [x = e] for variables [x], simply + * replacing all uses of [x] by [e]. *) +Qed. + +Theorem twoadd2_ok : + invariantFor (parallel twoadd_sys twoadd_sys) (twoadd_correct (private := _)). +Proof. + eapply invariant_weaken. + eapply invariant_simulates. + apply withInterference_abstracts. + apply withInterference_parallel. + apply twoadd_ok. + apply twoadd_ok. + + unfold twoadd_correct. + invert 1. + assumption. +Qed. diff --git a/ModelChecking_template.v b/ModelChecking_template.v index 5dc619e..de13a25 100644 --- a/ModelChecking_template.v +++ b/ModelChecking_template.v @@ -410,6 +410,196 @@ Proof. Admitted. + + + + + + + + + + + + + + +Inductive add2_bthread := +| BRead +| BWrite (local : bool). + +Inductive add2_binit : threaded_state bool add2_bthread -> Prop := +| Add2BInit : add2_binit {| Shared := true; Private := BRead |}. + +Inductive add2_bstep : threaded_state bool add2_bthread -> threaded_state bool add2_bthread -> Prop := +| StepBRead : forall global, + add2_bstep {| Shared := global; Private := BRead |} + {| Shared := global; Private := BWrite global |} +| StepBWrite : forall global local, + add2_bstep {| Shared := global; Private := BWrite local |} + {| Shared := local; Private := BRead |}. + +Definition add2_bsys1 := {| + Initial := add2_binit; + Step := add2_bstep +|}. + +Definition add2_bsys := parallel add2_bsys1 add2_bsys1. + +(* This invariant formalizes the connection between local states of threads, in + * the original and abstracted systems. *) +Inductive R_private1 : add2_thread -> add2_bthread -> Prop := +| RpRead : R_private1 Read BRead +| RpWrite : forall n b, (b = true <-> isEven n) + -> R_private1 (Write n) (BWrite b). + +(* We lift [R_private1] to a relation over whole states. *) +Inductive add2_R : threaded_state nat (add2_thread * add2_thread) + -> threaded_state bool (add2_bthread * add2_bthread) + -> Prop := +| Add2_R : forall n b th1 th2 th1' th2', + (b = true <-> isEven n) + -> R_private1 th1 th1' + -> R_private1 th2 th2' + -> add2_R {| Shared := n; Private := (th1, th2) |} + {| Shared := b; Private := (th1', th2') |}. + +(* Let's also recharacterize the initial states via a singleton set. *) +Theorem add2_init_is : + parallel1 add2_binit add2_binit = { {| Shared := true; Private := (BRead, BRead) |} }. +Proof. + simplify. + apply sets_equal; simplify. + propositional. + + invert H. + invert H2. + invert H4. + equality. + + invert H0. + constructor. + constructor. + constructor. +Qed. + +(* We ask Coq to remember this lemma as a hint, which will be used by the + * model-checking tactics that we refrain from explaining in detail. *) +Hint Rewrite add2_init_is. + +(* Now, let's verify the original system. *) +(*Theorem add2_ok : + invariantFor add2_sys add2_correct. +Proof. + (* First step: strengthen the invariant. We leave an underscore for the + * unknown invariant, to be found by model checking. *) + eapply invariant_weaken with (invariant1 := invariantViaSimulation add2_R _). + + (* One way to find an invariant-by-simulation is to find an invariant for the + * abstracted system, as this step asks to do. *) + apply invariant_simulates with (sys2 := add2_bsys). + + (* Now we must prove that the simulation via [add2_R] is valid, which is + * routine. *) + constructor; simplify. + + invert H. + invert H0. + invert H1. + exists {| Shared := true; Private := (BRead, BRead) |}; simplify. + propositional. + constructor. + propositional. + constructor. + constructor. + constructor. + + invert H. + invert H0; simplify. + + invert H7. + + invert H2. + exists {| Shared := b; Private := (BWrite b, th2') |}. + propositional. + constructor. + propositional. + constructor. + propositional. + assumption. + constructor. + constructor. + + invert H2. + exists {| Shared := b0; Private := (BRead, th2') |}. + propositional. + constructor. + propositional. + constructor. + assumption. + invert H0. + propositional. + constructor. + assumption. + constructor. + constructor. + + invert H7. + + invert H3. + exists {| Shared := b; Private := (th1', BWrite b) |}. + propositional. + constructor. + propositional. + assumption. + constructor. + propositional. + constructor. + constructor. + + invert H3. + exists {| Shared := b0; Private := (th1', BRead) |}. + propositional. + constructor. + propositional. + constructor. + assumption. + invert H0. + propositional. + assumption. + constructor. + constructor. + constructor. + + (* OK, we're glad to have that over with! Such a process could also be + * automated, but we won't bother doing so here. However, we are now in a + * good state, where our model checker can find the invariant + * automatically. *) + model_check_infer. + (* It finds exactly four reachable states. We finish by showing that they all + * obey the original invariant. *) + + invert 1. + invert H0. + simplify. + unfold add2_correct. + simplify. + propositional; subst. + + invert H. + propositional. + + invert H1. + propositional. + + invert H. + propositional. + + invert H1. + propositional. +Qed.*) + + (** * Another abstraction example *) Inductive pc :=