From ccb0db5daa1a3e5ce6706a228e2564e6831e061c Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 17:56:29 +0200
Subject: [PATCH] definitions, correct_store_buffer: latencies in Loads
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 140 +++++++------------------------------
src/definitions.v | 24 +++++--
2 files changed, 42 insertions(+), 122 deletions(-)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 5f858ca..ddfcc00 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -5,7 +5,7 @@ Import ListNotations.
(* free and cycle functions. *)
Definition ready isSuUsed sbState (elt : instr_kind) :=
match elt with
- | (Load, (Lsu, _)) => busFree isSuUsed sbState
+ | (Load _, (Lsu, _)) => busFree isSuUsed sbState
| (_, (Su, _)) => negb (sbStateT_beq sbState Full)
| (_, (Lu, S _)) => false
| _ => true
@@ -51,7 +51,10 @@ Definition cycle_elt isSuUsed sbState trace elt :=
| (opc, (st, S n)) => (opc, (st, n))
| (opc, (st, 0)) =>
if ready isSuUsed sbState elt && free isSuUsed sbState trace elt then
- (opc, (nstg st opc, 0))
+ match opc, nstg st opc with
+ | Load n, Lu => (Load n, (Lu, n))
+ | opc, nstg => (opc, (nstg, 0))
+ end
else
elt
end.
@@ -63,8 +66,8 @@ Definition cycle sbState trace :=
Definition is_constrained (elt : instr_kind) trace sbState :=
match elt, sbState with
| (_, (Sp, _)), _ => List.existsb is_in_lsu trace
- | (Load, (Lsu, _)), Empty => List.existsb is_in_lu trace || List.existsb is_in_su trace
- | (Load, (Lsu, _)), _ => true
+ | (Load _, (Lsu, _)), Empty => List.existsb is_in_lu trace || List.existsb is_in_su trace
+ | (Load _, (Lsu, _)), _ => true
| (Store, (Lsu, _)), _ => List.existsb is_in_su trace
| _, _ => false
end.
@@ -148,7 +151,7 @@ Section monotonicity.
Hypothesis Htc' : tc' = cycle sbState' t'.
Hypothesis Hlsbt : legal_sb_transitions st sbState sbState'.
Hypothesis HlsbtP : legal_sb_transitions_P (existsb is_in_su t) (existsb is_in_su t') sbState sbState'.
- Hypothesis Hlu : forall st opc, st = Lu -> opc = Load.
+ Hypothesis Hlu : forall st opc n, st = Lu -> opc = Load n.
Hypothesis Hsu : forall st opc, st = Su -> opc = Store.
(* Long hypotheses related to stage occupation. *)
@@ -175,11 +178,11 @@ Section monotonicity.
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)).
+ e = (opc, (st, 0)) -> e = e' -> forall n,
+ List.nth_error tc i = Some (opc, (nstg st opc, n)) ->
+ List.nth_error tc' i = Some (opc, (nstg st opc, n)).
Proof.
- intros He He'.
+ intros He He' n.
specialize (Hlu st opc).
specialize (Hsu st opc).
@@ -221,7 +224,7 @@ Section monotonicity.
+ discriminate.
(* Lu: instructions without latency (this is the case here) move to Sn. *)
- - now rewrite Hlu.
+ - now rewrite (Hlu n).
(* Su: if there is space in the store buffer, move to Sn, otherwise, remain
in Su. Eliminate cases where sbState/sbState' are inconsistent. *)
@@ -245,11 +248,14 @@ Section monotonicity.
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 |..].
+ + specialize (Huca (eq_refl _) (eq_refl _)).
+ now destruct opc, (nstg _ _);
+ rewrite (Huca 0 (eq_refl _))
+ || (rewrite (Huca n (eq_refl _));
+ apply compare_two_eq_true).
+ + destruct (ready _ _ _ && free _ _ _ _), st;
+ try reflexivity;
+ now destruct opc.
- apply compare_two_eq_true.
discriminate.
@@ -263,7 +269,6 @@ Section monotonicity.
compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
Proof.
intros He He' Hed Hsl.
- specialize (Hlu st opc).
specialize (Hsu st' opc).
(* work_on_e replacement. *)
@@ -286,7 +291,7 @@ Section monotonicity.
(* st = Sp, st' = Lsu, Lu, Su, Sn *)
- now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
- now destruct (ready _ _ _ && free _ _ _ _), opc.
- - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _).
+ - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
- now destruct (ready _ _ _ && free _ _ _ _), opc.
(* st = Lsu, st' = Lu, Su, Sn *)
@@ -297,106 +302,9 @@ Section monotonicity.
- now destruct (ready _ _ _ && free _ _ _ _), opc.
(* st = Lu, st' = Sn *)
- - now destruct opc;
- [| discriminate Hlu].
+ - now destruct opc.
(* st = Su, st' = Sn *)
- - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _).
+ - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
Qed.
End monotonicity.
-
-Section constrained.
- Variable opc : opcode.
- Variable e d : instr_kind.
- Variable t tpre tpost t' tpre' tpost' tc tc' : trace_kind.
- Variable i : nat.
- Variable sbState sbState' : sbStateT.
-
- Hypothesis Ht : t = tpre ++ e :: tpost.
- Hypothesis Ht' : t' = tpre' ++ e :: tpost'.
- Hypothesis Hi : i = List.length tpre.
- Hypothesis Hl : List.length tpre' = List.length tpre.
- Hypothesis Hl' : List.length tpost' = List.length tpost.
- Hypothesis Htc : tc = cycle sbState t.
- Hypothesis Htc' : tc' = cycle sbState' t'.
- Hypothesis HconstT : is_constrained e t sbState = true.
-
- (* Delve into tc, tc', cycle, cycle_elt, etc.
- * Pretty specific to these constraints, do not use it outside this section. *)
- Ltac constraint_delve He :=
- rewrite Htc, Htc';
- unfold cycle;
- rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _),
- (map_in_the_middle _ _ e d _ _ tpre' tpost' _);
- [ unfold cycle_elt;
- destruct e;
- match goal with
- | [ s : state |- _ ] =>
- destruct s;
- injection He;
- intros Hn Hs Ho;
- rewrite Ho, Hs, Hn;
- simpl
- end |
- exact Ht' |
- rewrite Hi, Hl;
- reflexivity |
- exact Ht |
- exact Hi ].
-
- (* If a constrained Sp can advance, an unconstrained Sp can advance. *)
- Theorem constrained_sp_can_advance_unconstrained_too :
- (* t is constrained, t' is unconstrained *)
- e = (opc, (Sp, 0)) -> is_constrained e t' sbState' = false ->
- List.nth_error tc i = Some (opc, (Lsu, 0)) -> List.nth_error tc' i = Some (opc, (Lsu, 0)).
- Proof.
- intros He HconstT'.
- rewrite He in HconstT'.
-
- constraint_delve He.
-
- unfold lsuFree, get_instr_in_stage.
- rewrite (not_existsb_means_cannot_find _ _ t');
- now destruct opc.
- Qed.
-
- (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
- (* Load version *)
- Theorem constrained_lsu_load_advance_unconstrained_too :
- (* t is constrained, t' is unconstrained *)
- e = (Load, (Lsu, 0)) -> is_constrained e t' sbState' = false ->
- List.nth_error tc i = Some (Load, (Lu, 0)) -> List.nth_error tc' i = Some (Load, (Lu, 0)).
- Proof.
- intro He.
-
- rewrite He.
- unfold is_constrained.
- destruct sbState';
- try discriminate.
- intro HconstT'.
- apply orb_false_elim in HconstT'.
- destruct HconstT' as [HconstT' HconstT'2].
-
- constraint_delve He.
-
- unfold luFree, get_instr_in_stage.
- rewrite (not_existsb_means_cannot_find _ _ t').
- - now rewrite HconstT'2.
- - exact HconstT'.
- Qed.
-
- (* Store version *)
- Theorem constrained_lsu_store_advance_unconstrained_too :
- (* t is constrained, t' is unconstrained *)
- e = (Store, (Lsu, 0)) -> is_constrained e t' sbState' = false ->
- List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
- Proof.
- intros He HconstT'.
- rewrite He in HconstT'.
-
- constraint_delve He.
-
- unfold suFree, get_instr_in_stage.
- now rewrite (not_existsb_means_cannot_find _ _ t').
- Qed.
-End constrained.
diff --git a/src/definitions.v b/src/definitions.v
index 77197b7..b1f10eb 100644
--- a/src/definitions.v
+++ b/src/definitions.v
@@ -7,11 +7,23 @@ Import ListNotations.
(* Basic definitions: opcodes, stages, store buffer state. *)
Variant opcode :=
- | Load
- | Store.
+ | Load : nat -> opcode
+ | Store : opcode.
Scheme Equality for opcode.
+Definition is_load opc :=
+ match opc with
+ | Load _ => True
+ | Store => False
+ end.
+
+Definition is_store opc :=
+ match opc with
+ | Load _ => False
+ | Store => True
+ end.
+
Variant stage :=
| Sp
| Lsu
@@ -29,7 +41,7 @@ Qed.
Definition nstg s opc :=
match s, opc with
| Sp, _ => Lsu
- | Lsu, Load => Lu
+ | Lsu, Load _ => Lu
| Lsu, Store => Su
| _, _ => Sn
end.
@@ -253,7 +265,7 @@ Definition check_latencies trace :=
Definition check_loads_and_stores trace :=
List.forallb (fun (elt : instr_kind) =>
match elt with
- | (Load, (Su, _))
+ | (Load _, (Su, _))
| (Store, (Lu, _)) => false
| _ => true
end) trace.
@@ -317,9 +329,9 @@ Section check_correctness.
Qed.
Lemma check_loads_and_stores_is_correct_v1 :
- e = (Load, (Su, lat)) -> check_loads_and_stores t = false.
+ forall n, e = (Load n, (Su, lat)) -> check_loads_and_stores t = false.
Proof.
- intro He.
+ intros n He.
rewrite <- Htstep in Ht.
rewrite (check_loads_and_stores_is_correct_v0 t t1 tstep).
--
GitLab