From e4a71034d7a9c107b2aba7bd79461f52722ddd4e Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Fri, 29 Jul 2022 15:35:30 +0200
Subject: [PATCH] correct_store_buffer: add comments for clarity
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 17 ++++++++++++++---
1 file changed, 14 insertions(+), 3 deletions(-)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 3438fe3..8013edc 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -347,8 +347,11 @@ Section monotonicity.
rewrite Hst' in Hsl, Hed |- *.
destruct st;
try discriminate.
- + now destruct (_ && _).
- + destruct (_ && _).
+ + (* st = Sp. In this case, the next stage is either Sp or Lsu, which are
+ * both lower than Lu. *)
+ now destruct (_ && _).
+ + (* st = Lsu. In this case, the next stage is either Lsu or Lu. *)
+ destruct (_ && _).
* simpl.
rewrite Nat.leb_le.
lia.
@@ -358,11 +361,19 @@ Section monotonicity.
- (* st = Lu. *)
destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat].
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. *)
- destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat].
rewrite Hst in Hsl, Hed |- *.
+ (* e is lower than e', hence n > n'. *)
now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')).
Qed.
--
GitLab