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

1 files changed, 363 insertions, 6 deletions

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, 
-  #<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.