SharedMemory: model-checking example, after tweaking library

Frap.v

@@ -1,4 +1,4 @@
-Require Import String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
+Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
 Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
 Require Import List.
 Export List ListNotations.
@@ -58,6 +58,7 @@ end.
 Ltac fancy_neq :=
   repeat match goal with
          | _ => maps_neq
+         | [ H : @eq (nat -> _) _ _ |- _ ] => apply (f_equal (fun f => f 0)) in H
          | [ H : _ = _ |- _ ] => invert H
          end.
 
@@ -129,33 +130,46 @@ Ltac first_order := firstorder idtac.
 
 (** * Model checking *)
 
-Ltac model_check_done :=
-  apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst;
-  repeat match goal with
-         | [ H : ?P |- _ ] =>
-           match type of P with
-           | Prop => invert H; simplify
-           end
-         end; equality.
+Ltac sets := Sets.sets ltac:(simpl in *; intuition (subst; auto)).
 
-Ltac singletoner :=
+Ltac model_check_invert1 :=
+  match goal with
+  | [ H : ?P |- _ ] =>
+    match type of P with
+    | Prop => invert H;
+              repeat match goal with
+                     | [ H : existT _ ?x _ = existT _ ?x _ |- _ ] =>
+                       apply inj_pair2 in H; subst
+                     end; simplify
+    end
+  end.
+
+Ltac model_check_invert := simplify; subst; repeat model_check_invert1.
+
+Lemma oneStepClosure_solve : forall A (sys : trsys A) I I',
+  oneStepClosure sys I I'
+  -> I = I'
+  -> oneStepClosure sys I I.
+Proof.
+  equality.
+Qed.
+
+Ltac singletoner := try (exfalso; solve [ sets ]);
   repeat match goal with
          (* | _ => apply singleton_in *)
          | [ |- _ ?S ] => idtac S; apply singleton_in
          | [ |- (_ \cup _) _ ] => apply singleton_in_other
          end.
 
+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_step :=
-  eapply MscStep; [
-    repeat (apply oneStepClosure_empty
-            || (apply oneStepClosure_split; [ simplify;
-                                              repeat match goal with
-                                                     | [ H : ?P |- _ ] =>
-                                                       match type of P with
-                                                       | Prop => invert H; simplify; try congruence
-                                                       end
-                                                     end; solve [ singletoner ] | ]))
-  | simplify ].
+  eapply MscStep; [ closure | simplify ].
 
 Ltac model_check_steps1 := model_check_done || model_check_step.
 Ltac model_check_steps := repeat model_check_steps1.
@@ -223,5 +237,3 @@ Ltac simplify_map :=
     simplify_map' (m $+ (k, v)) tt ltac:(fun m' =>
                                            replace (@add A B m k v) with m' by maps_equal)
   end.
-
-Ltac sets := Sets.sets ltac:(simpl in *; intuition (subst; auto)).

ModelCheck.v

@@ -37,28 +37,30 @@ Proof.
 Qed.
 
 Inductive multiStepClosure {state} (sys : trsys state)
-  : (state -> Prop) -> (state -> Prop) -> Prop :=
-| MscDone : forall inv,
+  : (state -> Prop) -> (state -> Prop) -> (state -> Prop) -> Prop :=
+| MscDone : forall inv worklist,
     oneStepClosure sys inv inv
-    -> multiStepClosure sys inv inv
-| MscStep : forall inv inv' inv'',
-    oneStepClosure sys inv inv'
-    -> multiStepClosure sys inv' inv''
-    -> multiStepClosure sys inv inv''.
+    -> multiStepClosure sys inv worklist 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 multiStepClosure_ok' : forall state (sys : trsys state) (inv inv' : state -> Prop),
-  multiStepClosure sys inv inv'
+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)
   -> invariantFor sys inv'.
 Proof.
   induction 1; simpl; intuition eauto using oneStepClosure_done.
 
-  unfold oneStepClosure, oneStepClosure_current in *.
-  intuition eauto.
+  apply IHmultiStepClosure.
+  intuition.
+  apply H1 in H2.
+  sets idtac.
 Qed.
 
 Theorem multiStepClosure_ok : forall state (sys : trsys state) (inv : state -> Prop),
-  multiStepClosure sys sys.(Initial) inv
+  multiStepClosure sys sys.(Initial) sys.(Initial) inv
   -> invariantFor sys inv.
 Proof.
   eauto using multiStepClosure_ok'.

Sets.v

