From 62aa10beac1541c67623fae7bbdabb9946e55c16 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:42:38 +0200
Subject: [PATCH] correct_store_buffer: if an instruction remains in the same
stage, it progresses
This proves that if an instruction in the same stage while the pipeline
is in a more advanced state, if the one in the less advanced pipeline
can progress, the one in the more advanced pipeline can, too.
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 91 ++++++++++++++++++++++++++++++++++++++
1 file changed, 91 insertions(+)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index d5a6174..4a5e566 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -163,6 +163,97 @@ Section monotonicity.
Hypothesis HbusFree :
busFree (existsb is_in_su t) sbState = true ->
busFree (existsb is_in_su t') sbState' = true.
+
+ Ltac work_on_e He' :=
+ rewrite Htc, Htc', Ht;
+ rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- *;
+ 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;
+ subst e.
+
+ Lemma unmoved_no_lat_can_advance :
+ e = (opc, (st, 0)) -> e = e' ->
+ List.nth_error tc i = Some (opc, (nstg st opc, 0)) ->
+ List.nth_error tc' i = Some (opc, (nstg st opc, 0)).
+ Proof.
+ intros He He'.
+ specialize (Hlu st opc).
+ specialize (Hsu st opc).
+
+ (* Delve onto e, then handle stages on a case-by-case basis. *)
+ work_on_e He'.
+ destruct st.
+
+ (* Sp. The proof does not rely on the kind of instruction. *)
+ - destruct (free _ _ t _) in HfreeLsuPersists |- *.
+ + (* LSU is free in t. *)
+ now destruct (free _ _ _ _) in HfreeLsuPersists |- *;
+ (* Either the next stage is also free in t': trivial. *)
+ (* Otherwise, the next stage is not free in t':
+ this is impossible per HfreeLsuPersists. *)
+ [| discriminate HfreeLsuPersists].
+ + (* LSU is not free in t: this is irrelevant. *)
+ rewrite andb_false_r.
+ discriminate.
+
+ (* Lsu *)
+ - destruct opc, (free _ _ t _) in HfreeFromLsuPersists |- *.
+
+ (* Loads *)
+ + unfold ready.
+ destruct (busFree _ sbState).
+ * now destruct (busFree _ _);
+ [
+ destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
+ try discriminate HfreeFromLsuPersists |
+ discriminate HbusFree
+ ].
+ * discriminate.
+ + rewrite andb_false_r.
+ discriminate.
+
+ (* Stores *)
+ + now destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
+ [| discriminate HfreeFromLsuPersists].
+ + discriminate.
+
+ (* Lu: instructions without latency (this is the case here) move to Sn. *)
+ - now rewrite Hlu.
+
+ (* Su: if there is space in the store buffer, move to Sn, otherwise, remain
+ in Su. Eliminate cases where sbState/sbState' are inconsistent. *)
+ - now rewrite Hsu;
+ destruct sbState, sbState', Hlsbt.
+
+ (* Sn: instructions remains in Sn. *)
+ - auto.
+ Qed.
+
+ Lemma unmoved_can_advance :
+ forall n, e = (opc, (st, n)) -> e = e' ->
+ compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+ Proof.
+ intros n He He'.
+
+ pose proof (unmoved_no_lat_can_advance) as Huca.
+ revert Huca.
+ work_on_e He'.
+ intro Huca.
+
+ destruct n.
+ - destruct (ready _ _ _ && free _ _ t _).
+ + rewrite (Huca (eq_refl _) (eq_refl _) (eq_refl _)).
+ apply compare_two_eq_true.
+ discriminate.
+ + now destruct (ready _ _ _ && free _ _ _ _), st;
+ [| destruct opc |..].
+
+ - apply compare_two_eq_true.
+ discriminate.
+ Qed.
End monotonicity.
Section constrained.
--
GitLab