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

correct_store_buffer: add comments for clarity


Signed-off-by: default avatarAlban Gruin <alban.gruin@irit.fr>
parent b5678f75
Branches
No related tags found
No related merge requests found
...@@ -347,8 +347,11 @@ Section monotonicity. ...@@ -347,8 +347,11 @@ Section monotonicity.
rewrite Hst' in Hsl, Hed |- *. rewrite Hst' in Hsl, Hed |- *.
destruct st; destruct st;
try discriminate. try discriminate.
+ now destruct (_ && _). + (* st = Sp. In this case, the next stage is either Sp or Lsu, which are
+ destruct (_ && _). * both lower than Lu. *)
now destruct (_ && _).
+ (* st = Lsu. In this case, the next stage is either Lsu or Lu. *)
destruct (_ && _).
* simpl. * simpl.
rewrite Nat.leb_le. rewrite Nat.leb_le.
lia. lia.
...@@ -358,11 +361,19 @@ Section monotonicity. ...@@ -358,11 +361,19 @@ Section monotonicity.
- (* st = Lu. *) - (* st = Lu. *)
destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat]. destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat].
rewrite Hst in Hsl, Hed |- *. rewrite Hst in Hsl, Hed |- *.
now destruct st'. destruct st';
(* Sp, Lsu: impossible since e' would be lower than e. *)
(* Su: impossible since loads cannot be in Su. *)
discriminate
(* Lu: since n' = 0, e' will be in Sn in the next cycle, e will still be
* in Lu. *)
(* Sn: e' will remain in Sn, e will still be in Lu. *)
|| reflexivity.
(* n and n' <> 0. *) (* n and n' <> 0. *)
- destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat]. - destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat].
rewrite Hst in Hsl, Hed |- *. rewrite Hst in Hsl, Hed |- *.
(* e is lower than e', hence n > n'. *)
now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')). now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')).
Qed. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment