Skip to content
Snippets Groups Projects
Commit 7350a43b authored by Alban Gruin's avatar Alban Gruin
Browse files

correct_store_buffer: generalize work_on_e for two instructions


Signed-off-by: default avatarAlban Gruin <alban.gruin@irit.fr>
parent e4a71034
No related branches found
No related tags found
No related merge requests found
...@@ -169,13 +169,25 @@ Section monotonicity. ...@@ -169,13 +169,25 @@ Section monotonicity.
Ltac work_on_e He' := Ltac work_on_e He' :=
rewrite Htc, Htc', Ht; rewrite Htc, Htc', Ht;
rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- *; match goal with
| [ _ : e = e' |- _ ] =>
rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- *
| [ _ : e <> e' |- _ ] =>
rewrite Ht'
end;
unfold cycle; unfold cycle;
rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi), rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi),
(map_in_the_middle _ _ e d _ _ tpre' tpost' _ (eq_refl _) Hi'); (map_in_the_middle _ _ _ d _ _ tpre' tpost' _ (eq_refl _) Hi');
unfold cycle_elt; unfold cycle_elt;
rewrite <- Ht; rewrite <- Ht;
subst e. match goal with
| [ _ : e = e' |- _ ] =>
subst e
| [ _ : e <> e' |- _ ] =>
rewrite <- Ht';
subst e;
subst e'
end.
Lemma unmoved_no_lat_can_advance : Lemma unmoved_no_lat_can_advance :
e = (opc, (st, 0)) -> e = e' -> forall n, e = (opc, (st, 0)) -> e = e' -> forall n,
...@@ -271,17 +283,9 @@ Section monotonicity. ...@@ -271,17 +283,9 @@ Section monotonicity.
intros He He' Hed Hsl. intros He He' Hed Hsl.
specialize (Hsu st' opc). specialize (Hsu st' opc).
(* work_on_e replacement. *)
(* Goal transformation: show exactly how e and e' are modified by the (* Goal transformation: show exactly how e and e' are modified by the
* cycle function. *) * cycle function. *)
rewrite Htc, Htc', Ht, Ht'. work_on_e Hed.
unfold cycle.
rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi),
(map_in_the_middle _ _ e' d _ _ tpre' tpost' _ (eq_refl _) Hi').
unfold cycle_elt.
rewrite <- Ht, <- Ht'.
subst e.
subst e'.
(* Case-by-case analysis *) (* Case-by-case analysis *)
destruct st, st'; destruct st, st';
...@@ -326,14 +330,7 @@ Section monotonicity. ...@@ -326,14 +330,7 @@ Section monotonicity.
(* n and n' are = 0. We have a lemma for that. *) (* n and n' are = 0. We have a lemma for that. *)
now apply moved_no_lat_is_monotonic | now apply moved_no_lat_is_monotonic |
(* Other cases: rewrite the goal to make cycle appear. *) (* Other cases: rewrite the goal to make cycle appear. *)
rewrite Htc, Htc', Ht, Ht'; work_on_e Hed;
unfold cycle;
rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi),
(map_in_the_middle _ _ e' d _ _ tpre' tpost' _ (eq_refl _) Hi');
unfold cycle_elt;
rewrite <- Ht, <- Ht';
subst e;
subst e';
(* Since n or n' is not equal to 0, opc is a load. Remove other cases. *) (* Since n or n' is not equal to 0, opc is a load. Remove other cases. *)
destruct opc; destruct opc;
[| discriminate (HvalidStLat (eq_refl _)) [| discriminate (HvalidStLat (eq_refl _))
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment