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

src: remove old files 


Signed-off-by: default avatarAlban Gruin <alban.gruin@irit.fr>
parent a9b3dd9c
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/correct_store_buffer.v deleted 100644 → 0
+ 0
− 519
View file @ a9b3dd9c
Require Import Bool Lia List Nat PeanoNat.
From StoreBuffer Require Import definitions utils.
Import ListNotations.
(* free and cycle functions. *)
Definition ready isSuUsed sbState (elt : instr_kind) :=
match elt with
| (Load _, (Lsu, _)) => busFree isSuUsed sbState
| (_, (Su, _)) => negb (sbStateT_beq sbState Full)
| (_, (Lu, S _)) => false
| _ => true
end.
Definition luFree isSuUsed sbState trace :=
let instr := get_instr_in_stage trace Lu in
match instr with
| Some elt => ready isSuUsed sbState elt (* Sn is always free *)
| None => true
end.
Definition suFree isSuUsed sbState trace :=
let instr := get_instr_in_stage trace Su in
match instr with
| Some elt => ready isSuUsed sbState elt (* Sn is always free *)
| None => true
end.
Definition lsuFree isSuUsed sbState trace :=
let instr := get_instr_in_stage trace Lsu in
match instr with
| Some (opcode, (stg, lat)) => ready isSuUsed sbState (opcode, (stg, lat)) &&
if stage_beq (nstg stg opcode) Lu then
luFree isSuUsed sbState trace
else
suFree isSuUsed sbState trace
| None => true
end.
Definition free isSuUsed sbState trace (elt : instr_kind) :=
let (opc, state) := elt in
let (st, _) := state in
match nstg st opc with
| Lu => luFree isSuUsed sbState trace
| Su => suFree isSuUsed sbState trace
| Lsu => lsuFree isSuUsed sbState trace
| _ => true
end.
Definition cycle_elt isSuUsed sbState trace elt :=
match elt with
| (opc, (st, S n)) => (opc, (st, n))
| (opc, (st, 0)) =>
if ready isSuUsed sbState elt && free isSuUsed sbState trace elt then
match opc, nstg st opc with
| Load n, Lu => (Load n, (Lu, n))
| opc, nstg => (opc, (nstg, 0))
end
else
elt
end.
Definition cycle sbState trace :=
let isSuUsed := List.existsb is_in_su trace in
List.map (cycle_elt isSuUsed sbState trace) trace.
Definition legal_sb_transitions st sbState sbState' :=
match st, sbState with
| Su, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
| Su, Empty => sbState' = Empty
| _, _ => sbState' = Full \/ sbState' = NotEmpty \/ sbState' = Empty
end.
Section monotonicity.
Variable opc : opcode.
Variable d : instr_kind.
Variable st st' : stage.
Variable t tpre tpost t' tpre' tpost' tc tc' : trace_kind.
Variable sbState sbState' : sbStateT.
Hypothesis Hleb : pipeline_leb t t' = true.
Hypothesis Hl : pipeline_leb tpre tpre' = true.
Hypothesis Hl' : pipeline_leb tpost tpost' = true.
Hypothesis Htc : tc = cycle sbState t.
Hypothesis Htc' : tc' = cycle sbState' t'.
Hypothesis Hlsbt : legal_sb_transitions st sbState sbState'.
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. *)
Hypothesis HfreeLsuPersists :
free (existsb is_in_su t) sbState t (opc, (Sp, 0)) = true ->
free (existsb is_in_su t') sbState' t' (opc, (Sp, 0)) = true.
Hypothesis HfreeFromLsuPersists :
free (existsb is_in_su t) sbState t (opc, (Lsu, 0)) = true ->
free (existsb is_in_su t') sbState' t' (opc, (Lsu, 0)) = true.
Hypothesis HbusFree :
forall st, st = Lsu ->
busFree (existsb is_in_su t) sbState = true ->
busFree (existsb is_in_su t') sbState' = true.
Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.
Hypothesis HvalidLdLat : forall (e : instr_kind) st n dlat, e = (Load dlat, (st, n)) -> 0 <> n -> st = Lu /\ n <= dlat.
Section simple_monotonicity.
Variable e e' : instr_kind.
Variable i : nat.
Hypothesis Ht : t = tpre ++ e :: tpost.
Hypothesis Ht' : t' = tpre' ++ e' :: tpost'.
Hypothesis Hi : i = List.length tpre.
Hypothesis Hi' : i = List.length tpre'.
Ltac work_on_e He' :=
rewrite Htc, Htc', Ht;
match goal with
| [ _ : e = e' |- _ ] =>
rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- *
| [ _ : e <> e' |- _ ] =>
rewrite Ht'
end;
unfold cycle;
rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ eq_refl Hi),
(map_in_the_middle _ _ _ d _ _ tpre' tpost' _ eq_refl Hi');
unfold cycle_elt;
rewrite <- Ht;
match goal with
| [ _ : e = e' |- _ ] =>
subst e
| [ _ : e <> e' |- _ ] =>
rewrite <- Ht';
subst e;
subst e'
end.
Lemma unmoved_no_lat_can_advance :
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' n.
specialize (Hlu st opc).
specialize (Hsu st opc).
specialize (HbusFree st).
(* 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 n).
(* 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;
try discriminate
|].
(* Sn: instructions remains in Sn. *)
- auto.
Qed.
Lemma unmoved_is_monotonic :
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'.
(* Extract e. *)
pose proof unmoved_no_lat_can_advance as Huca.
revert Huca.
work_on_e He'.
intro Huca.
destruct n.
- (* Case where an instruction has a latency of 0. *)
destruct (ready _ _ _ && free _ _ t _).
+ (* If e (in t) can progress. *)
(* apply unmoved_no_lat_can_advance, with all relevant parameters. *)
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).
+ (* If e (in t) cannot progress. *)
destruct (_ && _).
* (* If e (in t') can progress. cycle_elt e t' > cycle_elt e t. This
* is trivial, but each case must be analysed separately. *)
now destruct st, opc.
* (* If e (in t') cannot progress. cycle_elt e t' = cycle e t. This
* is also trivial. *)
now apply compare_two_eq_true.
- (* Case where an instruction has a latency higher than 0. *)
(* cycle_elt ... e = cycle_elt ... e'. Then, compare_two ... = true. *)
now apply compare_two_eq_true.
Qed.
Lemma moved_no_lat_is_monotonic :
e = (opc, (st, 0)) -> e' = (opc, (st', 0)) -> e <> e' ->
state_leb (st, 0) (st', 0) = true ->
compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
Proof.
intros He He' Hed Hsl.
specialize (Hlu st opc 0).
pose proof (Hsu st' opc) as Hsu'.
specialize (Hsu st opc).
(* Goal transformation: show exactly how e and e' are modified by the
* cycle function. *)
work_on_e Hed.
(* Case-by-case analysis *)
destruct st, st';
try contradiction;
try discriminate.
(* 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 _ _ _ _), opc.
- now destruct (ready _ _ _ && free _ _ _ _), opc.
(* st = Lsu, st' = Lu, Su, Sn *)
- now destruct (ready _ _ _ && free _ _ _ _), opc.
- destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc;
try reflexivity.
now discriminate Hsu'.
- now destruct (ready _ _ _ && free _ _ _ _), opc.
(* st = Lu, st' = Sn *)
- now destruct opc;
(* Trivial when opc = Load, eliminate the case where opc = Store. *)
[| discriminate Hlu].
(* st = Su, st' = Sn *)
- now destruct opc; [
(* Eliminate the case where opc = Load. *)
discriminate Hsu |
(* Either the instruction remains in Su, or it progresses in Sn. *)
(* Both cases are trivial. *)
destruct (_ && _)
].
Qed.
Lemma moved_lat_is_monotonic :
forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) -> e <> e' ->
state_leb (st, n) (st', n') = true ->
compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
Proof.
intros n n' He He' Hed Hsl.
pose proof (HvalidStLat e' st' n') as HvalidStLat'.
specialize (HvalidStLat e st n).
pose proof (HvalidLdLat e' st' n') as HvalidLdLat'.
specialize (HvalidLdLat e st n).
destruct n, n'; [
(* n and n' are = 0. We have a lemma for that. *)
now apply moved_no_lat_is_monotonic |
(* Other cases: rewrite the goal to make cycle appear. *)
work_on_e Hed;
(* Since n or n' is not equal to 0, opc is a load. Remove other cases. *)
destruct opc;
[| discriminate (HvalidStLat eq_refl)
|| discriminate (HvalidStLat' eq_refl)] ..
].
(* From there, opc = Load. *)
(* n = 0 and n' <> 0. *)
- (* st' = Lu. *)
destruct (HvalidLdLat' n eq_refl (O_S n')) as [Hst' Hlat'].
rewrite Hst' in Hsl, Hed |- *.
destruct st;
try discriminate.
+ (* 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.
* reflexivity.
(* n <> 0 and n' = 0. *)
- (* st = Lu. *)
destruct (HvalidLdLat n0 eq_refl (O_S n)) as [Hst Hlat].
rewrite Hst in Hsl, Hed |- *.
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.
Theorem is_monotonic :
forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) ->
state_leb (st, n) (st', n') = true ->
compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
Proof.
intros n n' He He' Hsl.
pose proof (instr_kind_is_comparable e e') as Heqd.
(* e = e' or e <> e'. *)
destruct Heqd as [Heq | Hdiff].
- (* If e = e', we have a lemma for this. *)
now apply (unmoved_is_monotonic n).
- (* If e <> e', we have a lemma for this. *)
now apply (moved_lat_is_monotonic n n').
Qed.
End simple_monotonicity.
Lemma tc_and_tc' : List.length tc = List.length tc'.
Proof.
(* i = length tpre = length tpre'. *)
(* length t = length t'. *)
(* cycle t = map ... t. *)
(* length (map ... t) = length t. *)
rewrite Htc, Htc'.
unfold cycle.
repeat rewrite map_length.
unfold pipeline_leb in Hleb.
now rewrite andb_true_iff, Nat.eqb_eq in Hleb.
Qed.
Variable e e' : instr_kind.
Variable n n' : nat.
Hypothesis Ht : t = tpre ++ e :: tpost.
Hypothesis Ht' : t' = tpre' ++ e' :: tpost'.
Hypothesis Hi : forall i, i = List.length tpre.
Hypothesis Hi' : forall i, i = List.length tpre'.
Hypothesis He : e = (opc, (st, n)).
Hypothesis He' : e' = (opc, (st', n')).
Hypothesis Hsl : state_leb (st, n) (st', n') = true.
Let is_monotonic' ni :=
is_monotonic e e' ni Ht Ht' (Hi ni) (Hi' ni) n n' He He' Hsl.
Lemma cycled_instrs_are_leb :
forall instrs, In instrs (combine tc tc') -> instrs_leb instrs = true.
Proof.
(* Since instrs is in (combine tc tc'), there is a
* i' < length (combine tc tc') and
* nth i' (combine tc tc') (d, d)) = instrs. *)
intros instrs HIn.
destruct (In_nth (combine tc tc') instrs (d, d) HIn) as [i HInth].
destruct HInth as [Hil Hinstrs].
(* since nth i (combine tc tc') = instrs,
* instrs = (nth i tc d, nth i tc' d). *)
rewrite combine_nth in Hinstrs.
- (* instrs_leb instrs = true means
* compare_two (nth_error tc i) (nth_error tc' i) = true.
* We have a lemma for this. *)
(* Then, compare_two (nth_error tc i) (nth_error tc' i) = true.
* We have a theorem for this. *)
rewrite <- Hinstrs.
apply (compare_two_true_means_instrs_leb tc tc' i d), (is_monotonic' i).
- (* length tc = length tc'. We have a lemma for this. *)
apply tc_and_tc'.
Qed.
Theorem is_fully_monotonic : pipeline_leb tc tc' = true.
Proof.
unfold pipeline_leb.
rewrite andb_true_iff.
split.
- (* First, length tc = length tc'. We have a lemma for this. *)
rewrite Nat.eqb_eq.
apply tc_and_tc'.
- (* Now, forallb instrs_leb (combine tc tc') = true. *)
(* Transform the goal into
* forall instrs, In instrs (combine ...) -> instrs_leb instrs = true. *)
rewrite forallb_forall.
intros instrs HIn.
(* We have a lemma for this. *)
now rewrite cycled_instrs_are_leb.
Qed.
End monotonicity.
Section monotonicity_everywhere.
Variable opc : opcode.
Variable d : instr_kind.
Variable t t' tc tc' : trace_kind.
Variable sbState sbState' : sbStateT.
Hypothesis Hleb : pipeline_leb t t' = true.
Hypothesis Htc : tc = cycle sbState t.
Hypothesis Htc' : tc' = cycle sbState' t'.
Hypothesis Hlsbt : forall st, legal_sb_transitions st sbState sbState'.
(* Hypothesis Hl : forall tpre tpre', pipeline_leb tpre tpre' = true. *)
(* Hypothesis Hl' : forall tpost tpost', pipeline_leb tpost tpost' = true. *)
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. *)
Hypothesis HfreeLsuPersists : forall opc,
free (existsb is_in_su t) sbState t (opc, (Sp, 0)) = true ->
free (existsb is_in_su t') sbState' t' (opc, (Sp, 0)) = true.
Hypothesis HfreeFromLsuPersists : forall opc,
free (existsb is_in_su t) sbState t (opc, (Lsu, 0)) = true ->
free (existsb is_in_su t') sbState' t' (opc, (Lsu, 0)) = true.
Hypothesis HbusFree :
forall st, st = Lsu ->
busFree (existsb is_in_su t) sbState = true ->
busFree (existsb is_in_su t') sbState' = true.
Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.
Hypothesis HvalidLdLat : forall (e : instr_kind) st n dlat, e = (Load dlat, (st, n)) -> 0 <> n -> st = Lu /\ n <= dlat.
Ltac destruct_lieoc H e tpre tpost i H' :=
destruct H as [e H], H as [tpre H], H as [tpost H], H as [i H], H as [H H'].
Theorem monotonicity_everywhere : pipeline_leb tc tc' = true.
Proof.
pose proof (tc_and_tc' t t' tc tc' sbState sbState' Hleb Htc Htc') as Hlength'.
pose proof Hleb as Htpre.
unfold pipeline_leb in Hleb.
rewrite andb_true_iff, Nat.eqb_eq in Hleb.
destruct Hleb as [Hlength _].
destruct (list_is_empty_or_composed _ t) as [Ht | Ht].
- apply eq_sym in Hlength.
rewrite Ht, length_zero_iff_nil in Hlength.
rewrite Ht in Htc.
rewrite Hlength in Htc'.
compute in Htc, Htc'.
now rewrite Htc, Htc'.
- destruct Ht as [e Ht], Ht as [tpre Ht], Ht as [tpost Ht], Ht as [i Ht], Ht as [Ht Hi].
pose proof (list_is_composed instr_kind e d t tpre tpost i Ht Hi t' Hlength) as Hlic.
destruct Hlic as [e' Hlic], Hlic as [tpre' Hlic], Hlic as [tpost' Ht'], Ht' as [Ht' Hi'].
assert (List.length tpre = List.length tpre') as HHH.
now rewrite Hi' in Hi.
apply (pipeline_sub_is_leb _ _ tpre tpre' tpost tpost' e e' Hlength HHH Ht Ht') in Htpre.
destruct Htpre as [Htpre Htpost], Htpost as [Htpost Hte].
destruct e eqn:He, e' eqn:He'.
destruct s, s0.
assert (o = o0).
admit.
Check is_fully_monotonic.
admit.
Admitted.
End monotonicity_everywhere.
(* - rewrite Ht in Hlength. *)
(* simpl in Hlength. *)
(* apply eq_sym in Hlength. *)
(* rewrite length_zero_iff_nil in Hlength. *)
(* now rewrite Hlength, Htcd. *)
(* - destruct Htcd as [e Htcd], Htcd as [tpre Htcd], Htcd as [tpost Htcd], Htcd as [i Htcd], Htcd as [Htcd Hi]. *)
(* destruct (list_is_empty_or_composed _ tc) as [Htcd | Htcd], (list_is_empty_or_composed _ tc') as [Htcd' | Htcd']; *)
(* match goal with *)
(* | [Ha : _ = [], Hb : (exists _, _) |- _] => *)
(* destruct_lieoc Hb e tpre tpost i Hb'; *)
(* rewrite Ha, Hb, app_length, <- Hb' in Hlength; *)
(* simpl in Hlength; *)
(* lia *)
(* | [_ : _ = [] |- _] => now rewrite Htcd, Htcd' *)
(* | _ => idtac *)
(* end. *)
(* destruct_lieoc Htcd e tpre tpost i Htcd_. *)
(* destruct Htcd' as [e' Htcd'], Htcd' as [tpre' Htcd'], Htcd' as [tpost' Htcd']. *)
(* inversion Htcd'. *)
(* exists i in Htcd'. *)
(* Check is_fully_monotonic. *)
src/definitions.v deleted 100644 → 0
+ 0
− 227
View file @ a9b3dd9c
(* definitions.v, defines common structures, such as opcodes, stages, and
various related proofs. *)
(* They may or may not be useful… *)
Require Import Bool List Nat PeanoNat.
From Coq.Arith Require Import Plus.
Import ListNotations.
(* Basic definitions: opcodes, stages, store buffer state. *)
Variant opcode :=
| Load : nat -> opcode
| Store : opcode.
Scheme Equality for opcode.
Variant stage :=
| Sp
| Lsu
| Lu
| Su
| Sn.
Scheme Equality for stage.
Lemma stage_beq_eq_true : forall s, stage_beq s s = true.
Proof.
now destruct s.
Qed.
Definition nstg s opc :=
match s, opc with
| Sp, _ => Lsu
| Lsu, Load _ => Lu
| Lsu, Store => Su
| _, _ => Sn
end.
(* Boolean stage comparison. Sp < Lsu < (Lu, Su) < Sn. *)
Definition leb x y :=
match x, y with
| Sp, _ => true
| _, Sn => true
| Sn, _ => false
| Lsu, Sp => false
| Lsu, _ => true
| Lu, Lu => true
| Lu, _ => false
| Su, Su => true
| Su, _ => false
end.
Variant sbStateT :=
| Empty
| NotEmpty
| Full.
Scheme Equality for sbStateT.
Definition busFree isSuUsed sbState :=
(sbStateT_beq sbState Empty) && (negb isSuUsed).
(* State of an instruction in the pipeline. *)
Definition state := (stage * nat)%type.
(* Comparison between two states. *)
Definition state_leb st1 st2 :=
match st1, st2 with
| (s1, n1), (s2, n2) =>
if stage_beq s1 s2 then
Nat.leb n2 n1
else
leb s1 s2
end.
Lemma state_leb_eq_true : forall st, state_leb st st = true.
Proof.
intro st.
destruct st.
simpl.
now rewrite stage_beq_eq_true, Nat.leb_le.
Qed.
(* Type definitions etc. *)
Definition instr_kind := (opcode * state)%type.
Definition trace_kind := list instr_kind.
(* Lemma for comparison. *)
Lemma instr_kind_is_comparable : forall (e e' : instr_kind), (e = e') \/ (e <> e').
Proof.
repeat decide equality.
Qed.
(* Compare two with options. This will be necessary for proofs since we will
* make heavy use of List.nth_error. *)
Definition compare_two (e1 e2 : option instr_kind) :=
match e1, e2 with
| None, _
| _, None => false
| Some (_, st1), Some (_, st2) => state_leb st1 st2
end.
Lemma compare_two_eq_true : forall e, e <> None -> compare_two e e = true.
Proof.
intros e Hn.
destruct e as [i |].
- (* e = Some i *)
destruct i as [o s].
simpl.
(* state_leb s s = true, we have a lemma for this. *)
now rewrite state_leb_eq_true.
- (* None <> None. *)
contradiction.
Qed.
(* Pipeline comparison. *)
Definition instrs_leb (instrs : (instr_kind * instr_kind)) :=
match instrs with
| ((_, st1), (_, st2)) => state_leb st1 st2
(* | ((o1, st1), (o2, st2)) => opcode_beq o1 o2 && state_leb st1 st2 *)
end.
Definition pipeline_leb p1 p2 :=
let comb := List.combine p1 p2 in
Nat.eqb (List.length p1) (List.length p2) && List.forallb instrs_leb comb.
Section pipeline_comparison.
Variable t t' : trace_kind.
Variable i : nat.
Variable d : instr_kind.
Hypothesis Hct : compare_two (List.nth_error t i) (List.nth_error t' i) = true.
Lemma compare_two_true_means_exists :
(exists e, List.nth_error t i = Some e)
/\ (exists e, List.nth_error t' i = Some e).
split.
- (* First case. *)
destruct (nth_error t _).
+ now exists i0. (* Some i0 = Some e -> i0 = e. *)
+ discriminate. (* compare_two None ... = true is a contradiction. *)
- (* Second case. *)
destruct (nth_error t' _).
+ now exists i0. (* Some i0 = Some e -> i0 = e. *)
+ (* compare_two ... None = true is a contradiction, with extra steps. *)
destruct (nth_error t _).
* simpl in Hct.
destruct i0.
discriminate.
* discriminate.
Qed.
Lemma compare_two_true_means_instrs_leb :
instrs_leb (List.nth i t d, List.nth i t' d) = true.
Proof.
destruct compare_two_true_means_exists as [Hec Hec'].
destruct Hec as [ec Hnth], Hec' as [ec' Hnth'].
rewrite Hnth, Hnth' in Hct.
now rewrite (nth_error_nth t i d Hnth), (nth_error_nth t' i d Hnth').
Qed.
End pipeline_comparison.
Lemma combine_app :
forall (A B : Type) (l1 l2 : list A) (l1' l2' : list B),
length l1 = length l1' ->
combine (l1 ++ l2) (l1' ++ l2') = combine l1 l1' ++ combine l2 l2'.
Proof.
intros A B l1 l2.
induction l1 as [| a l1 IHl1];
destruct l1'.
- reflexivity.
- discriminate.
- discriminate.
- simpl.
intros l2' Hlength.
rewrite IHl1.
+ reflexivity.
+ now apply eq_add_S.
Qed.
Lemma pipeline_sub_is_leb :
forall (t t' tpre tpre' tpost tpost' : trace_kind) (e e' : instr_kind),
List.length t = List.length t' -> List.length tpre = List.length tpre' ->
t = tpre ++ e :: tpost -> t' = tpre' ++ e' :: tpost' ->
pipeline_leb t t' = true ->
pipeline_leb tpre tpre' = true /\ pipeline_leb tpost tpost' = true /\
(let (_, st1) := e in let (_, st2) := e' in state_leb st1 st2) = true.
Proof.
intros t t' tpre tpre' tpost tpost' e e' Hlength Hlength' Ht Ht' Hleb.
unfold pipeline_leb in Hleb |- *.
rewrite andb_true_iff, Nat.eqb_eq in Hleb |- *.
destruct Hleb as [_ Hforall].
rewrite Ht, Ht', combine_app, forallb_app, andb_true_iff in Hforall;
[| exact Hlength'].
destruct Hforall as [Hfpre Hfpost].
simpl in Hfpost.
rewrite andb_true_iff in Hfpost.
destruct Hfpost as [He Hfpost].
split.
- now split.
- rewrite andb_true_iff, Nat.eqb_eq.
split;
try split;
try assumption.
rewrite Ht, Ht', app_length, app_length, Hlength' in Hlength.
apply plus_reg_l in Hlength.
simpl in Hlength.
auto.
Qed.
(* Helper functions, may be useful to all implementations. *)
(* Check if an instruction is in a stage. *)
Definition is_in_stage st (instr : instr_kind) :=
match instr with
| (_, (st', _)) => stage_beq st st'
end.
(* Ready-to-use functions. *)
Definition is_in_su := is_in_stage Su.
Definition get_instr_in_stage trace st := List.find (is_in_stage st) trace.
src/store_buffer.v deleted 100644 → 0
+ 0
− 334
View file @ a9b3dd9c
Require Import Bool Lia List Nat PeanoNat.
From StoreBuffer Require Import definitions utils.
Import ListNotations.
(* free and cycle functions. *)
Definition ready isSuUsed dchit busTaken wbFull (elt : instr_kind) :=
match elt with
| (_, (Lsu, 0)) => dchit || (negb busTaken) || (negb (wbFull && isSuUsed))
| (_, (_, 0)) => true
| _ => false
end.
Definition lu_free isSuUsed dchit busTaken wbFull trace :=
let instr := get_instr_in_stage trace Lu in
match instr with
| Some elt => ready isSuUsed dchit busTaken wbFull elt
| None => true
end.
Definition su_free isSuUsed dchit busTaken wbFull trace :=
let instr := get_instr_in_stage trace Su in
match instr with
| Some elt => ready isSuUsed dchit busTaken wbFull elt
| None => true
end.
Definition lsu_free isSuUsed dchit busTaken wbFull trace :=
let instr := get_instr_in_stage trace Lsu in
match instr with
| Some (Load, _) => lu_free isSuUsed dchit busTaken wbFull trace
| Some (Store, _) => su_free isSuUsed dchit busTaken wbFull trace
| None => true
end.
Definition free isSuUsed dchit busTaken wbFull trace (elt : instr_kind) :=
let (opc, state) := elt in
let (st, _) := state in
match nstg st opc with
| Lu => lu_free isSuUsed dchit busTaken wbFull trace
| Su => su_free isSuUsed dchit busTaken wbFull trace
| Lsu => lsu_free isSuUsed dchit busTaken wbFull trace
| _ => true
end.
Definition cycle_elt isSuUsed dchit busTaken wbFull trace elt :=
match elt with
| (opc, (st, S n)) => (opc, (st, n))
| (opc, (st, 0)) =>
if ready isSuUsed dchit busTaken wbFull elt
&& free isSuUsed dchit busTaken wbFull trace elt then
(opc, (nstg st opc, 0))
else
elt
end.
Definition cycle dchit busTaken wbFull trace :=
let isSuUsed := List.existsb is_in_su trace in
List.map (cycle_elt isSuUsed dchit busTaken wbFull trace) trace.
Section can_advance.
Variable isSuUsed dchit busTaken wbFull : bool.
Variable n : nat.
Variable t : trace_kind.
Theorem su_can_advance : ready isSuUsed dchit busTaken wbFull (Store, (Su, 0)) = true.
Proof.
reflexivity.
Qed.
Theorem lu_can_advance : ready isSuUsed dchit busTaken wbFull (Load, (Lu, 0)) = true.
Proof.
reflexivity.
Qed.
Theorem after_su_co :
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (Store, (Su, 0)))) = Sn.
Proof.
reflexivity.
Qed.
Theorem after_lu_co :
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (Load, (Lu, 0)))) = Sn.
Proof.
reflexivity.
Qed.
Theorem lu_with_latency :
cycle_elt isSuUsed dchit busTaken wbFull t (Load, (Lu, S n)) = (Load, (Lu, n)).
Proof.
reflexivity.
Qed.
Theorem load_cannot_be_in_su :
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (Load, (Lsu, 0)))) <> Su.
Proof.
destruct dchit, busTaken, wbFull, isSuUsed;
simpl;
try destruct (lu_free _ _ _ _ _);
discriminate.
Qed.
Theorem store_cannot_be_in_lu :
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (Store, (Lsu, 0)))) <> Lu.
Proof.
destruct dchit, busTaken, wbFull, isSuUsed;
simpl;
try destruct (su_free _ _ _ _ _);
discriminate.
Qed.
Theorem load_after_lsu_lsu_or_lu :
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (Load, (Lsu, 0)))) = Lu \/
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (Load, (Lsu, 0)))) = Lsu.
Proof.
destruct dchit, busTaken, wbFull, isSuUsed;
simpl;
try destruct (lu_free _ _ _ _ _);
(left; reflexivity) || (right; reflexivity).
Qed.
Theorem store_after_lsu_lsu_or_lu :
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (Store, (Lsu, 0)))) = Su \/
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (Store, (Lsu, 0)))) = Lsu.
Proof.
destruct dchit, busTaken, wbFull, isSuUsed;
simpl;
try destruct (su_free _ _ _ _ _);
(left; reflexivity) || (right; reflexivity).
Qed.
Theorem after_pre_lsu_or_pre :
forall opc,
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (opc, (Sp, 0)))) = Lsu \/
fst (snd (cycle_elt isSuUsed dchit busTaken wbFull t (opc, (Sp, 0)))) = Sp.
Proof.
intro opc.
destruct isSuUsed, dchit, busTaken, wbFull;
simpl;
destruct (lsu_free _ _ _ _ _);
(left; reflexivity) || (right; reflexivity).
Qed.
Lemma same_length :
List.length (cycle dchit busTaken wbFull t) = List.length t.
Proof.
unfold cycle.
apply List.map_length.
Qed.
Hypothesis Hn : n < List.length t.
Lemma combine_cycle :
forall comb, comb = List.combine t (cycle dchit busTaken wbFull t) ->
List.nth_error comb n <> None.
Proof.
intros comb Hcomb.
assert (List.length comb = List.length t).
- rewrite Hcomb, List.combine_length, same_length.
apply min_l, le_n.
- rewrite <- H in Hn.
apply List.nth_error_Some.
exact Hn.
Qed.
Theorem instruction_never_regresses :
forall t' e1, t' = cycle dchit busTaken wbFull t ->
List.nth_error t n = Some e1 ->
compare_two (List.nth_error t n) (List.nth_error t' n) = true.
Proof.
intros t' e1 Ht' He1.
rewrite Ht', He1.
unfold cycle.
rewrite (map_nth_error _ _ _ He1).
unfold compare_two.
destruct e1.
unfold cycle_elt.
destruct s, n0.
- destruct (ready _ _ _ _ _ && free _ _ _ _ _ _);
destruct s, o;
reflexivity.
- destruct s;
simpl;
rewrite Nat.leb_le;
lia.
Qed.
End can_advance.
Theorem instr_locked_means_not_ready_and_free :
forall opc st lat (e d : instr_kind) t tpre tpost t' i isSuUsed dchit busTaken wbFull,
st <> Sn -> e = (opc, (st, lat)) -> t = tpre ++ e :: tpost -> i = List.length tpre ->
isSuUsed = List.existsb is_in_su t -> t' = cycle dchit busTaken wbFull t ->
List.nth_error t i = List.nth_error t' i ->
(ready isSuUsed dchit busTaken wbFull e && free isSuUsed dchit busTaken wbFull t e) = false.
Proof.
intros opc st lat e d t tpre tpost t' i isSuUsed dchit busTaken wbFull.
intros Hst He Ht Hi HisSuUsed Ht'.
assert (List.nth_error t i = Some e) as Hnth.
- apply (nth_error_on_composed_list _ _ d _ tpre tpost);
assumption.
- rewrite Ht', Hnth.
unfold cycle.
rewrite (map_nth_error _ i t Hnth).
unfold cycle_elt.
destruct e, s, n.
+ rewrite HisSuUsed.
destruct (ready _ _ _ _ _ && free _ _ _ _ _ _).
* destruct s;
simpl;
try (destruct o;
intro Hs;
inversion Hs);
injection He;
intros Hlat Hst1;
rewrite <- Hst1 in Hst;
contradiction.
* reflexivity.
+ intro Hs.
injection Hs.
lia.
Qed.
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 dchit busTaken wbFull : bool.
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 dchit busTaken wbFull t.
Hypothesis Htc' : tc' = cycle dchit busTaken wbFull t'.
(* 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_advance_unconstrained_too :
e = (opc, (Sp, 0)) ->
(* t is constrained, t' is unconstrained *)
(List.existsb is_in_lsu t) = true -> (List.existsb is_in_lsu t') = false ->
List.nth_error tc i = Some (opc, (Lsu, 0)) -> List.nth_error tc' i = Some (opc, (Lsu, 0)).
Proof.
intros He HconstT HconstT'.
constraint_delve He.
unfold lsu_free, get_instr_in_stage.
rewrite (not_existsb_means_cannot_find _ _ t').
- reflexivity.
- assumption.
Qed.
(* If a constained Lsu can advance, an uncontrained Lsu can advance. *)
(* Load version *)
Theorem constrained_lsu_load_advance_unconstrained_too :
e = (Load, (Lsu, 0)) ->
(* t is constrained, t' is unconstrained *)
(List.existsb is_in_lu t) = true -> (List.existsb is_in_lu t') = false ->
(* Should be obvious *)
(List.existsb is_in_su t') = false ->
List.nth_error tc i = Some (Load, (Lu, 0)) -> List.nth_error tc' i = Some (Load, (Lu, 0)).
Proof.
intros He HconstT HconstT' HconstT'2.
constraint_delve He.
unfold lu_free, get_instr_in_stage.
rewrite (not_existsb_means_cannot_find _ _ t').
- rewrite HconstT'2.
destruct (dchit || negb busTaken).
+ reflexivity.
+ rewrite andb_false_r.
reflexivity.
- assumption.
Qed.
(* Store version *)
Theorem constrained_lsu_store_advance_unconstrained_too :
e = (Store, (Lsu, 0)) ->
(* t is constrained, t' is unconstrained *)
(List.existsb is_in_su t) = true -> (List.existsb is_in_su t') = false ->
List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
Proof.
intros He HconstT HconstT'.
constraint_delve He.
unfold su_free, get_instr_in_stage.
rewrite (not_existsb_means_cannot_find _ _ t').
- rewrite HconstT', andb_true_r, andb_false_r, orb_true_r.
reflexivity.
- assumption.
Qed.
End constrained.
Section progression.
Variable t tpre tpost tc : trace_kind.
Variable dchit busTaken wbFull : bool.
Hypothesis Htc : tc = cycle dchit busTaken wbFull t.
Hypothesis Hv : valid t = true.
End progression.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment