summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-12-08 16:18:32 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-12-08 16:18:32 +0000
commit3a84d95c41c20f19737f68e76e534d467cbb581c (patch)
treea9b3b8a4f4c1ccd4084d6b749f4e004c73c8d009 /lib
parent64bacbbc939551a47bb03371d0f1a065af1e278c (diff)
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
Diffstat (limited to 'lib')
-rw-r--r--lib/Parmov.v369
1 files changed, 363 insertions, 6 deletions
diff --git a/lib/Parmov.v b/lib/Parmov.v
index c244b8b..9a07a72 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,
- #<A HREF="http://www-sop.inria.fr/lemme/Laurence.Rideau/RideauSerpetteJFLA05.ps">#
- 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'',
+ #<A HREF="http://hal.inria.fr/inria-00176007">#
+ http://hal.inria.fr/inria-00176007
#</A>#
*)
@@ -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.