diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v deleted file mode 100644 index 252ca6ec1fa9b86251c58ab816adcedee9b1ce6c..0000000000000000000000000000000000000000 --- a/src/correct_store_buffer.v +++ /dev/null @@ -1,519 +0,0 @@ -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. *) diff --git a/src/definitions.v b/src/definitions.v deleted file mode 100644 index 122ca502c4af00283ee818cec3951597ee369f9d..0000000000000000000000000000000000000000 --- a/src/definitions.v +++ /dev/null @@ -1,227 +0,0 @@ -(* 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. diff --git a/src/store_buffer.v b/src/store_buffer.v deleted file mode 100644 index dcfd33a4f73f64bb38170b8163dddefa5bb382dd..0000000000000000000000000000000000000000 --- a/src/store_buffer.v +++ /dev/null @@ -1,334 +0,0 @@ -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.