From 1e7c33f0a973ff8639f951d4fcc173ca40a79f28 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 5 Mar 2017 20:46:53 -0500 Subject: [PATCH] Optimizing tactics for faster state-space exploration --- ConcurrentSeparationLogic.v | 4 +- ConcurrentSeparationLogic_template.v | 4 +- Frap.v | 17 +- Map.v | 4 +- ModelChecking.v | 25 ++- ModelChecking_template.v | 19 +- Sets.v | 319 ++++++++++++++++++++++++++- _CoqProject | 2 +- 8 files changed, 374 insertions(+), 20 deletions(-) diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index f6ac7e8..1f96af0 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -1329,7 +1329,7 @@ Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a, ~f a \in l -> nth_error linvs a = Some I -> (forall x y, f x = f y -> x = y) - -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in l \cup {f a})) ===> I)%sep linvs. + -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in {f a} \cup l)) ===> I)%sep linvs. Proof. induct linvs; simplify. @@ -1362,7 +1362,7 @@ Qed. Lemma lockChunks_lock : forall a l I linvs, ~a \in l -> nth_error linvs a = Some I - -> lockChunks l linvs ===> I * lockChunks (l \cup {a}) linvs. + -> lockChunks l linvs ===> I * lockChunks ({a} \cup l) linvs. Proof. simp. apply lockChunks_lock' with (f := fun n => n); auto. diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v index 410bb30..a0a62d9 100644 --- a/ConcurrentSeparationLogic_template.v +++ b/ConcurrentSeparationLogic_template.v @@ -1232,7 +1232,7 @@ Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a, ~f a \in l -> nth_error linvs a = Some I -> (forall x y, f x = f y -> x = y) - -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in l \cup {f a})) ===> I)%sep linvs. + -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in {f a} \cup l)) ===> I)%sep linvs. Proof. induct linvs; simplify. @@ -1265,7 +1265,7 @@ Qed. Lemma lockChunks_lock : forall a l I linvs, ~a \in l -> nth_error linvs a = Some I - -> lockChunks l linvs ===> I * lockChunks (l \cup {a}) linvs. + -> lockChunks l linvs ===> I * lockChunks ({a} \cup l) linvs. Proof. simp. apply lockChunks_lock' with (f := fun n => n); auto. diff --git a/Frap.v b/Frap.v index 10d7c67..a06743d 100644 --- a/Frap.v +++ b/Frap.v @@ -174,7 +174,7 @@ Ltac simplify := repeat (unifyTails; pose proof I); | [ H : True |- _ ] => clear H end; repeat progress (simpl in *; intros; try autorewrite with core in *; simpl_maps); - repeat (removeDups || doSubtract). + repeat (normalize_set || doSubtract). Ltac propositional := intuition idtac. Ltac linear_arithmetic := intros; @@ -284,10 +284,21 @@ Ltac closure := Ltac model_check_done := apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ]. -Ltac model_check_step := +Ltac model_check_step0 := eapply MscStep; [ closure | simplify ]. -Ltac model_check_steps1 := model_check_done || model_check_step. +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_steps := repeat model_check_steps1. Ltac model_check_finish := simplify; propositional; subst; simplify; try equality; try linear_arithmetic. diff --git a/Map.v b/Map.v index 149af30..743200e 100644 --- a/Map.v +++ b/Map.v @@ -161,8 +161,8 @@ Module Type S. Hint Rewrite merge_empty1 merge_empty2 using solve [ eauto 1 ]. Hint Rewrite merge_empty1_alt merge_empty2_alt using congruence. - Hint Rewrite merge_add1 using solve [ eauto | unfold Sets.In; autorewrite with core in *; simpl in *; intuition congruence ]. - Hint Rewrite merge_add1_alt using solve [ congruence | unfold Sets.In; autorewrite with core in *; simpl in *; intuition congruence ]. + Hint Rewrite merge_add1 using solve [ eauto | unfold Sets.In; autorewrite with core in *; simpl in *; try (normalize_set; simpl); intuition congruence ]. + Hint Rewrite merge_add1_alt using solve [ congruence | unfold Sets.In; autorewrite with core in *; simpl in *; try (normalize_set; simpl); intuition congruence ]. Axiom includes_intro : forall K V (m1 m2 : fmap K V), (forall k v, m1 $? k = Some v -> m2 $? k = Some v) diff --git a/ModelChecking.v b/ModelChecking.v index 8f8c6ec..597e968 100644 --- a/ModelChecking.v +++ b/ModelChecking.v @@ -161,11 +161,12 @@ Proof. simplify. propositional. - left. right. + left. apply H. equality. + right. right. eapply H2. eassumption. @@ -197,6 +198,8 @@ Theorem fact_init_is : forall original_input, Proof. simplify. apply sets_equal; simplify. + (* Note the use of a theorem [sets_equal], saying that sets are equal if they + * have the same elements. *) propositional. invert H. @@ -209,7 +212,7 @@ Qed. (* Now we will prove that factorial is correct, for the input 2, without needing * to write out an inductive invariant ourselves. Note that it's important that * we choose a small, constant input, so that the reachable state space is - * finite. *) + * finite and tractable. *) Theorem factorial_ok_2 : invariantFor (factorial_sys 2) (fact_correct 2). Proof. @@ -297,17 +300,17 @@ Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A), Proof. simplify. right. + right. assumption. Qed. Ltac singletoner := repeat match goal with - (* | _ => apply singleton_in *) | [ |- _ ?S ] => idtac S; apply singleton_in | [ |- (_ \cup _) _ ] => apply singleton_in_other end. -Ltac model_check_step := +Ltac model_check_step0 := eapply MscStep; [ repeat ((apply oneStepClosure_empty; simplify) || (apply oneStepClosure_split; [ simplify; @@ -316,7 +319,18 @@ Ltac model_check_step := end; solve [ singletoner ] | ])) | simplify ]. -Ltac model_check_steps1 := model_check_done || model_check_step. +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_steps := repeat model_check_steps1. Ltac model_check_finish := simplify; propositional; subst; simplify; equality. @@ -1573,4 +1587,3 @@ Theorem twoadd6_ok : Proof. twoadd. Qed. - diff --git a/ModelChecking_template.v b/ModelChecking_template.v index 7fc632c..5dc619e 100644 --- a/ModelChecking_template.v +++ b/ModelChecking_template.v @@ -125,11 +125,12 @@ Proof. simplify. propositional. - left. right. + left. apply H. equality. + right. right. eapply H2. eassumption. @@ -213,6 +214,7 @@ Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A), Proof. simplify. right. + right. assumption. Qed. @@ -222,7 +224,7 @@ Ltac singletoner := | [ |- (_ \cup _) _ ] => apply singleton_in_other end. -Ltac model_check_step := +Ltac model_check_step0 := eapply MscStep; [ repeat ((apply oneStepClosure_empty; simplify) || (apply oneStepClosure_split; [ simplify; @@ -231,7 +233,18 @@ Ltac model_check_step := end; solve [ singletoner ] | ])) | simplify ]. -Ltac model_check_steps1 := model_check_done || model_check_step. +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_steps := repeat model_check_steps1. Ltac model_check_finish := simplify; propositional; subst; simplify; equality. diff --git a/Sets.v b/Sets.v index 95c8002..06fa615 100644 --- a/Sets.v +++ b/Sets.v @@ -127,7 +127,7 @@ End properties. Hint Resolve subseteq_refl subseteq_In. -Hint Rewrite union_constant. +(*Hint Rewrite union_constant.*) (** * Removing duplicates from constant sets *) @@ -269,3 +269,320 @@ Ltac unifyTails := | ?A -> Prop => unify x (constant (@nil A)) end end. + + +(** * But wait... there's a reflective way to do some of this, too. *) + +Require Import Arith. +Import List ListNotations. + +Section setexpr. + Variable A : Type. + + Inductive setexpr := + | Literal (vs : list nat) + | Constant (s : set A) + | Union (e1 e2 : setexpr). + + Fixpoint interp_setexpr (env : list A) (e : setexpr) : set A := + match e with + | Literal vs => + match env with + | [] => {} + | x :: _ => constant (map (nth_default x env) vs) + end + | Constant s => s + | Union e1 e2 => interp_setexpr env e1 \cup interp_setexpr env e2 + end. + + Record normal_form := { + Elements : list nat; + Other : option (set A) + }. + + Fixpoint member (n : nat) (ls : list nat) : bool := + match ls with + | [] => false + | m :: ls' => (n =? m) || member n ls' + end. + + Fixpoint dedup (ls : list nat) : list nat := + match ls with + | [] => [] + | n :: ls => + let ls' := dedup ls in + if member n ls' then ls' else n :: ls' + end. + + Fixpoint setmerge (ls1 ls2 : list nat) : list nat := + match ls1 with + | [] => ls2 + | n :: ls1' => + if member n ls2 then setmerge ls1' ls2 else n :: setmerge ls1' ls2 + end. + + Fixpoint normalize_setexpr (e : setexpr) : normal_form := + match e with + | Literal vs => {| Elements := dedup vs; Other := None |} + | Constant s => {| Elements := []; Other := Some s |} + | Union e1 e2 => + let nf1 := normalize_setexpr e1 in + let nf2 := normalize_setexpr e2 in + {| Elements := setmerge nf1.(Elements) nf2.(Elements); + Other := match nf1.(Other), nf2.(Other) with + | None, None => None + | o, None => o + | None, o => o + | Some s1, Some s2 => Some (s1 \cup s2) + end |} + end. + + Definition interp_normal_form (env : list A) (nf : normal_form) : set A := + let cs := match env with + | [] => {} + | x :: _ => constant (map (nth_default x env) nf.(Elements)) + end in + match nf.(Other) with + | None => cs + | Some o => cs \cup o + end. + + Lemma member_ok : forall n ns, + if member n ns then In n ns else ~In n ns. + Proof. + induction ns; simpl; intuition. + case_eq (n =? a); simpl; intros. + apply beq_nat_true in H; auto. + apply beq_nat_false in H. + destruct (member n ns); intuition. + Qed. + + Lemma In_dedup_fwd : forall n ns, + In n (dedup ns) + -> In n ns. + Proof. + induction ns; simpl; intuition. + pose proof (member_ok a (dedup ns)). + destruct (member a (dedup ns)); simpl in *; intuition. + Qed. + + Lemma In_dedup_bwd : forall n ns, + In n ns + -> In n (dedup ns). + Proof. + induction ns; simpl; intuition. + pose proof (member_ok a (dedup ns)). + destruct (member a (dedup ns)); simpl in *; intuition congruence. + pose proof (member_ok a (dedup ns)). + destruct (member a (dedup ns)); simpl in *; intuition congruence. + Qed. + + Lemma constant_dedup : forall (f : _ -> A) vs, + constant (map f (dedup vs)) = constant (map f vs). + Proof. + induction vs; simpl; intuition. + pose proof (member_ok a (dedup vs)). + case_eq (member a (dedup vs)); intro. + rewrite IHvs. + rewrite H0 in H. + apply In_dedup_fwd in H. + apply sets_equal. + unfold constant. + simpl. + intuition. + apply in_map_iff. + eauto. + simpl. + apply sets_equal. + simpl. + intuition congruence. + Qed. + + Lemma constant_map_setmerge : forall (f : _ -> A) ns2 ns1, + constant (map f (setmerge ns1 ns2)) = constant (map f ns1) \cup constant (map f ns2). + Proof. + induction ns1; simpl; intros. + + sets ltac:(simpl in *; intuition). + + pose proof (member_ok a ns2). + destruct (member a ns2). + rewrite IHns1. + sets ltac:(simpl in *; intuition). + right. + eapply in_map_iff; eauto. + + simpl. + sets ltac:(simpl in *; intuition). + change (In x (map f (setmerge ns1 ns2))) with ((fun x => In x (map f (setmerge ns1 ns2))) x) in H1. + rewrite IHns1 in H1. + tauto. + change (In x (map f (setmerge ns1 ns2))) with ((fun x => In x (map f (setmerge ns1 ns2))) x). + rewrite IHns1. + tauto. + change (In x (map f (setmerge ns1 ns2))) with ((fun x => In x (map f (setmerge ns1 ns2))) x). + rewrite IHns1. + tauto. + Qed. + + Theorem normalize_setexpr_ok : forall env e, + interp_normal_form env (normalize_setexpr e) = interp_setexpr env e. + Proof. + induction e; simpl; intros. + + unfold interp_normal_form; simpl. + destruct env; trivial. + apply constant_dedup. + + unfold interp_normal_form; simpl. + destruct env; sets ltac:(simpl in *; intuition). + + unfold interp_normal_form in *; simpl in *. + destruct (Other (normalize_setexpr e1)), (Other (normalize_setexpr e2)). + destruct env. + rewrite <- IHe1. + rewrite <- IHe2. + sets ltac:(simpl in *; intuition). + rewrite <- IHe1. + rewrite <- IHe2. + rewrite constant_map_setmerge. + sets ltac:(simpl in *; intuition). + destruct env. + rewrite <- IHe1. + rewrite <- IHe2. + sets ltac:(simpl in *; intuition). + rewrite constant_map_setmerge. + rewrite <- IHe1. + rewrite <- IHe2. + sets ltac:(simpl in *; intuition). + destruct env. + rewrite <- IHe1. + rewrite <- IHe2. + sets ltac:(simpl in *; intuition). + rewrite constant_map_setmerge. + rewrite <- IHe1. + rewrite <- IHe2. + sets ltac:(simpl in *; intuition). + destruct env. + rewrite <- IHe1. + rewrite <- IHe2. + sets ltac:(simpl in *; intuition). + rewrite constant_map_setmerge. + rewrite <- IHe1. + rewrite <- IHe2. + sets ltac:(simpl in *; intuition). + Qed. + + Fixpoint included (ns1 ns2 : list nat) : bool := + match ns1 with + | [] => true + | n :: ns1' => member n ns2 && included ns1' ns2 + end. + + Lemma included_true : forall ns2 ns1, + included ns1 ns2 = true + -> (forall x, In x ns1 -> In x ns2). + Proof. + induction ns1; simpl; intuition subst. + + pose proof (member_ok x ns2). + destruct (member x ns2); simpl in *; auto; congruence. + + pose proof (member_ok a ns2). + destruct (member a ns2); simpl in *; auto; congruence. + Qed. + + Require Import Bool. + + Theorem compare_sets : forall env e1 e2, + let nf1 := normalize_setexpr e1 in + let nf2 := normalize_setexpr e2 in + match Other nf1, Other nf2 with + | None, None => included nf1.(Elements) nf2.(Elements) + && included nf2.(Elements) nf1.(Elements) = true + | _, _ => False + end + -> interp_setexpr env e1 = interp_setexpr env e2. + Proof. + intros. + do 2 rewrite <- normalize_setexpr_ok. + subst nf1. + subst nf2. + unfold interp_normal_form. + destruct (Other (normalize_setexpr e1)), (Other (normalize_setexpr e2)); intuition. + destruct env; trivial. + apply andb_true_iff in H; intuition. + specialize (included_true _ _ H0). + specialize (included_true _ _ H1). + clear H0 H1. + intros. + apply sets_equal. + unfold constant; simpl; intuition. + apply in_map_iff. + apply in_map_iff in H1. + firstorder. + apply in_map_iff. + apply in_map_iff in H1. + firstorder. + Qed. +End setexpr. + +Ltac quote E env k := + let T := type of E in + match eval hnf in T with + | ?A -> Prop => + let rec lookup E env k := + match env with + | [] => k 0 [E] + | E :: _ => k 0 env + | ?E' :: ?env' => + lookup E env' ltac:(fun pos env'' => k (S pos) (E' :: env'')) + end in + + let rec lookups Es env k := + match Es with + | [] => k (@nil nat) env + | ?E :: ?Es' => + lookup E env ltac:(fun pos env' => + lookups Es' env' ltac:(fun poss env'' => + k (pos :: poss) env'')) + end in + + let rec quote' E env k := + match E with + | constant ?Es => + lookups Es env ltac:(fun poss env' => k (Literal A poss) env') + | ?E1 \cup ?E2 => + quote' E1 env ltac:(fun e1 env' => + quote' E2 env' ltac:(fun e2 env'' => + k (Union e1 e2) env'')) + | _ => + (let pf := constr:(eq_refl : E = {}) in + k (Literal A []) env) + || k (Constant E) env + end in + + quote' E env k + end. + +Ltac normalize_set := + match goal with + | [ |- context[@union ?A ?X ?Y] ] => + quote (@union A X Y) (@nil A) ltac:(fun e env => + change (@union A X Y) with (interp_setexpr env e); + rewrite <- normalize_setexpr_ok; + cbv beta iota zeta delta [interp_normal_form normalize_setexpr nth_default + setmerge Elements Other nth_error map dedup member beq_nat orb]) + end. + +Ltac compare_sets := + match goal with + | [ |- @eq ?T ?X ?Y ] => + match eval hnf in T with + | ?A -> _ => + quote X (@nil A) ltac:(fun x env => + quote Y env ltac:(fun y env' => + change (interp_setexpr env' x = interp_setexpr env' y); + apply compare_sets; reflexivity)) + end + end. diff --git a/_CoqProject b/_CoqProject index be158d8..bf3a3c4 100644 --- a/_CoqProject +++ b/_CoqProject @@ -33,7 +33,7 @@ DeepAndShallowEmbeddings.v SepCancel.v SeparationLogic_template.v SeparationLogic.v -SharedMemory.v +#SharedMemory.v ConcurrentSeparationLogic_template.v ConcurrentSeparationLogic.v MessagesAndRefinement.v