From 3a84d95c41c20f19737f68e76e534d467cbb581c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 8 Dec 2007 16:18:32 +0000 Subject: Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Compcert) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@460 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Parmov.v | 369 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 363 insertions(+), 6 deletions(-) (limited to 'lib/Parmov.v') diff --git a/lib/Parmov.v b/lib/Parmov.v index c244b8b6..9a07a725 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -26,11 +26,12 @@ An amazing fact is that for any parallel move problem, at most one temporary (or in our case one integer temporary and one float temporary) is needed. - The development in this section was contributed by Laurence Rideau and - Bernard Serpette. It is described in their paper - ``Coq à la conquête des moulins'', JFLA 2005, - ## - http://www-sop.inria.fr/lemme/Laurence.Rideau/RideauSerpetteJFLA05.ps + The development in this section was designed by Laurence Rideau and + Bernard Serpette. It is described in the paper + ``Tilting at windmills with Coq: Formal verification of + a compilation algorithm for parallel moves'', + ## + http://hal.inria.fr/inria-00176007 ## *) @@ -60,6 +61,8 @@ Variable reg_eq : forall (r1 r2: reg), {r1=r2} + {r1<>r2}. Variable temp: reg -> reg. +Definition is_temp (r: reg): Prop := exists s, r = temp s. + (** A set of moves is a list of pairs of registers, of the form (source, destination). *) @@ -1171,7 +1174,7 @@ Qed. generated by [parmove mu]: any such move [s -> d] is either already present in [mu], or of the form [temp s -> d] or [s -> temp s] for some [s -> d] in [mu]. This syntactic property is useful - to show that [parmove] preserves typing, for instance. *) + to show that [parmove] preserves register classes, for instance. *) Section PROPERTIES. @@ -1250,4 +1253,358 @@ Proof. intros. unfold parmove2. apply parmove_wf_moves. Qed. +(** As a corollary, we show that all sources of [parmove mu] + are sources of [mu] or temporaries, + and likewise all destinations of [parmove mu] are destinations of [mu] + or temporaries. *) + +Remark wf_move_initial_reg_or_temp: + forall mu s d, + wf_move mu s d -> + (In s (srcs mu) \/ is_temp s) /\ (In d (dests mu) \/ is_temp d). +Proof. + induction 1. + split; left. + change s with (fst (s, d)). unfold srcs. apply List.in_map; auto. + change d with (snd (s, d)). unfold dests. apply List.in_map; auto. + split. right. exists s; auto. tauto. + split. tauto. right. exists s; auto. +Qed. + +Lemma parmove_initial_reg_or_temp: + forall mu s d, + In (s, d) (parmove mu) -> + (In s (srcs mu) \/ is_temp s) /\ (In d (dests mu) \/ is_temp d). +Proof. + intros. apply wf_move_initial_reg_or_temp. apply parmove_wf_moves. auto. +Qed. + +Remark in_srcs: + forall mu s, In s (srcs mu) -> exists d, In (s, d) mu. +Proof. + intros. destruct (list_in_map_inv (@fst reg reg) _ _ H) as [[s' d'] [A B]]. + simpl in A. exists d'; congruence. +Qed. + +Remark in_dests: + forall mu d, In d (dests mu) -> exists s, In (s, d) mu. +Proof. + intros. destruct (list_in_map_inv (@snd reg reg) _ _ H) as [[s' d'] [A B]]. + simpl in A. exists s'; congruence. +Qed. + +Lemma parmove_srcs_initial_reg_or_temp: + forall mu s, + In s (srcs (parmove mu)) -> In s (srcs mu) \/ is_temp s. +Proof. + intros. destruct (in_srcs _ _ H) as [d A]. + destruct (parmove_initial_reg_or_temp _ _ _ A). auto. +Qed. + +Lemma parmove_dests_initial_reg_or_temp: + forall mu d, + In d (dests (parmove mu)) -> In d (dests mu) \/ is_temp d. +Proof. + intros. destruct (in_dests _ _ H) as [s A]. + destruct (parmove_initial_reg_or_temp _ _ _ A). auto. +Qed. + +(** As a second corollary, we show that [parmov] preserves register + classes, in the sense made precise below. *) + +Section REGISTER_CLASSES. + +Variable class: Set. +Variable regclass: reg -> class. +Hypothesis temp_preserves_class: forall r, regclass (temp r) = regclass r. + +Definition is_class_compatible (mu: moves) : Prop := + forall s d, In (s, d) mu -> regclass s = regclass d. + +Lemma parmove_preserves_register_classes: + forall mu, + is_class_compatible mu -> + is_class_compatible (parmove mu). +Proof. + intros. + assert (forall s d, wf_move mu s d -> regclass s = regclass d). + induction 1. + apply H; auto. + rewrite temp_preserves_class. auto. + symmetry; apply temp_preserves_class. + red; intros. apply H0. apply parmove_wf_moves. auto. +Qed. + +End REGISTER_CLASSES. + +(** * Extension to partially overlapping registers *) + +(** We now extend the previous results to the case where distinct + registers can partially overlap, so that assigning to one register + changes the value of the other. We asuume given a disjointness relation + [disjoint] between registers. *) + +Variable disjoint: reg -> reg -> Prop. + +Hypothesis disjoint_sym: + forall r1 r2, disjoint r1 r2 -> disjoint r2 r1. + +Hypothesis disjoint_not_equal: + forall r1 r2, disjoint r1 r2 -> r1 <> r2. + +(** Two registers partially overlap if they are different and not disjoint. + For the Coq development, it is easier to define the complement: + two registers do not partially overlap if they are identical or disjoint. *) + +Definition no_overlap (r1 r2: reg) : Prop := + r1 = r2 \/ disjoint r1 r2. + +Lemma no_overlap_sym: + forall r1 r2, no_overlap r1 r2 -> no_overlap r2 r1. +Proof. + intros. destruct H. left; auto. right; auto. +Qed. + +(** We axiomatize the effect of assigning a value to a register over an + execution environment. The target register is set to the given value + (property [weak_update_s]), and registers disjoint from the target + keep their previous values (property [weak_update_d]). The values of + other registers are undefined after the assignment. *) + +Variable weak_update: reg -> val -> env -> env. + +Hypothesis weak_update_s: + forall r v e, weak_update r v e r = v. + +Hypothesis weak_update_d: + forall r1 v e r2, disjoint r1 r2 -> weak_update r1 v e r2 = e r2. + +Fixpoint weak_exec_seq (m: moves) (e: env) {struct m}: env := + match m with + | nil => e + | (s, d) :: m' => weak_exec_seq m' (weak_update d (e s) e) + end. + +Definition disjoint_list (r: reg) (l: list reg) : Prop := + forall r', In r' l -> disjoint r r'. + +Inductive pairwise_disjoint: list reg -> Prop := + | pairwise_disjoint_nil: + pairwise_disjoint nil + | pairwise_disjoint_cons: forall r l, + disjoint_list r l -> + pairwise_disjoint l -> + pairwise_disjoint (r :: l). + +Definition disjoint_temps (r: reg) : Prop := + forall t, is_temp t -> disjoint r t. + +Section OVERLAP. + +(** We consider a parallel move problem [mu] that satisfies the following + conditions, which are stronger, overlap-aware variants of the + [move_no_temp mu] and [is_mill mu] conditions used previously. *) + +Variable mu: moves. + +(** Sources and destinations are disjoint from all temporary registers. *) + +Hypothesis mu_no_temporaries_src: + forall s, In s (srcs mu) -> disjoint_temps s. + +Hypothesis mu_no_temporaries_dst: + forall d, In d (dests mu) -> disjoint_temps d. + +(** Destinations are pairwise disjoint. *) + +Hypothesis mu_dest_pairwise_disjoint: + pairwise_disjoint (dests mu). + +(** Sources and destinations do not partially overlap. *) + +Hypothesis mu_src_dst_no_overlap: + forall s d, In s (srcs mu) -> In d (dests mu) -> no_overlap s d. + +(** Distinct temporaries do not partially overlap. *) + +Hypothesis temps_no_overlap: + forall t1 t2, is_temp t1 -> is_temp t2 -> no_overlap t1 t2. + +(** The following lemmas show that [mu] is a windmill and does not + contain temporary registers. *) + +Lemma disjoint_list_notin: + forall r l, disjoint_list r l -> ~In r l. +Proof. + intros. red; intro. + assert (r <> r). apply disjoint_not_equal. apply H; auto. + congruence. +Qed. + +Lemma pairwise_disjoint_norepet: + forall l, pairwise_disjoint l -> list_norepet l. +Proof. + induction 1. + constructor. + constructor. apply disjoint_list_notin; auto. auto. +Qed. + +Lemma disjoint_temps_not_temp: + forall r, disjoint_temps r -> is_not_temp r. +Proof. + intros; red; intros. apply disjoint_not_equal. apply H. exists d; auto. +Qed. + +Lemma mu_is_mill: + is_mill mu. +Proof. + red. apply pairwise_disjoint_norepet. auto. +Qed. + +Lemma mu_move_no_temp: + move_no_temp mu. +Proof. + red; intros. + split; apply disjoint_temps_not_temp. + apply mu_no_temporaries_src; auto. + unfold srcs. change s with (fst (s,d)). apply List.in_map; auto. + apply mu_no_temporaries_dst; auto. + unfold dests. change d with (snd (s,d)). apply List.in_map; auto. +Qed. + +(** We define the ``adherence'' of the problem [mu] as the set of + registers that partially overlap with one of the registers + possibly assigned by the parallel move: destinations and temporaries. + Again, we define the complement of the ``adherence'' set, which is + more convenient for Coq reasoning. *) + +Definition no_adherence (r: reg) : Prop := + forall x, In x (dests mu) \/ is_temp x -> no_overlap x r. + +(** As a consequence of the hypotheses on [mu], none of the destination + registers, source registers, and temporaries belong to the adherence. *) + +Lemma no_overlap_pairwise: + forall r1 r2 m, pairwise_disjoint m -> In r1 m -> In r2 m -> no_overlap r1 r2. +Proof. + induction 1; intros. + elim H. + simpl in *. destruct H1; destruct H2. + left. congruence. + subst. right. apply H. auto. + subst. right. apply disjoint_sym. apply H. auto. + auto. +Qed. + +Lemma no_adherence_dst: + forall d, In d (dests mu) -> no_adherence d. +Proof. + intros; red; intros. + destruct H0. apply no_overlap_pairwise with (dests mu); auto. + right. apply disjoint_sym. apply mu_no_temporaries_dst; auto. +Qed. + +Lemma no_adherence_src: + forall s, In s (srcs mu) -> no_adherence s. +Proof. + intros; red; intros. + destruct H0. + apply no_overlap_sym. apply mu_src_dst_no_overlap; auto. + right. apply disjoint_sym. apply mu_no_temporaries_src; auto. +Qed. + +Lemma no_adherence_tmp: + forall t, is_temp t -> no_adherence t. +Proof. + intros; red; intros. + destruct H0. + right. apply mu_no_temporaries_dst; auto. + apply temps_no_overlap; auto. +Qed. + +(** The relation [env_match] holds between two environments [e1] and [e2] + if they assign the same values to all registers not in the adherence set. *) + +Definition env_match (e1 e2: env) : Prop := + forall r, no_adherence r -> e1 r = e2 r. + +(** The following lemmas relate the effect of executing moves + using normal, overlap-unaware update and weak, overlap-aware update. *) + +Lemma weak_update_match: + forall e1 e2 s d, + (In s (srcs mu) \/ is_temp s) -> + (In d (dests mu) \/ is_temp d) -> + env_match e1 e2 -> + env_match (update d (e1 s) e1) + (weak_update d (e2 s) e2). +Proof. + intros. red; intros. + assert (no_overlap d r). apply H2. auto. + destruct H3. + subst. rewrite update_s. rewrite weak_update_s. apply H1. + destruct H. apply no_adherence_src; auto. apply no_adherence_tmp; auto. + rewrite update_o. rewrite weak_update_d. apply H1. auto. + auto. apply sym_not_equal. apply disjoint_not_equal. auto. +Qed. + +Lemma weak_exec_seq_match: + forall m e1 e2, + (forall s, In s (srcs m) -> In s (srcs mu) \/ is_temp s) -> + (forall d, In d (dests m) -> In d (dests mu) \/ is_temp d) -> + env_match e1 e2 -> + env_match (exec_seq m e1) (weak_exec_seq m e2). +Proof. + induction m; intros; simpl. + auto. + destruct a as [s d]. simpl in H. simpl in H0. + apply IHm; auto. + apply weak_update_match; auto. +Qed. + +End OVERLAP. + +(** These lemmas imply the following correctness theorem for the [parmove2] + function, taking partial register overlap into account. *) + +Theorem parmove2_correctness_with_overlap: + forall sl dl, + List.length sl = List.length dl -> + (forall r, In r sl -> disjoint_temps r) -> + (forall r, In r dl -> disjoint_temps r) -> + pairwise_disjoint dl -> + (forall s d, In s sl -> In d dl -> no_overlap s d) -> + (forall t1 t2, is_temp t1 -> is_temp t2 -> no_overlap t1 t2) -> + forall e, + let e' := weak_exec_seq (parmove2 sl dl) e in + List.map e' dl = List.map e sl /\ + forall r, disjoint_list r dl -> disjoint_temps r -> e' r = e r. +Proof. + intros. + assert (list_norepet dl). + apply pairwise_disjoint_norepet; auto. + assert (forall r : reg, In r sl -> is_not_temp r). + intros. apply disjoint_temps_not_temp; auto. + assert (forall r : reg, In r dl -> is_not_temp r). + intros. apply disjoint_temps_not_temp; auto. + generalize (parmove2_correctness sl dl H H5 H6 H7 e). + set (e1 := exec_seq (parmove2 sl dl) e). intros [A B]. + destruct (srcs_dests_combine sl dl H) as [C D]. + assert (env_match (combine sl dl) e1 e'). + unfold parmove2. unfold e1, e'. + apply weak_exec_seq_match; try (rewrite C); try (rewrite D); auto. + intros. rewrite <- C. apply parmove_srcs_initial_reg_or_temp. auto. + intros. rewrite <- D. apply parmove_dests_initial_reg_or_temp. auto. + red; auto. + split. + rewrite <- A. + apply list_map_exten; intros. apply H8. + apply no_adherence_dst. rewrite D; auto. rewrite D; auto. rewrite D; auto. + intros. transitivity (e1 r). + symmetry. apply H8. red. rewrite D. intros. destruct H11. + right. apply disjoint_sym. apply H9. auto. + right. apply disjoint_sym. apply H10. auto. + apply B. apply disjoint_list_notin; auto. apply disjoint_temps_not_temp; auto. +Qed. + End PARMOV. -- cgit