@@ -201,7 +201,7 @@ Inductive doSubtract A : list A -> list A -> list A -> Prop :=
   -> doSubtract ls ls0 ls'
   -> doSubtract (x :: ls) ls0 (x :: ls')
 | DsDrop : forall x ls ls0 ls',
-  List.In x ls
+  List.In x ls0
   -> doSubtract ls ls0 ls'
   -> doSubtract (x :: ls) ls0 ls'.
 
@@ -213,6 +213,7 @@ Theorem doSubtract_fwd : forall A x (ls ls0 ls' : list A),
 Proof.
   induction 1; simpl; intuition.
   subst; eauto.
+  tauto.
 Qed.
 
 Theorem doSubtract_bwd1 : forall A x (ls ls0 ls' : list A),
@@ -243,12 +244,18 @@ Proof.
   unfold constant; intuition eauto using doSubtract_fwd, doSubtract_bwd1, doSubtract_bwd2.
 Qed.
 
+Ltac fancy_neq :=
+  solve [ repeat match goal with
+                 | [ H : @eq (nat -> _) _ _ |- _ ] => apply (f_equal (fun f => f 0)) in H
+                 | [ H : _ = _ |- _ ] => inversion H; clear H; subst
+                 end ].
+
 Ltac doSubtract :=
   match goal with
   | [ |- context[constant ?ls \setminus constant ?ls0] ] =>
     erewrite (@doSubtract_ok _ ls ls0)
       by repeat (apply DsNil
-                 || (apply DsKeep; [ simpl; intuition congruence | ])
+                 || (apply DsKeep; [ simpl; intuition (congruence || fancy_neq) | ])
                  || (apply DsDrop; [ simpl; intuition congruence | ]))
   end.
 

SharedMemory.v

@@ -25,48 +25,42 @@ Ltac simp := repeat (simplify; subst; propositional;
 
 (** * An object language with shared-memory concurrency *)
 
-Inductive loop_outcome acc :=
-| Done (a : acc)
-| Again (a : acc).
+(* Let's simplify the encoding by only working with commands that generate
+ * [nat]. *)
+Inductive loop_outcome :=
+| Done (a : nat)
+| Again (a : nat).
 
-Inductive cmd : Set -> Type :=
-| Return {result : Set} (r : result) : cmd result
-| Bind {result result'} (c1 : cmd result') (c2 : result' -> cmd result) : cmd result
-| Read (a : nat) : cmd nat
-| Write (a v : nat) : cmd unit
-| Loop {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) : cmd acc
-| Fail {result} : cmd result
+Inductive cmd :=
+| Return (r : nat)
+| Bind (c1 : cmd) (c2 : nat -> cmd)
+| Read (a : nat)
+| Write (a v : nat)
+| Fail
 
 (* Now here's the new part: parallel composition of commands. *)
-| Par (c1 c2 : cmd unit) : cmd unit
+| Par (c1 c2 : cmd)
 
 (* Let's also add locking commands, where locks are named by [nat]s. *)
-| Lock (a : nat) : cmd unit
-| Unlock (a : nat) : cmd unit.
+| Lock (a : nat)
+| Unlock (a : nat).
 
 Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80).
-Notation "'for' x := i 'loop' c1 'done'" := (Loop i (fun x => c1)) (right associativity, at level 80).
 Infix "||" := Par.
 
 Definition locks := set nat.
 
-Inductive step : forall A, heap * locks * cmd A -> heap * locks * cmd A -> Prop :=
-| StepBindRecur : forall result result' (c1 c1' : cmd result') (c2 : result' -> cmd result) h h' l l',
+Inductive step : heap * locks * cmd -> heap * locks * cmd -> Prop :=
+| StepBindRecur : forall c1 c1' c2 h h' l l',
   step (h, l, c1) (h', l', c1')
   -> step (h, l, Bind c1 c2) (h', l', Bind c1' c2)
-| StepBindProceed : forall (result result' : Set) (v : result') (c2 : result' -> cmd result) h l,
+| StepBindProceed : forall v c2 h l,
   step (h, l, Bind (Return v) c2) (h, l, c2 v)
 
-| StepLoop : forall (acc : Set) (init : acc) (body : acc -> cmd (loop_outcome acc)) h l,
-  step (h, l, Loop init body) (h, l, o <- body init; match o with
-                                                     | Done a => Return a
-                                                     | Again a => Loop a body
-                                                     end)
-
 | StepRead : forall h l a,
   step (h, l, Read a) (h, l, Return (h $! a))
 | StepWrite : forall h l a v,
-  step (h, l, Write a v) (h $+ (a, v), l, Return tt)
+  step (h, l, Write a v) (h $+ (a, v), l, Return 0)
 
 | StepParRecur1 : forall h l c1 c2 h' l' c1',
   step (h, l, c1) (h', l', c1')
@@ -74,19 +68,60 @@ Inductive step : forall A, heap * locks * cmd A -> heap * locks * cmd A -> Prop
 | StepParRecur2 : forall h l c1 c2 h' l' c2',
   step (h, l, c2) (h', l', c2')
   -> step (h, l, Par c1 c2) (h', l', Par c1 c2')
-| StepParProceed1 : forall h l c2,
-   step (h, l, Par (Return tt) c2) (h, l, c2)
-| StepParProceed2 : forall h l c1,
-   step (h, l, Par c1 (Return tt)) (h, l, c1)
+| StepParProceed : forall h l,
+   step (h, l, Par (Return 0) (Return 0)) (h, l, Return 0)
 
 | StepLock : forall h l a,
   ~a \in l
-  -> step (h, l, Lock a) (h, l \cup {a}, Return tt)
+  -> step (h, l, Lock a) (h, l \cup {a}, Return 0)
 | StepUnlock : forall h l a,
   a \in l
-  -> step (h, l, Unlock a) (h, l \setminus {a}, Return tt).
+  -> step (h, l, Unlock a) (h, l \setminus {a}, Return 0).
 
-Definition trsys_of (h : heap) (l : locks) {result} (c : cmd result) := {|
+Definition trsys_of (h : heap) (l : locks) (c : cmd) := {|
   Initial := {(h, l, c)};
-  Step := step (A := result)
+  Step := step
 |}.
+
+
+Example two_increments_thread :=
+  _ <- Lock 0;
+  n <- Read 0;
+  _ <- Write 0 (n + 1);
+  Unlock 0.
+
+Example two_increments := two_increments_thread || two_increments_thread.
+
+Theorem two_increments_ok :
+  invariantFor (trsys_of $0 {} two_increments)
+               (fun p => let '(h, l, c) := p in
+                         c = Return 0
+                         -> h $! 0 = 2).
+Proof.
+  unfold two_increments, two_increments_thread.
+  simplify.
+  eapply invariant_weaken.
+  apply multiStepClosure_ok; simplify.
+
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_step.
+  model_check_done.
+
+  simplify.
+  propositional; subst; try equality.
+  simplify.
+  reflexivity.
+Qed.