1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
Require Import DepExampleEqTest.
Require Import Parallelizability.
Module PChk := ParallelChecks L PosResourceSet.
Definition bblock_is_para (p: bblock) : bool :=
PChk.is_parallelizable (comp_bblock p).
Local Hint Resolve the_mem_separation reg_map_separation.
Section SEC.
Variable ge: P.genv.
(* Actually, almost the same proof script than [comp_bblock_correct_aux] !
We could definitely factorize the proof through a lemma on compilation to macros.
*)
Lemma comp_bblock_correct_para_iw p: forall sin sout min mout,
match_state sin min ->
match_state sout mout ->
match_option_state (sem_bblock_par_iw p sin sout) (PChk.prun_iw ge (comp_bblock p) mout min).
Proof.
induction p as [|i p IHp]; simpl; eauto.
intros sin sout min mout Hin Hout; destruct i; simpl; erewrite !comp_op_correct; eauto; simpl.
- (* MOVE *)
apply IHp; auto.
destruct Hin as [H1 H2]; destruct Hout as [H3 H4]; constructor 1; simpl; auto.
+ rewrite L.assign_diff; auto.
+ unfold assign; intros r; destruct (Pos.eq_dec dest r).
* subst; rewrite L.assign_eq; auto.
* rewrite L.assign_diff; auto.
- (* ARITH *)
apply IHp; auto.
destruct Hin as [H1 H2]; destruct Hout as [H3 H4]; constructor 1; simpl; auto.
+ rewrite L.assign_diff; auto.
+ unfold assign; intros r; destruct (Pos.eq_dec dest r).
* subst; rewrite L.assign_eq; auto.
* rewrite L.assign_diff; auto.
- (* LOAD *)
destruct Hin as [H1 H2]; destruct Hout as [H3 H4].
rewrite H1, H2; simpl.
unfold get_addr.
destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto.
apply IHp. { constructor 1; auto. }
constructor 1; simpl.
+ rewrite L.assign_diff; auto.
+ unfold assign; intros r; destruct (Pos.eq_dec dest r).
* subst; rewrite L.assign_eq; auto.
* rewrite L.assign_diff; auto.
- (* STORE *)
destruct Hin as [H1 H2]; destruct Hout as [H3 H4].
rewrite H1, !H2; simpl.
unfold get_addr.
destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto.
apply IHp. { constructor 1; auto. }
constructor 1; simpl; auto.
intros r; rewrite L.assign_diff; auto.
- (* MEMSWAP *)
destruct Hin as [H1 H2]; destruct Hout as [H3 H4].
rewrite H1, !H2; simpl.
unfold get_addr.
destruct (rm sin base + operand_eval offset (rm sin))%Z; simpl; auto.
apply IHp. { constructor 1; auto. }
constructor 1; simpl; auto.
+ intros r0; rewrite L.assign_diff; auto.
unfold assign; destruct (Pos.eq_dec r r0).
* subst; rewrite L.assign_eq; auto.
* rewrite L.assign_diff; auto.
Qed.
Local Hint Resolve match_trans_state.
Definition trans_option_state (os: option state): option L.mem :=
match os with
| Some s => Some (trans_state s)
| None => None
end.
Lemma match_trans_option_state os: match_option_state os (trans_option_state os).
Proof.
destruct os; simpl; eauto.
Qed.
Local Hint Resolve match_trans_option_state comp_bblock_correct match_option_state_intro_X match_from_res_eq res_equiv_from_match.
Lemma is_mem_reg (x: P.R.t): x=the_mem \/ exists r, x=reg_map r.
Proof.
case (Pos.eq_dec x the_mem); auto.
unfold the_mem, reg_map; constructor 2.
eexists (Pos.pred x). rewrite Pos.succ_pred; auto.
Qed.
Lemma res_eq_from_match (os: option state) (om1 om2: option L.mem):
(match_option_stateX om1 os) -> (match_option_state os om2) -> (L.res_eq om1 om2).
Proof.
destruct om1 as [m1|]; simpl.
- intros (s & H1 & H2 & H3); subst; simpl.
intros (m2 & H4 & H5 & H6); subst; simpl.
eapply ex_intro; intuition eauto.
destruct (is_mem_reg x) as [H|(r & H)]; subst; congruence.
- intro; subst; simpl; auto.
Qed.
(* We use axiom of functional extensionality ! *)
Require Coq.Logic.FunctionalExtensionality.
Lemma match_from_res_equiv os1 os2 om:
res_equiv os2 os1 -> match_option_state os1 om -> match_option_state os2 om.
Proof.
destruct os2 as [s2 | ]; simpl.
- intros (s & H1 & H2 & H3). subst; simpl.
intros (m & H4 & H5 & H6); subst; simpl.
eapply ex_intro; intuition eauto.
constructor 1.
+ rewrite H5; apply f_equal; eapply FunctionalExtensionality.functional_extensionality; auto.
+ congruence.
- intros; subst; simpl; auto.
Qed.
Require Import Sorting.Permutation.
Local Hint Constructors Permutation.
Lemma comp_bblock_Permutation p p': Permutation p p' -> Permutation (comp_bblock p) (comp_bblock p').
Proof.
induction 1; simpl; eauto.
Qed.
Lemma comp_bblock_Permutation_back p1 p1': Permutation p1 p1' ->
forall p, p1=comp_bblock p ->
exists p', p1'=comp_bblock p' /\ Permutation p p'.
Proof.
induction 1; simpl; eauto.
- destruct p as [|i p]; simpl; intro X; inversion X; subst.
destruct (IHPermutation p) as (p' & H1 & H2); subst; auto.
eexists (i::p'). simpl; eauto.
- destruct p as [|i1 p]; simpl; intro X; inversion X as [(H & H1)]; subst; clear X.
destruct p as [|i2 p]; simpl; inversion_clear H1.
eexists (i2::i1::p). simpl; eauto.
- intros p H1; destruct (IHPermutation1 p) as (p' & H2 & H3); subst; auto.
destruct (IHPermutation2 p') as (p'' & H4 & H5); subst; eauto.
Qed.
Local Hint Resolve comp_bblock_Permutation res_eq_from_match match_from_res_equiv comp_bblock_correct_para_iw.
Lemma bblock_par_iff_prun p s os':
sem_bblock_par p s os' <-> PChk.prun ge (comp_bblock p) (trans_state s) (trans_option_state os').
Proof.
unfold sem_bblock_par, PChk.prun. constructor 1.
- intros (p' & H1 & H2).
eexists (comp_bblock p'); intuition eauto.
- intros (p' & H1 & H2).
destruct (comp_bblock_Permutation_back _ _ H2 p) as (p0 & H3 & H4); subst; auto.
eexists p0; constructor 1; eauto.
Qed.
Theorem bblock_is_para_correct p:
bblock_is_para p = true -> forall s os', (sem_bblock_par p s os' <-> res_equiv os' (sem_bblock p s)).
Proof.
intros H; generalize (PChk.is_parallelizable_correct ge _ H); clear H.
intros H s os'.
rewrite bblock_par_iff_prun, H.
constructor; eauto.
Qed.
End SEC.
|
