From 69de20dec86597534052615349203477b3612bc3 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Mon, 20 Apr 2020 11:56:23 -0400
Subject: [PATCH] Revising before class, including with an optimization to the
 model-checking engine

---
 FrapWithoutSets.v | 18 ++-------------
 ModelCheck.v      | 56 +++++++++++++++++++++++++++++++++--------------
 SharedMemory.v    | 14 ++++++------
 frap_book.tex     | 10 ++++-----
 4 files changed, 53 insertions(+), 45 deletions(-)

diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v
index bd2ac72..e68f595 100644
--- a/FrapWithoutSets.v
+++ b/FrapWithoutSets.v
@@ -318,22 +318,8 @@ Ltac closure :=
   repeat (apply oneStepClosure_empty
           || (apply oneStepClosure_split; [ model_check_invert; try equality; solve [ singletoner ] | ])).
 
-Ltac model_check_done :=
-  apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].
-
-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_done := apply MscDone.
+Ltac model_check_step := eapply MscStep; [ closure | simplify ].
 
 Ltac model_check_steps1 := model_check_step || model_check_done.
 Ltac model_check_steps := repeat model_check_steps1.
diff --git a/ModelCheck.v b/ModelCheck.v
index cd77e36..594894b 100644
--- a/ModelCheck.v
+++ b/ModelCheck.v
@@ -1,4 +1,4 @@
-Require Import Invariant Relations Sets.
+Require Import Invariant Relations Sets Classical.
 
 Set Implicit Arguments.
 
@@ -27,35 +27,57 @@ Proof.
   unfold oneStepClosure; tauto.
 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)
   : (state -> Prop) -> (state -> Prop) -> (state -> Prop) -> Prop :=
-| MscDone : forall inv worklist,
-    oneStepClosure sys inv inv
-    -> multiStepClosure sys inv worklist inv
+| MscDone : forall inv,
+    multiStepClosure sys inv (constant nil) inv
 | MscStep : forall inv worklist inv' inv'',
     oneStepClosure sys worklist inv'
     -> multiStepClosure sys (inv \cup inv') (inv' \setminus inv) 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),
   multiStepClosure sys inv worklist inv'
   -> (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'.
 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.
-  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.
 Qed.
 
@@ -63,7 +85,7 @@ Theorem multiStepClosure_ok : forall state (sys : trsys state) (inv : state -> P
   multiStepClosure sys sys.(Initial) sys.(Initial) inv
   -> invariantFor sys inv.
 Proof.
-  eauto using multiStepClosure_ok'.
+  intros; eapply multiStepClosure_ok'; eauto; sets idtac.
 Qed.
 
 Theorem oneStepClosure_empty : forall state (sys : trsys state),
diff --git a/SharedMemory.v b/SharedMemory.v
index 1b97263..3552e1a 100644
--- a/SharedMemory.v
+++ b/SharedMemory.v
@@ -149,6 +149,7 @@ Proof.
   model_check_step.
   model_check_step.
   model_check_step.
+  model_check_step.
   model_check_done.
 
   simplify.
@@ -383,6 +384,7 @@ Proof.
   model_check_step.
   model_check_step.
   model_check_step.
+  model_check_step.
   model_check_done.
 
   simplify.
@@ -433,6 +435,7 @@ Proof.
   model_check_step.
   model_check_step.
   model_check_step.
+  model_check_step.
   model_check_done.
 
   simplify.
@@ -540,7 +543,7 @@ Inductive stepC (s : summary)  : heap * locks * cmd -> heap * locks * cmd -> Pro
                             * with [c0]. *)
 
                            -> 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
                             * command. *)
 
@@ -1371,11 +1374,8 @@ Ltac por_closure :=
   repeat (apply oneStepClosure_empty
           || (apply oneStepClosure_split; [ por_invert; try equality; solve [ singletoner ] | ])).
 
-Ltac por_step :=
-  eapply MscStep; [ por_closure | simplify ].
-
-Ltac por_done :=
-  apply MscDone; eapply oneStepClosure_solve; [ por_closure | simplify; solve [ sets ] ].
+Ltac por_step := eapply MscStep; [ por_closure | simplify ].
+Ltac por_done := apply MscDone.
 
 (* 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
@@ -1405,7 +1405,7 @@ Proof.
   por_step.
   por_step.
   por_step.
-
+  por_step.
   por_done.
 
   sets.
diff --git a/frap_book.tex b/frap_book.tex
index 726f488..ab2f36f 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -4533,9 +4533,9 @@ $$\infer{\summ{\mt{Lock} \; a}{(r, w, \ell)}}{
   a \in \ell
 }$$
 
-$$\infer{\summ{c_1 || c_2}{(r, w, \ell)}}{
-  \summ{c_1}{(r, w, \ell)}
-  & \summ{c_1}{(r, w, \ell)}
+$$\infer{\summ{c_1 || c_2}{s}}{
+  \summ{c_1}{s}
+  & \summ{c_2}{s}
 }$$
 
 \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 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.
-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.
 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:
 $$(\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.
-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.
 
 \begin{description}