From f147e348e18544dc54298f87caa9b36f2656c129 Mon Sep 17 00:00:00 2001
From: Felipe Lisboa <lisboafelipe5@gmail.com>
Date: Tue, 30 Jan 2024 14:57:54 +0100
Subject: [PATCH] Finished refactoring FIFO conforming the new version of the
framework
---
framework/DRAM/Core/Address.v | 7 +-
framework/DRAM/Core/Arbiter.v | 31 +
framework/DRAM/Core/BankMachine.v | 12 +-
framework/DRAM/Core/Commands.v | 15 +-
framework/DRAM/Core/ImplementationInterface.v | 20 +-
framework/DRAM/Core/InterfaceSubLayer.v | 32 +-
framework/DRAM/Core/Trace.v | 44 +-
framework/DRAM/Core/Util.v | 14 +-
.../Implementations/BM/FIFOimpSL/FIFOimpSL.v | 50 +
.../BM/FIFOimpSL/FIFOimpSL_sim.v | 102 +
.../DRAM/Implementations/BM/RRimpSL/RRimpSL.v | 100 +
.../Implementations/BM/RRimpSL/RRimpSL_sim.v | 111 +
.../Implementations/BM/TDMimpSL/TDMimpSL.v | 101 +
.../BM/TDMimpSL/TDMimpSL_sim.v | 111 +
.../Implementations/FIFOimpSL/FIFOimpSL.v | 66 -
.../FIFOimpSL/FIFOimpSL_test.v | 119 -
.../Implementations/{ => TS}/DynTDM/TDMds.v | 0
.../Implementations/{ => TS}/DynTDM/TDMes.v | 0
.../{ => TS}/DynTDM/TDMesREF.v | 0
.../{ => TS}/DynTDM/TDMesREFpg.v | 0
.../DRAM/Implementations/{ => TS}/FIFO/FIFO.v | 61 +-
.../{ => TS}/FIFO/FIFO_extraction.v | 0
.../{ => TS}/FIFO/FIFO_proofs.v | 3176 ++++++++---------
.../Implementations/{ => TS}/FIFO/FIFO_sim.v | 0
.../{ => TS}/FIFO/haskell_gencode_fifo/App.hs | 0
.../haskell_gencode_fifo/ForeignCommand.hsc | 0
.../haskell_gencode_fifo/ForeignCommand_t.h | 0
.../haskell_gencode_fifo/ForeignRequest.hsc | 0
.../haskell_gencode_fifo/ForeignRequest_t.h | 0
.../FIFO/haskell_gencode_fifo/MCsimRequest.h | 0
.../FIFO/haskell_gencode_fifo/README.md | 0
.../FIFO/haskell_gencode_fifo/main.cpp | 0
.../FIFO/haskell_gencode_fifo/makefile | 0
.../{ => TS}/FIFOImp2/FIFOImp2.v | 0
.../{ => TS}/FIFOImp2/FIFOImp2Properties.v | 0
.../{ => TS}/FIFOImp2/FIFOImp2Test.v | 0
.../DRAM/Implementations/{ => TS}/TDM/TDM.v | 56 +-
.../Implementations/{ => TS}/TDM/TDMREF.v | 0
.../{ => TS}/TDM/TDM_extraction.v | 0
.../Implementations/{ => TS}/TDM/TDM_proofs.v | 0
.../Implementations/{ => TS}/TDM/TDM_sim.v | 0
.../{ => TS}/TDM/haskell_gencode_tdm/App.hs | 0
.../haskell_gencode_tdm/ForeignCommand.hsc | 0
.../haskell_gencode_tdm/ForeignCommand_t.h | 0
.../haskell_gencode_tdm/ForeignRequest.hsc | 0
.../haskell_gencode_tdm/ForeignRequest_t.h | 0
.../TDM/haskell_gencode_tdm/MCsimRequest.h | 0
.../TDM/haskell_gencode_tdm/README.md | 0
.../{ => TS}/TDM/haskell_gencode_tdm/main.cpp | 0
.../{ => TS}/TDM/haskell_gencode_tdm/makefile | 0
framework/DRAM/_CoqProject | 12 +-
51 files changed, 2123 insertions(+), 2117 deletions(-)
create mode 100644 framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL.v
create mode 100644 framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL_sim.v
create mode 100644 framework/DRAM/Implementations/BM/RRimpSL/RRimpSL.v
create mode 100644 framework/DRAM/Implementations/BM/RRimpSL/RRimpSL_sim.v
create mode 100644 framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL.v
create mode 100644 framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_sim.v
delete mode 100644 framework/DRAM/Implementations/FIFOimpSL/FIFOimpSL.v
delete mode 100644 framework/DRAM/Implementations/FIFOimpSL/FIFOimpSL_test.v
rename framework/DRAM/Implementations/{ => TS}/DynTDM/TDMds.v (100%)
rename framework/DRAM/Implementations/{ => TS}/DynTDM/TDMes.v (100%)
rename framework/DRAM/Implementations/{ => TS}/DynTDM/TDMesREF.v (100%)
rename framework/DRAM/Implementations/{ => TS}/DynTDM/TDMesREFpg.v (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/FIFO.v (81%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/FIFO_extraction.v (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/FIFO_proofs.v (51%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/FIFO_sim.v (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/App.hs (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/ForeignCommand.hsc (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/ForeignCommand_t.h (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/ForeignRequest.hsc (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/ForeignRequest_t.h (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/MCsimRequest.h (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/README.md (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/main.cpp (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFO/haskell_gencode_fifo/makefile (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFOImp2/FIFOImp2.v (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFOImp2/FIFOImp2Properties.v (100%)
rename framework/DRAM/Implementations/{ => TS}/FIFOImp2/FIFOImp2Test.v (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/TDM.v (84%)
rename framework/DRAM/Implementations/{ => TS}/TDM/TDMREF.v (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/TDM_extraction.v (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/TDM_proofs.v (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/TDM_sim.v (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/App.hs (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/ForeignCommand.hsc (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/ForeignCommand_t.h (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/ForeignRequest.hsc (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/ForeignRequest_t.h (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/MCsimRequest.h (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/README.md (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/main.cpp (100%)
rename framework/DRAM/Implementations/{ => TS}/TDM/haskell_gencode_tdm/makefile (100%)
diff --git a/framework/DRAM/Core/Address.v b/framework/DRAM/Core/Address.v
index 415073f..25c14ea 100644
--- a/framework/DRAM/Core/Address.v
+++ b/framework/DRAM/Core/Address.v
@@ -12,14 +12,15 @@ Section Address.
(* ------------ Definition of Bankgroup ---------------- *)
Definition Bankgroup_t := { bg : nat | bg < BANKGROUPS }.
+ Check exist.
+
Program Definition Nat_to_bankgroup a : Bankgroup_t :=
match a < BANKGROUPS with
- | true => (exist _ a _) (* blank here is the proof that a satisfies P a *)
+ | true => (exist (fun x : nat => x < BANKGROUPS) a _) (* blank here is the proof that a satisfies P a *)
| false => (exist _ (BANKGROUPS - 1) _)
end.
Next Obligation.
- rewrite subn1 ltn_predL lt0n.
- by specialize BANKGROUPS_pos.
+ rewrite subn1 ltn_predL lt0n; by specialize BANKGROUPS_pos.
Qed.
Definition Bankgroup_to_nat (a : Bankgroup_t) : nat :=
diff --git a/framework/DRAM/Core/Arbiter.v b/framework/DRAM/Core/Arbiter.v
index 415bf87..8c56d19 100644
--- a/framework/DRAM/Core/Arbiter.v
+++ b/framework/DRAM/Core/Arbiter.v
@@ -38,6 +38,37 @@ Section Arbiter.
forall t, (Arbitrate t).(Time) == t
}.
+ Class SequentialConsistent_Arbiter {AF : Arrival_function_t} {AR : Arbiter_t} := mkSeqArbiter {
+
+ R2 : forall ta reqa tb reqb,
+ reqa \in (Arrival_at ta) -> (* reqa arrives at ta *)
+ reqb \in (Arrival_at tb) -> (* reqb arrives at tb *)
+ (* either reqa arrived before reqb OR
+ they arrived at the same instant, but there
+ is an arbitrary order between reqa and reqb,
+ and reqa is to be serviced before *)
+ (ta < tb) \/ (ta = tb /\ index reqa (Arrival_at ta) < index reqb (Arrival_at ta))
+ (* txa, the completion date of reqa must happen before txb,
+ the completion date of reqb *)
+ -> exists txa txb, (CAS_of_req reqa txa \in (Arbitrate txa).(Commands))
+ && (CAS_of_req reqb txb \in (Arbitrate txb).(Commands)) && (txa < txb)
+}.
+
+Class W_SequentialConsistent_Arbiter {AF : Arrival_function_t} {AR : Arbiter_t} := mkWSeqARbiter {
+ R2_relaxed : forall ta reqa tb reqb,
+ reqa \in (Arrival_at ta) -> (* reqa arrives at ta *)
+ reqb \in (Arrival_at tb) -> (* reqb arrives at tb *)
+ (ta < tb) \/
+ (ta = tb /\ index reqa (Arrival_at ta) < index reqb (Arrival_at ta))
+ (* Here, an additional pre-condition: reqa and reqb target the same row *) ->
+ reqa.(Address).(Row) = reqb.(Address).(Row) ->
+ (* txa, the completion date of reqa must happen before txb,
+ the completion date of reqb *)
+ exists txa txb,
+ (CAS_of_req reqa txa \in (Arbitrate txa).(Commands)) &&
+ (CAS_of_req reqb txb \in (Arbitrate txb).(Commands)) && (txa < txb)
+}.
+
Definition Default_arrival_at Input t :=
[seq x <- Input | x.(Date) == t].
diff --git a/framework/DRAM/Core/BankMachine.v b/framework/DRAM/Core/BankMachine.v
index 99b9afd..ad3e5e4 100644
--- a/framework/DRAM/Core/BankMachine.v
+++ b/framework/DRAM/Core/BankMachine.v
@@ -139,7 +139,7 @@ Section BankMachine.
Fixpoint map_arriving_req_to_cmd (Q : Requests_t) (m : ReqCmdMap_t) SS : ReqCmdMap_t :=
match Q with
| Datatypes.nil => m
- | req :: tl => (cmdGEN req SS) :: (map_arriving_req_to_cmd tl m SS)
+ | req :: tl => (map_arriving_req_to_cmd tl m SS) ++ [cmdGEN req SS]
end.
Fixpoint map_running_req_to_cmd (m : ReqCmdMap_t) SS : ReqCmdMap_t :=
@@ -147,17 +147,11 @@ Section BankMachine.
| nil => m
| hd :: tl =>
match hd with
- | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => (cmdGEN r SS) :: (map_running_req_to_cmd tl SS)
+ | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r =>
+ (cmdGEN r SS) :: (map_running_req_to_cmd tl SS)
| _ => (map_running_req_to_cmd tl SS)
end
end.
-
- Definition TDM (requestor : Requestor_t) (map : ReqCmdMap_t) : option Command_kind_t :=
- seq.ohead (filter (fun cmd =>
- match cmd with
- | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => r.(Requestor) == requestor
- | _ => false
- end) map).
Definition IssueREF (m : ReqCmdMap_t) SS :=
match pP with
diff --git a/framework/DRAM/Core/Commands.v b/framework/DRAM/Core/Commands.v
index 0955017..b67d2a2 100644
--- a/framework/DRAM/Core/Commands.v
+++ b/framework/DRAM/Core/Commands.v
@@ -2,9 +2,10 @@ Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From mathcomp Require Import ssreflect eqtype ssrbool ssrnat fintype div ssrZ zify.
-From Coq Require Import ProofIrrelevance.
-From DRAM Require Export Requests.
+From Coq Require Import ProofIrrelevance PeanoNat.
+
+From DRAM Require Export Requests.
Section Commands.
@@ -139,11 +140,11 @@ Section Commands.
Definition get_req (cmd : Command_t) : option Request_t :=
match cmd.(CKind) with
- | ACT r => Some r
- | CRD r => Some r
- | CRDA r => Some r
- | CWR r => Some r
- | CWRA r => Some r
+ | ACT r
+ | CRD r
+ | CRDA r
+ | CWR r
+ | CWRA r
| PRE r => Some r
| _ => None
end.
diff --git a/framework/DRAM/Core/ImplementationInterface.v b/framework/DRAM/Core/ImplementationInterface.v
index ea88240..595b4ef 100644
--- a/framework/DRAM/Core/ImplementationInterface.v
+++ b/framework/DRAM/Core/ImplementationInterface.v
@@ -13,24 +13,20 @@ Section ImplementationInterface.
Context {SYS_CFG : System_configuration}.
Context {REQUESTOR_CFG : Requestor_configuration}.
Context {ARBITER_CFG : Arbiter_configuration}.
-
- Record Arbiter_state_t := mkArbiterState
+
+ Class Implementation_t := mkImplementation
+ {
+ Init : Requests_t -> State_t;
+ Next : Requests_t -> State_t -> State_t * Command_kind_t;
+ }.
+
+ Record Arbiter_state_t := mkArbiterState
{
Arbiter_Commands : Commands_t;
Arbiter_Time : nat;
Implementation_State : State_t;
- (*
- Arbiter_Commands_date :
- forall c,
- c \in Arbiter_Commands -> c.(CDate) <= Arbiter_Time
- *)
- }.
- Class Implementation_t := mkImplementation
- {
- Init : Requests_t -> State_t;
- Next : Requests_t -> State_t -> State_t * Command_kind_t;
}.
(* Computes the t_th state *)
diff --git a/framework/DRAM/Core/InterfaceSubLayer.v b/framework/DRAM/Core/InterfaceSubLayer.v
index 30f1ef7..491fc3e 100644
--- a/framework/DRAM/Core/InterfaceSubLayer.v
+++ b/framework/DRAM/Core/InterfaceSubLayer.v
@@ -55,12 +55,12 @@ Section InterfaceSubLayer.
(* Schedule_In : forall m SYS_ST SCH_ST, m <> [] -> Schedule m SYS_ST SCH_ST \in m; *)
InitSchState : SchState_t;
- UpdatSchState : SystemState_t -> SchState_t -> SchState_t;
+ UpdatSchState : Command_kind_t -> ReqCmdMap_t -> SystemState_t -> SchState_t -> SchState_t;
}.
Context {SCH : Scheduler_t}.
- #[local] Instance ARBITER_CFG : Arbiter_configuration :=
+ #[global] Instance ARBITER_CFG : Arbiter_configuration :=
{
State_t := option ImplSubLayerState_t;
}.
@@ -69,7 +69,10 @@ Section InterfaceSubLayer.
(* --------------------------------------------------------------------------- *)
(* ------------------------------ Init function ------------------------------ *)
(* --------------------------------------------------------------------------- *)
- Definition InitBank : BankState_t := IDLE (mkLocalCounters 0 0 0 0 0 0).
+ (* Change this to start with the nominal value of constraints *)
+ Definition init_val := 1000.
+
+ Definition InitBank : BankState_t := IDLE (mkLocalCounters init_val init_val init_val init_val init_val init_val).
Lemma repeat_size {A} (x : A) (N : nat) :
size (repeat x N) == N.
@@ -80,13 +83,13 @@ Section InterfaceSubLayer.
Definition InitSS := (mkSystemState
(exist _ (repeat InitBank BANKS) (repeat_size InitBank BANKS))
(mkGlobalCounters
- (exist _ (repeat 0 3) (repeat_size 0 3))
- (exist _ (repeat 0 BANKGROUPS) (repeat_size 0 BANKGROUPS))
- 0
- (exist _ (repeat 0 BANKGROUPS) (repeat_size 0 BANKGROUPS))
- 0
- (exist _ (repeat 0 BANKGROUPS) (repeat_size 0 BANKGROUPS))
- 0) BRD).
+ (exist _ (repeat init_val 3) (repeat_size 0 3))
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ init_val
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ init_val
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ T_RFC) BRD).
Definition empty_rcmdmap : ReqCmdMap_t := [].
@@ -123,19 +126,22 @@ Section InterfaceSubLayer.
let sch_cmd := Schedule rdy_cmds SS SchS in
(* ------------------------ Updating phase ---------------------------- ----*)
(* If the scheduled command is CRD or CWR, remove it from the map *)
- let updated_map := seq.rem sch_cmd cmdmap'' in
+ let updated_map := (match sch_cmd with
+ | CRD _ | CRDA _ | CWR _ | CWRA _ => seq.rem sch_cmd cmdmap''
+ | _ => cmdmap''
+ end) in
(* Update the system *)
let SS' := SystemUpdate sch_cmd (Some SS) in
match SS' with
| None => (None,NOP)
| Some SS'valid =>
- let new_SchState := UpdatSchState SS SchS in
+ let new_SchState := UpdatSchState sch_cmd cmdmap'' SS SchS in
let new_ImplSubLayerState := mkImplSubLayerState SS'valid updated_map new_SchState in
(Some new_ImplSubLayerState, sch_cmd)
end
end.
- #[local] Instance ImplementationSubLayer : Implementation_t :=
+ #[global] Instance ImplementationSubLayer : Implementation_t :=
mkImplementation Init_SL_state Next_SL_state.
Definition get_cACTsb_ (SS : option SystemState_t) (bk : Bank_t) : option Counter_t :=
diff --git a/framework/DRAM/Core/Trace.v b/framework/DRAM/Core/Trace.v
index 31ce4fa..ce76072 100644
--- a/framework/DRAM/Core/Trace.v
+++ b/framework/DRAM/Core/Trace.v
@@ -42,6 +42,10 @@ Section Trace.
| a::S' => Diff_Bank_ a S' && Diff_Bank S'
end.
+ Definition Same_Row a b := (get_row a == get_row b).
+ Definition Same_Bank a b := (get_bank a == get_bank b).
+ Definition Same_Bankgroup a b := (get_bankgroup a == get_bankgroup b).
+
Record TestTrace_t := mkTestTrace
{
TestCommands : Commands_t;
@@ -67,22 +71,22 @@ Section Trace.
(* Ensure that the time between an ACT and a CAS commands respects T_RCD *)
Cmds_T_RCD_ok : forall a b, a \in Commands -> b \in Commands ->
- isACT a -> isCAS b -> (get_bank a == get_bank b) ->
+ isACT a -> isCAS b -> Same_Bank a b ->
Before a b -> Apart_at_least a b T_RCD;
(* Ensure that the time between a PRE and an ACT commands respects T_RP *)
Cmds_T_RP_ok : forall a b, a \in Commands -> b \in Commands ->
- isPRE a -> isACT b -> (get_bank a == get_bank b) ->
+ isPRE a -> isACT b -> Same_Bank a b ->
Before a b -> Apart_at_least a b T_RP;
(* Ensure that the time between two ACT commands respects T_RC *)
Cmds_T_RC_ok : forall a b, a \in Commands -> b \in Commands ->
- isACT a -> isACT b -> (get_bank a == get_bank b) ->
+ isACT a -> isACT b -> Same_Bank a b ->
Before a b -> Apart_at_least a b T_RC;
(* Maximum interval between ACT and PRE is T_RAS *)
Cmds_T_RAS_ok : forall a b, a \in Commands -> b \in Commands ->
- isACT a -> isPRE b -> (get_bank a == get_bank b) ->
+ isACT a -> isPRE b -> Same_Bank a b ->
Before a b -> Apart_at_least a b T_RAS;
(* RL *)
@@ -90,12 +94,12 @@ Section Trace.
(* Ensure that the time between a CRD and a PRE commands respects T_RTP *)
Cmds_T_RTP_ok : forall a b, a \in Commands -> b \in Commands ->
- isCRD a -> isPRE b -> (get_bank a == get_bank b) ->
+ isCRD a -> isPRE b -> Same_Bank a b ->
Before a b -> Apart_at_least a b T_RTP;
(* Ensure that the time between a CWR and a PRE commands respects T_WR + T_WL + T_BURST *)
Cmds_T_WTP_ok : forall a b, a \in Commands -> b \in Commands ->
- isCWR a -> isPRE b -> (get_bank a == get_bank b) ->
+ isCWR a -> isPRE b -> Same_Bank a b ->
Before a b -> Apart_at_least a b (T_WR + T_WL + T_BURST);
(* ------------------ Intra and Inter-bank constraints ----------------------- *)
@@ -105,19 +109,19 @@ Section Trace.
Apart_at_least a b T_RTW;
Cmds_T_WtoR_SBG_ok : forall a b, a \in Commands -> b \in Commands ->
- isCWR a -> isCRD b -> Before a b -> (get_bankgroup a == get_bankgroup b) ->
+ isCWR a -> isCRD b -> Before a b -> Same_Bankgroup a b ->
Apart_at_least a b (T_WTR_l + T_WL + T_BURST);
- Cmds_T_WtoR_DBG_ok : BANKGROUPS > 1 -> forall a b, a \in Commands -> b \in Commands ->
- isCWR a -> isCRD b -> Before a b -> ~~ (get_bankgroup a == get_bankgroup b) ->
+ Cmds_T_WtoR_DBG_ok : forall a b, a \in Commands -> b \in Commands ->
+ isCWR a -> isCRD b -> Before a b -> ~~ Same_Bankgroup a b ->
Apart_at_least a b (T_WTR_s + T_WL + T_BURST);
Cmds_T_CCD_SBG_ok : forall a b, a \in Commands -> b \in Commands ->
- (isCRD a /\ isCRD b) \/ (isCWR a /\ isCWR b) -> Before a b -> (get_bankgroup a == get_bankgroup b) ->
+ (isCRD a /\ isCRD b) \/ (isCWR a /\ isCWR b) -> Before a b -> Same_Bankgroup a b ->
Apart_at_least a b T_CCD_l;
- Cmds_T_CCD_DBG_ok : BANKGROUPS > 1 -> forall a b, a \in Commands -> b \in Commands ->
- (isCRD a /\ isCRD b) \/ (isCWR a /\ isCWR b)-> Before a b -> ~~ (get_bankgroup a == get_bankgroup b) ->
+ Cmds_T_CCD_DBG_ok : forall a b, a \in Commands -> b \in Commands ->
+ (isCRD a /\ isCRD b) \/ (isCWR a /\ isCWR b)-> Before a b -> ~~ Same_Bankgroup a b ->
Apart_at_least a b T_CCD_s;
(* ------------------ Refresh-related constraints -------------------------- *)
@@ -135,11 +139,11 @@ Section Trace.
Apart_at_least a d T_FAW;
Cmds_T_RRD_SBG_ok : forall a b, a \in Commands -> b \in Commands ->
- isACT a -> isACT b -> ~~ (get_bank a == get_bank b) -> (get_bankgroup a == get_bankgroup b) ->
+ isACT a -> isACT b -> ~~ Same_Bank a b -> Same_Bankgroup a b ->
Before a b -> Apart_at_least a b T_RRD_l;
- Cmds_T_RRD_DBG_ok : BANKGROUPS > 1 -> forall a b, a \in Commands -> b \in Commands ->
- isACT a -> isACT b -> ~~ (get_bank a == get_bank b) -> ~~ (get_bankgroup a == get_bankgroup b) ->
+ Cmds_T_RRD_DBG_ok : forall a b, a \in Commands -> b \in Commands ->
+ isACT a -> isACT b -> ~~ Same_Bank a b -> ~~ Same_Bankgroup a b ->
Before a b -> Apart_at_least a b T_RRD_s;
(* ------------------------------------------------------------------------- *)
@@ -147,18 +151,18 @@ Section Trace.
(* ------------------------------------------------------------------------- *)
Cmds_ACT_ok: forall a b, a \in Commands -> b \in Commands ->
- isACT a \/ isCAS a -> isACT b -> (get_bank a == get_bank b) -> Before a b ->
- exists c, (c \in Commands) && (isPRE c) && (get_bank b == get_bank c) && (get_bank a == get_bank c)
+ isACT a \/ isCAS a -> isACT b -> Same_Bank a b -> Before a b ->
+ exists c, (c \in Commands) && (isPRE c) && Same_Bank b c && Same_Bank a c
&& (After c a) && (Before c b);
(* Every CAS command is preceded by a matching ACT without another ACT or PRE in between *)
Cmds_row_ok : forall b c, b \in Commands -> c \in Commands ->
- isCAS b -> isPRE c -> (get_bank b == get_bank c) -> Before c b ->
- exists a, (a \in Commands) && (isACT a) && (get_row a == get_row b) && (After a c) && (Before a b);
+ isCAS b -> isPRE c -> Same_Bank b c -> Before c b ->
+ exists a, (a \in Commands) && (isACT a) && Same_Row a b && (After a c) && (Before a b);
(* implies the init state of the memory *)
Cmds_initial : forall b, b \in Commands -> isCAS b ->
- exists a, (a \in Commands) && (isACT a) && (get_row a == get_row b) && (Before a b);
+ exists a, (a \in Commands) && (isACT a) && Same_Row a b && (Before a b);
(* Banks must be idle for at least T_RP cycles before a REF is issued *)
Cmds_REF_ok : forall ref, ref \in Commands ->
diff --git a/framework/DRAM/Core/Util.v b/framework/DRAM/Core/Util.v
index add5fa6..6cd8519 100644
--- a/framework/DRAM/Core/Util.v
+++ b/framework/DRAM/Core/Util.v
@@ -1,17 +1,11 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
-From mathcomp Require Import ssreflect ssrnat ssrbool seq eqtype div.
+From mathcomp Require Import ssreflect ssrnat ssrbool seq eqtype div zify.
-Lemma nat_ltn_leq_pred m n :
- (m < n) -> (m <= n.-1).
-Proof.
-Admitted.
-
-Lemma nat_add_pred m n :
- (m + n).-1 = m + n.-1.
-Proof.
-Admitted.
+Lemma nat_ltn_leq_pred x y :
+ y > 0 -> x <= (x + y).-1.
+Proof. lia. Qed.
Lemma nat_cancel_terms a:
a - a = 0.
diff --git a/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL.v b/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL.v
new file mode 100644
index 0000000..4347d7d
--- /dev/null
+++ b/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL.v
@@ -0,0 +1,50 @@
+Set Printing Projections.
+Set Warnings "-notation-overridden,-parsing".
+
+From mathcomp Require Import ssreflect eqtype ssrbool ssrnat fintype div ssrZ zify tuple.
+From Coq Require Import Program Equality.
+From DRAM Require Export InterfaceSubLayer.
+
+Section FIFOimpSL.
+
+ Context {SYS_CFG : System_configuration}.
+
+ #[global] Instance REQUESTOR_CFG : Requestor_configuration :=
+ {
+ Requestor_t := unit_eqType
+ }.
+
+ Context {SCH_OPT : SchedulingOptions_t}.
+ Context {AF : Arrival_function_t}.
+
+ Definition FIFO_internal_state := unit.
+
+ #[global] Instance SCH_ST : SchedulerInternalState := mkSIS FIFO_internal_state.
+
+ Definition FIFO_schedule
+ (map : ReqCmdMap_t)
+ (SS : SystemState_t)
+ (FIFO_st : FIFO_internal_state) : Command_kind_t :=
+ let cmd := seq.ohead map in
+ match cmd with
+ | Some cmd => cmd
+ | None => NOP
+ end.
+
+ Definition UpdatSchState (cmd : Command_kind_t) (cmd_map : ReqCmdMap_t) (SS : SystemState_t)
+ (FIFO_st : FIFO_internal_state) : FIFO_internal_state := tt.
+
+ #[global] Program Instance FIFO : Scheduler_t :=
+ mkScheduler FIFO_schedule _ _ tt UpdatSchState.
+
+ (* The one defined in Interface SubLayer *)
+ #[global] Existing Instance ARBITER_CFG.
+
+ #[global] Existing Instance ImplementationSubLayer.
+
+ Definition FIFO_arbitrate t :=
+ @mkTestTrace SYS_CFG REQUESTOR_CFG
+ ((Default_arbitrate t).(Arbiter_Commands))
+ ((Default_arbitrate t).(Arbiter_Time)).
+
+End FIFOimpSL.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL_sim.v b/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL_sim.v
new file mode 100644
index 0000000..9d489e9
--- /dev/null
+++ b/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL_sim.v
@@ -0,0 +1,102 @@
+Set Printing Projections.
+
+From mathcomp Require Import ssreflect eqtype ssrbool ssrnat fintype div ssrZ zify tuple.
+(* From Coq Require Import Program Equality. *)
+From Coq Require Import Program List.
+From DRAM Require Import FIFOimpSL.
+
+Section FIFOimpSL_sim.
+
+ Program Instance SYS_CFG : System_configuration := {
+ BANKGROUPS := 1;
+ BANKS := 2;
+ T_BURST := 2;
+ T_WL := 2;
+ T_RRD_s := 1;
+ T_RRD_l := 3;
+ T_FAW := 20;
+ T_RC := 3;
+ T_RP := 4;
+ T_RCD := 2;
+ T_RAS := 4;
+ T_RTP := 4;
+ T_WR := 1;
+ T_RTW := 10;
+ T_WTR_s := 1;
+ T_WTR_l := 10;
+ T_CCD_s := 1;
+ T_CCD_l := 12;
+ T_REFI := 100;
+ T_RFC := 6
+ }.
+
+ (* The one defined in TDMimpSL *)
+ Existing Instance REQUESTOR_CFG.
+
+ (* The one defined in TDMimpSL *)
+ Existing Instance SCH_ST.
+
+ (* The one defined in Interface SubLayer *)
+ Existing Instance ARBITER_CFG.
+
+ (* Defined in Interface SubLayer*)
+ Existing Instance ImplementationSubLayer.
+
+ Instance SCH_OPT : SchedulingOptions_t := mkSCH_OPT opage.
+
+ Program Definition Req1 := mkReq tt 1 RD
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 0) 5).
+
+ Program Definition Req2 := mkReq tt 2 RD
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 10).
+
+ Program Definition Req3 := mkReq tt 3 WR
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 0) 5).
+
+ Program Definition Req4 := mkReq tt 4 WR
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 15).
+
+ Definition Input := [:: Req1;Req2;Req3;Req4].
+
+ Program Instance AF : Arrival_function_t := Default_arrival_function_t Input.
+
+ (* The one defined in TDMimpSL *)
+ (* More like a round robin really ... *)
+ (* But it will keep waiting forever if the slot owner has no CAS *)
+ Instance FIFO_arbiter : TestArbiter_t := mkTestArbiter AF FIFO_arbitrate.
+
+ Definition inst := 30.
+
+ (* Still have a problem : Why ACT is only issued at cycle 7 ?! *)
+ Eval vm_compute in (Default_arbitrate inst).(Arbiter_Commands).
+
+ Eval vm_compute in
+ proj1_sig (match (Default_arbitrate inst).(Implementation_State) with
+ | Some st => st.(SystemState).(Banks)
+ | None => (exist _ (repeat InitBank BANKS) (repeat_size InitBank BANKS))
+ end).
+
+ Eval vm_compute in
+ (match (Default_arbitrate 4).(Implementation_State) with
+ | Some st => st.(CMap)
+ | None => [::]
+ end).
+
+ Definition get_sys_cnts :=
+ match (Default_arbitrate inst).(Implementation_State) with
+ | Some st => st.(SystemState).(SysCounters)
+ | None => (mkGlobalCounters
+ (exist _ (repeat init_val 3) (repeat_size 0 3))
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0)
+ end.
+
+ Eval vm_compute in proj1_sig get_sys_cnts.(cACTdb).
+ Eval vm_compute in proj1_sig get_sys_cnts.(cACTbgs).
+ Eval vm_compute in get_sys_cnts.(cRDdb).
+
+End TDMimpSL_sim.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL.v b/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL.v
new file mode 100644
index 0000000..ad59330
--- /dev/null
+++ b/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL.v
@@ -0,0 +1,100 @@
+Set Printing Projections.
+Set Warnings "-notation-overridden,-parsing".
+
+From mathcomp Require Import ssreflect eqtype ssrbool ssrnat fintype div ssrZ zify tuple.
+From Coq Require Import Program Equality.
+From DRAM Require Export InterfaceSubLayer.
+
+Section RRimpSL.
+
+ Context {SYS_CFG : System_configuration}.
+
+ Class RR_configuration := mkRRCFG {
+ SN : nat;
+ SN_gt_1 : SN > 1;
+ }.
+
+ Context {RR_CFG : RR_configuration}.
+
+ Definition Slot_t := ordinal_eqType SN.
+
+ #[global] Instance REQUESTOR_CFG : Requestor_configuration :=
+ {
+ Requestor_t := Slot_t
+ }.
+
+ Context {SCH_OPT : SchedulingOptions_t}.
+ Context {AF : Arrival_function_t}.
+
+ #[global] Instance SCH_ST : SchedulerInternalState := mkSIS Slot_t.
+
+ Definition filter_cmd slot := fun cmd =>
+ match cmd with
+ | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => r.(Requestor) == slot
+ | _ => false
+ end.
+
+ Definition RR_schedule
+ (map : ReqCmdMap_t)
+ (SS : SystemState_t)
+ (slot : Slot_t) : Command_kind_t :=
+ let cmd := seq.ohead (filter (filter_cmd slot) map) in
+ match cmd with
+ | Some cmd => cmd
+ | None => NOP
+ end.
+
+ Lemma SN_pos : SN > 0.
+ Proof. specialize SN_gt_1; lia. Qed.
+
+ Definition OZSlot := Ordinal SN_pos.
+ Definition O1Slot := Ordinal SN_gt_1.
+
+ (* Wrap around counter *)
+ Definition Next_slot (c : Slot_t) :=
+ let nextc := c.+1 < SN in
+ (if nextc as X return (nextc = X -> Slot_t) then
+ fun (P : nextc = true) => Ordinal (P : nextc)
+ else
+ fun _ => OZSlot) Logic.eq_refl.
+
+ (* version with auto-precharge should be OK because of assumption that adjacent slots
+ target different banks *)
+
+ (* Can't update when the CAS is seen on the structure, but rather issued to the device *)
+ (* Maybe look at counters to detect a CWR or RD ?! *)
+ (* Give up slot if no pending request *)
+ Definition UpdatSchState cmd cmd_map (SS : SystemState_t) (slot : Slot_t) : Slot_t :=
+ let cond1 := (* no commands belonging to the current slot owner *)
+ ((find (fun cmd =>
+ match cmd with
+ | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => r.(Requestor) == slot
+ | _ => false
+ end) cmd_map) == seq.size cmd_map) in
+ let cond2 := (* scheduled command is a CAS *)
+ (match cmd with
+ | CRD _ | CRDA _ | CWR _ | CWRA _ => true
+ | _ => false
+ end) in
+ if (cond1 || cond2) then Next_slot slot else slot.
+
+ #[global] Program Instance RR : Scheduler_t :=
+ mkScheduler RR_schedule _ _ OZSlot UpdatSchState.
+ Next Obligation.
+ unfold RR_schedule.
+ destruct hd; simpl;
+ try (destruct (eq_op r.(Requestor) SCH_ST0) eqn:H_req; rewrite H_req //=);
+ try (by left); by right.
+ Qed.
+
+ (* The one defined in Interface SubLayer *)
+ #[global] Existing Instance ARBITER_CFG.
+
+ #[global] Existing Instance ImplementationSubLayer.
+
+ Definition RR_arbitrate t :=
+ @mkTestTrace SYS_CFG REQUESTOR_CFG
+ ((Default_arbitrate t).(Arbiter_Commands))
+ ((Default_arbitrate t).(Arbiter_Time)).
+
+End RRimpSL.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL_sim.v b/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL_sim.v
new file mode 100644
index 0000000..3bdfcb8
--- /dev/null
+++ b/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL_sim.v
@@ -0,0 +1,111 @@
+Set Printing Projections.
+
+From mathcomp Require Import ssreflect eqtype ssrbool ssrnat fintype div ssrZ zify tuple.
+(* From Coq Require Import Program Equality. *)
+From Coq Require Import Program List.
+From DRAM Require Import RRimpSL.
+
+Section RRimpSL_sim.
+
+ Program Instance SYS_CFG : System_configuration := {
+ BANKGROUPS := 1;
+ BANKS := 2;
+ T_BURST := 2;
+ T_WL := 2;
+ T_RRD_s := 1;
+ T_RRD_l := 3;
+ T_FAW := 20;
+ T_RC := 3;
+ T_RP := 4;
+ T_RCD := 2;
+ T_RAS := 4;
+ T_RTP := 4;
+ T_WR := 1;
+ T_RTW := 10;
+ T_WTR_s := 1;
+ T_WTR_l := 10;
+ T_CCD_s := 1;
+ T_CCD_l := 12;
+ T_REFI := 100;
+ T_RFC := 6
+ }.
+
+ (* The one defined in RRimpSL *)
+ Existing Instance REQUESTOR_CFG.
+
+ (* The one defined in RRimpSL *)
+ Existing Instance SCH_ST.
+
+ (* The one defined in Interface SubLayer *)
+ Existing Instance ARBITER_CFG.
+
+ (* Defined in Interface SubLayer*)
+ Existing Instance ImplementationSubLayer.
+
+ Instance SCH_OPT : SchedulingOptions_t := mkSCH_OPT opage.
+
+ (* There has to be at least two requestors *)
+ Program Instance RR_CFG : RR_configuration := mkRRCFG 2 _.
+
+ Program Definition Req1 := mkReq (Ordinal (_ : 0 < SN)) 1 RD
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 0) 5).
+
+ Program Definition Req2 := mkReq (Ordinal (_ : 1 < SN)) 1 RD
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 10).
+
+ Definition Input := [:: Req1;Req2].
+
+ Program Instance AF : Arrival_function_t := Default_arrival_function_t Input.
+
+ (* The one defined in RRimpSL *)
+ (* More like a round robin really ... *)
+ (* But it will keep waiting forever if the slot owner has no CAS *)
+ Instance RRarbiter : TestArbiter_t := mkTestArbiter AF RR_arbitrate.
+
+ Definition inst := 5.
+
+ (* At 9 see the CRD from Req1 -> Change slot owner to 1 *)
+ (* At 11 see the CRD from Req2 -> Change slot owner to 0 *)
+ (* At 13 see the CRD from Req1 -> Change slot owner to 1 *)
+ (* A (C)| A (C)| | C *)
+ (* 1 2 3 4 5 6 7 8 | 9 10 11 |12| 13 14 15 16 17 18 19 20*)
+ (* 0 0 0 0 0 0 0 0 | 1 1 1 | 0| 1 0 0 0 0 0 0 0*)
+ Eval vm_compute in map (fun x =>
+ nat_of_ord (match (Default_arbitrate x).(Implementation_State) with
+ | Some st => st.(SchState)
+ | None => Ordinal (_ : 0 < SN)
+ end)) (seq.iota 1 30).
+
+ (* Still have a problem : Why ACT is only issued at cycle 7 ?! *)
+ Eval vm_compute in (Default_arbitrate inst).(Arbiter_Commands).
+
+ Eval vm_compute in
+ proj1_sig (match (Default_arbitrate inst).(Implementation_State) with
+ | Some st => st.(SystemState).(Banks)
+ | None => (exist _ (repeat InitBank BANKS) (repeat_size InitBank BANKS))
+ end).
+
+ Eval vm_compute in
+ (match (Default_arbitrate 4).(Implementation_State) with
+ | Some st => st.(CMap)
+ | None => [::]
+ end).
+
+ Definition get_sys_cnts :=
+ match (Default_arbitrate inst).(Implementation_State) with
+ | Some st => st.(SystemState).(SysCounters)
+ | None => (mkGlobalCounters
+ (exist _ (repeat init_val 3) (repeat_size 0 3))
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0)
+ end.
+
+ Eval vm_compute in proj1_sig get_sys_cnts.(cACTdb).
+ Eval vm_compute in proj1_sig get_sys_cnts.(cACTbgs).
+ Eval vm_compute in get_sys_cnts.(cRDdb).
+
+End RRimpSL_sim.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL.v b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL.v
new file mode 100644
index 0000000..a0d9bd0
--- /dev/null
+++ b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL.v
@@ -0,0 +1,101 @@
+Set Printing Projections.
+Set Warnings "-notation-overridden,-parsing".
+
+From mathcomp Require Import ssreflect eqtype ssrbool ssrnat fintype div ssrZ zify tuple.
+From Coq Require Import Program Equality.
+From DRAM Require Export InterfaceSubLayer.
+
+Section TDMimpSL.
+
+ Context {SYS_CFG : System_configuration}.
+
+ Class TDM_configuration := mkTDMCFG {
+ SN : nat;
+ SN_gt_1 : SN > 1;
+
+ SL : nat;
+ SL_pos : SL > 0
+ }.
+
+ Context {TDM_CFG : TDM_configuration}.
+
+ Definition Slot_t := ordinal_eqType SN.
+
+ #[global] Instance REQUESTOR_CFG : Requestor_configuration :=
+ {
+ Requestor_t := Slot_t
+ }.
+
+ Context {SCH_OPT : SchedulingOptions_t}.
+ Context {AF : Arrival_function_t}.
+
+ Definition TDM_counter_t := ordinal_eqType SL.
+
+ Definition TDM_internal_state : Type := (Slot_t * TDM_counter_t)%type.
+
+ #[global] Instance SCH_ST : SchedulerInternalState := mkSIS TDM_internal_state.
+
+ Definition filter_cmd (slot : Slot_t) := filter (fun cmd =>
+ match cmd with
+ | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => r.(Requestor) == slot
+ | _ => false
+ end).
+
+ Definition TDM_schedule
+ (map : ReqCmdMap_t)
+ (SS : SystemState_t)
+ (TDM_st : TDM_internal_state) : Command_kind_t :=
+ let slot := fst TDM_st in
+ let cmd := seq.ohead (filter_cmd slot map) in
+ match cmd with
+ | Some cmd => cmd
+ | None => NOP
+ end.
+
+ Lemma SN_pos : SN > 0.
+ Proof. specialize SN_gt_1; lia. Qed.
+
+ Definition OZSlot := Ordinal SN_pos.
+ Definition O1Slot := Ordinal SN_gt_1.
+ Definition OZCycle := Ordinal SL_pos.
+
+ (* Increment counter for cycle offset (with wrap-arround). *)
+ Definition Next_cycle (c : TDM_counter_t) : TDM_counter_t :=
+ let nextc := c.+1 < SL in
+ (if nextc as X return (nextc = X -> TDM_counter_t) then
+ fun (P : nextc = true) => Ordinal (P : nextc)
+ else
+ fun _ => OZCycle) Logic.eq_refl.
+
+ Definition Next_slot (s : Slot_t) (c : TDM_counter_t) : Slot_t :=
+ if (c.+1 < SL) then s else
+ let nexts := s.+1 < SN in
+ (if nexts as X return (nexts = X -> Slot_t) then
+ fun (P : nexts = true) => Ordinal (P : nexts)
+ else fun _ => OZSlot) Logic.eq_refl.
+
+ Definition UpdatSchState (cmd : Command_kind_t) (cmd_map : ReqCmdMap_t) (SS : SystemState_t)
+ (TDM_st : TDM_internal_state) : TDM_internal_state :=
+ let '(s,c) := TDM_st in
+ ((Next_slot s c),(Next_cycle c)).
+
+ #[global] Program Instance TDM : Scheduler_t :=
+ mkScheduler TDM_schedule _ _ (OZSlot,OZCycle) UpdatSchState.
+ Next Obligation.
+ unfold TDM_schedule.
+ destruct hd; simpl;
+ try (destruct (eq_op r.(Requestor) (fst SCH_ST0)) eqn:H_req; rewrite H_req //=);
+ try (by left); by right.
+ Qed.
+
+ (* The one defined in Interface SubLayer *)
+ #[global] Existing Instance ARBITER_CFG.
+
+ #[global] Existing Instance ImplementationSubLayer.
+
+ Definition TDM_arbitrate t :=
+ @mkTestTrace SYS_CFG REQUESTOR_CFG
+ ((Default_arbitrate t).(Arbiter_Commands))
+ ((Default_arbitrate t).(Arbiter_Time)).
+
+End TDMimpSL.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_sim.v b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_sim.v
new file mode 100644
index 0000000..dbc0ebb
--- /dev/null
+++ b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_sim.v
@@ -0,0 +1,111 @@
+Set Printing Projections.
+
+From mathcomp Require Import ssreflect eqtype ssrbool ssrnat fintype div ssrZ zify tuple.
+From Coq Require Import Program List.
+From DRAM Require Import TDMimpSL.
+
+Section TDMimpSL_sim.
+
+ Program Instance SYS_CFG : System_configuration := {
+ BANKGROUPS := 1;
+ BANKS := 2;
+ T_BURST := 2;
+ T_WL := 2;
+ T_RRD_s := 1;
+ T_RRD_l := 3;
+ T_FAW := 20;
+ T_RC := 3;
+ T_RP := 4;
+ T_RCD := 2;
+ T_RAS := 4;
+ T_RTP := 4;
+ T_WR := 1;
+ T_RTW := 10;
+ T_WTR_s := 1;
+ T_WTR_l := 10;
+ T_CCD_s := 1;
+ T_CCD_l := 12;
+ T_REFI := 100;
+ T_RFC := 6
+ }.
+
+ (* The one defined in TDMimpSL *)
+ Existing Instance REQUESTOR_CFG.
+
+ (* The one defined in TDMimpSL *)
+ Existing Instance SCH_ST.
+
+ (* The one defined in Interface SubLayer *)
+ Existing Instance ARBITER_CFG.
+
+ (* Defined in Interface SubLayer*)
+ Existing Instance ImplementationSubLayer.
+
+ Instance SCH_OPT : SchedulingOptions_t := mkSCH_OPT opage.
+
+ (* There has to be at least two requestors *)
+ Program Instance TDM_CFG : TDM_configuration := mkTDMCFG 2 _ 15 _.
+
+ Program Definition Req1 := mkReq (Ordinal (_ : 0 < SN)) 1 RD
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 0) 5).
+
+ Program Definition Req2 := mkReq (Ordinal (_ : 1 < SN)) 1 RD
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 10).
+
+ Definition Input := [:: Req1;Req2].
+
+ Program Instance AF : Arrival_function_t := Default_arrival_function_t Input.
+
+ (* The one defined in TDMimpSL *)
+ (* More like a round robin really ... *)
+ (* But it will keep waiting forever if the slot owner has no CAS *)
+ Instance TDM_arbiter : TestArbiter_t := mkTestArbiter AF TDM_arbitrate.
+
+ Definition inst := 30.
+
+ (* At 9 see the CRD from Req1 -> Change slot owner to 1 *)
+ (* At 11 see the CRD from Req2 -> Change slot owner to 0 *)
+ (* At 13 see the CRD from Req1 -> Change slot owner to 1 *)
+ (* A (C)| A (C)| | C *)
+ (* 1 2 3 4 5 6 7 8 | 9 10 11 |12| 13 14 15 16 17 18 19 20*)
+ (* 0 0 0 0 0 0 0 0 | 1 1 1 | 0| 1 0 0 0 0 0 0 0*)
+ Eval vm_compute in
+ map (fun '(a,b) => (nat_of_ord a, nat_of_ord b))
+ (map (fun x => (match (Default_arbitrate x).(Implementation_State) with
+ | Some st => (fst st.(SchState),snd st.(SchState))
+ | None => (Ordinal (_ : 0 < SN),Ordinal (_ : 0 < SL))
+ end)) (seq.iota 1 30)).
+
+ (* Still have a problem : Why ACT is only issued at cycle 7 ?! *)
+ Eval vm_compute in (Default_arbitrate inst).(Arbiter_Commands).
+
+ Eval vm_compute in
+ proj1_sig (match (Default_arbitrate inst).(Implementation_State) with
+ | Some st => st.(SystemState).(Banks)
+ | None => (exist _ (repeat InitBank BANKS) (repeat_size InitBank BANKS))
+ end).
+
+ Eval vm_compute in
+ (match (Default_arbitrate 4).(Implementation_State) with
+ | Some st => st.(CMap)
+ | None => [::]
+ end).
+
+ Definition get_sys_cnts :=
+ match (Default_arbitrate inst).(Implementation_State) with
+ | Some st => st.(SystemState).(SysCounters)
+ | None => (mkGlobalCounters
+ (exist _ (repeat init_val 3) (repeat_size 0 3))
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0
+ (exist _ (repeat init_val BANKGROUPS) (repeat_size init_val BANKGROUPS))
+ 0)
+ end.
+
+ Eval vm_compute in proj1_sig get_sys_cnts.(cACTdb).
+ Eval vm_compute in proj1_sig get_sys_cnts.(cACTbgs).
+ Eval vm_compute in get_sys_cnts.(cRDdb).
+
+End TDMimpSL_sim.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/FIFOimpSL/FIFOimpSL.v b/framework/DRAM/Implementations/FIFOimpSL/FIFOimpSL.v
deleted file mode 100644
index 9291f92..0000000
--- a/framework/DRAM/Implementations/FIFOimpSL/FIFOimpSL.v
+++ /dev/null
@@ -1,66 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-
-From mathcomp Require Import ssreflect ssrnat ssrbool eqtype seq zify.
-From DRAM Require Export InterfaceSubLayer.
-
-Module FIFOimpSL (SYS : SystemModule) (REQ : Requestor_configuration).
-
- Module Import MIntSubLayer := InterfaceSubLayer SYS REQ.
-
- (* Interface sub layer defines an implementation interface module *)
- Import MImpInterface.
- (* Implementation interface defines an arbiter module *)
- Import MArbiter.
- (* Arbiter modules defines a trace module *)
- Import MTrace.
- (* Trace modules defines a bank machine module *)
- Import MBankMachine.
- (* Bank machine module defines a commands module *)
- Import MCommands.
- (* Commands module defines a requests module *)
- Import MRequests.
- (* Requests module defines an address module *)
- Import MAddress.
- (* Use qualified names for SYS *)
- Import SYS.
-
- Section Sec_FIFOiARBITER_CFGmpSL.
-
- (* An abstract instance of the schedulign option, defined in Bank_Machine_t *)
- Context {SCH_OPT : Scheduling_Options}.
- (* An abstract instance of the arrival function, defined in Arbiter_t *)
- Context {AF : Arrival_function_t}.
-
- (* -------------------------------------------------------------- *)
- (* These ones don't need concrete instances *)
- (* -------------------------------------------------------------- *)
-
- (* An instance of Arbiter_configuration, defined in InterfaceSubLayer *)
- Existing Instance ARBITER_CFG.
-
- (* An instance of Implementation_t, defined in InterfaceSubLayer *)
- Existing Instance ImplementationSubLayer.
-
- Definition FIFO_sch (M : seq (option Request_t * Command_kind_t)) :=
- head (None, NOP) M.
-
- #[global] Instance FIFO_Scheduler : Scheduler.
- refine (mkScheduler FIFO_sch _).
- unfold FIFO_sch; intros.
- induction s;
- [ simpl; right; apply /eqP; reflexivity | ].
- destruct IHs as [IHIn | IHhd];
- simpl; left; left; reflexivity.
- Defined.
-
- Definition FIFO_arbitrate t :=
- @mkTestTrace
- ((Default_arbitrate t).(Arbiter_Commands))
- ((Default_arbitrate t).(Arbiter_Time)).
-
- End Sec_FIFOiARBITER_CFGmpSL.
-
-End FIFOimpSL.
-
-
diff --git a/framework/DRAM/Implementations/FIFOimpSL/FIFOimpSL_test.v b/framework/DRAM/Implementations/FIFOimpSL/FIFOimpSL_test.v
deleted file mode 100644
index c57f486..0000000
--- a/framework/DRAM/Implementations/FIFOimpSL/FIFOimpSL_test.v
+++ /dev/null
@@ -1,119 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-
-From DRAM Require Import FIFOimpSL.
-From Coq Require Import Vector.
-From RecordUpdate Require Import RecordSet.
-
-Import RecordSetNotations.
-Import VectorNotations.
-
-Module SYS_CFG <: SystemModule.
-
- Definition BANKGROUPS := 1.
- Definition BANKS := 2.
-
- Lemma BANKGROUPS_pos : BANKGROUPS != 0. auto. Qed.
- Lemma BANKS_pos : BANKS != 0. auto. Qed.
-
- Definition T_BURST := 4.
- Definition T_WL := 2.
-
- Definition T_RRD_s := 2.
- Definition T_RRD_l := 4.
-
- Definition T_FAW := 5.
-
- Definition T_RC := 3.
- Definition T_RP := 3.
- Definition T_RCD := 3.
- Definition T_RAS := 3.
- Definition T_RTP := 3.
- Definition T_WR := 3.
-
- Definition T_RTW := 5.
- Definition T_WTR_s := 2.
- Definition T_WTR_l := 4.
- Definition T_CCD_s := 2.
- Definition T_CCD_l := 4.
-
- Definition T_REFI := 500.
- Definition T_RFC := 10.
-
- Lemma T_REFI_pos : T_REFI > 0. auto. Qed.
- Lemma T_REFI_GT_T_RFC : T_REFI > T_RFC. auto. Qed.
-
- Lemma T_RRD_s_pos : T_RRD_s != 0. auto. Qed.
- Lemma T_RRD_l_pos : T_RRD_l != 0. auto. Qed.
- Lemma T_FAW_pos : T_FAW != 0. auto. Qed.
- Lemma T_RC_pos : T_RC != 0. auto. Qed.
- Lemma T_RP_pos : T_RP != 0. auto. Qed.
- Lemma T_RCD_pos : T_RCD != 0. auto. Qed.
- Lemma T_RAS_pos : T_RAS != 0. auto. Qed.
- Lemma T_RTP_pos : T_RTP != 0. auto. Qed.
- Lemma T_WR_pos : T_WR != 0. auto. Qed.
- Lemma T_RTW_pos : T_RTW != 0. auto. Qed.
- Lemma T_WTR_s_pos : T_WTR_s != 0. auto. Qed.
- Lemma T_WTR_l_pos : T_WTR_l != 0. auto. Qed.
- Lemma T_CCD_s_pos : T_CCD_s != 0. auto. Qed.
- Lemma T_CCD_l_pos : T_CCD_l != 0. auto. Qed.
- Lemma T_RFC_pos : T_RFC > 0. auto. Qed.
-
- Lemma T_RRD_bgs : T_RRD_s < T_RRD_l. auto. Qed.
- Lemma T_WTR_bgs : T_WTR_s < T_WTR_l. auto. Qed.
- Lemma T_CCD_bgs : T_CCD_s < T_CCD_l. auto. Qed.
-
-End SYS_CFG.
-
-Module REQ_CFG <: Requestor_configuration.
- Definition Requestor_t := unit_eqType.
-End REQ_CFG.
-
-Module Import FIFO_test_instance := FIFOimpSL SYS_CFG REQ_CFG.
-
-Import MIntSubLayer.
-(* Interface sub layer defines an implementation interface module *)
-Import MImpInterface.
-(* Implementation interface defines an arbiter module *)
-Import MArbiter.
-(* Arbiter modules defines a trace module *)
-Import MTrace.
-(* Trace modules defines a bank machine module *)
-Import MBankMachine.
-(* Bank machine module defines a commands module *)
-Import MCommands.
-(* Commands module defines a requests module *)
-Import MRequests.
-(* Requests module defines an address module *)
-Import MAddress.
-
-#[global] Instance SCH_OPT : Scheduling_Options := mkSCH_OPT opage.
-
-Definition Req1 := mkReq tt 1 RD
- (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 0) 5).
-
-Definition Req2 := mkReq tt 2 RD
- (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 10).
-
- (*
- Definition Req2 := mkReq tt 2 WR (Nat_to_bankgroup 0) (Nat_to_bank 1) 0.
- Definition Req3 := mkReq tt 4 WR (Nat_to_bankgroup 0) (Nat_to_bank 0) 2.
- Definition Req4 := mkReq tt 8 RD (Nat_to_bankgroup 0) (Nat_to_bank 2) 10.
- Definition Input := [::Req1;Req2;Req3;Req4].
- *)
-
-Definition Input := [::Req1].
-
-#[global] Program Instance AF : Arrival_function_t := Default_arrival_function_t Input.
-
-#[global] Instance FIFOArbiter : TestArbiter_t := mkTestArbiter AF FIFO_arbitrate.
-
-(* things go wrong after the RD ? *)
-Definition inst := 11.
-
-(* maybe commands do not need to take parameters *)
-Eval vm_compute in (Default_arbitrate inst).(Arbiter_Commands).
-Eval vm_compute in (Default_arbitrate inst).(Implementation_State).(SystemState).
-Eval vm_compute in (Default_arbitrate inst).(Implementation_State).(CMap).(ReqCmdMap.this).
-
-(* Maybe try to run this in Ocaml instead of Coq to ignore proofs ? *)
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/DynTDM/TDMds.v b/framework/DRAM/Implementations/TS/DynTDM/TDMds.v
similarity index 100%
rename from framework/DRAM/Implementations/DynTDM/TDMds.v
rename to framework/DRAM/Implementations/TS/DynTDM/TDMds.v
diff --git a/framework/DRAM/Implementations/DynTDM/TDMes.v b/framework/DRAM/Implementations/TS/DynTDM/TDMes.v
similarity index 100%
rename from framework/DRAM/Implementations/DynTDM/TDMes.v
rename to framework/DRAM/Implementations/TS/DynTDM/TDMes.v
diff --git a/framework/DRAM/Implementations/DynTDM/TDMesREF.v b/framework/DRAM/Implementations/TS/DynTDM/TDMesREF.v
similarity index 100%
rename from framework/DRAM/Implementations/DynTDM/TDMesREF.v
rename to framework/DRAM/Implementations/TS/DynTDM/TDMesREF.v
diff --git a/framework/DRAM/Implementations/DynTDM/TDMesREFpg.v b/framework/DRAM/Implementations/TS/DynTDM/TDMesREFpg.v
similarity index 100%
rename from framework/DRAM/Implementations/DynTDM/TDMesREFpg.v
rename to framework/DRAM/Implementations/TS/DynTDM/TDMesREFpg.v
diff --git a/framework/DRAM/Implementations/FIFO/FIFO.v b/framework/DRAM/Implementations/TS/FIFO/FIFO.v
similarity index 81%
rename from framework/DRAM/Implementations/FIFO/FIFO.v
rename to framework/DRAM/Implementations/TS/FIFO/FIFO.v
index b4487e2..5af2442 100644
--- a/framework/DRAM/Implementations/FIFO/FIFO.v
+++ b/framework/DRAM/Implementations/TS/FIFO/FIFO.v
@@ -4,23 +4,13 @@ Set Printing Projections.
From mathcomp Require Import ssreflect ssrnat ssrbool eqtype seq zify fintype.
From DRAM Require Export ImplementationInterface Arbiter.
-Module REQ_CFG <: Requestor_configuration.
- Definition Requestor_t := unit_eqType.
-End REQ_CFG.
+Section FIFO.
-Module FIFO (SYS : SystemModule).
+ Context {SYS_CFG : System_configuration}.
- Module Import MImpInterface := ImplementationInterface SYS REQ_CFG.
-
- Import MArbiter.
- Import MTrace.
- Import MBankMachine.
- Import MCommands.
- Import MRequests.
- Import MAddress.
- Import SYS.
-
- Section FIFOSec.
+ Instance REQUESTOR_CFG : Requestor_configuration := {
+ Requestor_t := unit_eqType
+ }.
(* #[local] Axiom DDR3 : BANKGROUPS = 1. *)
@@ -59,11 +49,14 @@ Module FIFO (SYS : SystemModule).
Context {FIFO_CFG : FIFO_configuration}.
Context {AF : Arrival_function_t}.
+ (* ------------------------------------------------------------------------- *)
+ (* Helper Lemmas *)
+
Lemma FIFO_WAIT_GT_SCAS :
CAS_date.+1 < WAIT.
Proof.
apply ltn_trans with (n := CAS_date + T_RTP); [ | exact WAIT_END_READ ].
- rewrite -ltn_predRL nat_add_pred nat_ltn_add; done || (rewrite ltn_predRL; exact T_RTP_GT_ONE).
+ rewrite -ltn_predRL; specialize T_RTP_GT_ONE; lia.
Qed.
Lemma FIFO_WAIT_GT_SACT :
@@ -74,11 +67,9 @@ Module FIFO (SYS : SystemModule).
unfold CAS_date, ACT_date.
rewrite prednK.
2: specialize T_RP_GT_ONE as H; apply ltn_trans with (n := 1); done || exact H.
- rewrite addnC -nat_add_pred addnC nat_add_pred.
- apply nat_ltn_add.
- rewrite ltn_predRL; exact T_RCD_GT_ONE.
- Qed.
-
+ specialize T_RCD_GT_ONE; lia.
+ Qed.
+
Lemma CAS_neq_ACT:
(CAS_date == ACT_date) = false.
Proof.
@@ -88,6 +79,8 @@ Module FIFO (SYS : SystemModule).
specialize T_RCD_pos as H. rewrite -lt0n in H; by rewrite H.
Qed.
+ (* ------------------------------------------------------------------------------- *)
+
Definition Counter_t := ordinal WAIT.
Variant FIFO_state_t :=
@@ -111,35 +104,29 @@ Module FIFO (SYS : SystemModule).
else
fun _ => OCycle0) Logic.eq_refl.
- Definition Enqueue (R P : Requests_t) :=
- P ++ R.
-
- Definition Dequeue r (P : Requests_t) :=
- rem r P.
-
Definition Init_state R :=
- IDLE OCycle0 (Enqueue R [::]).
+ IDLE OCycle0 R.
- Definition Next_state R (AS : FIFO_state_t) : (FIFO_state_t * (option Request_t * Command_kind_t)) :=
+ Definition Next_state R (AS : FIFO_state_t) : (FIFO_state_t * Command_kind_t) :=
match AS with
| IDLE c P =>
let c' := Next_cycle c in
let P' := Enqueue R P in
match P with
- | [::] => (IDLE c' P', (None,NOP))
- | r :: PP => (RUNNING OCycle0 (Enqueue R (Dequeue r P)) r, (Some r,PRE r))
+ | [::] => (IDLE c' P',NOP)
+ | r :: PP => (RUNNING OCycle0 (Enqueue R (Dequeue r P)) r,PRE r)
end
| RUNNING c P r =>
let P' := Enqueue R P in
let c' := Next_cycle c in
- if nat_of_ord c == OACT_date then (RUNNING c' P' r, (Some r, ACT r))
- else if nat_of_ord c == OCAS_date then (RUNNING c' P' r, (Some r, (Kind_of_req r) r))
+ if nat_of_ord c == OACT_date then (RUNNING c' P' r,ACT r)
+ else if nat_of_ord c == OCAS_date then (RUNNING c' P' r,(Kind_of_req r) r)
else if nat_of_ord c == WAIT.-1 then
match P with
- | [::] => (IDLE OCycle0 P', (None, NOP))
- | r :: PP => (RUNNING OCycle0 (Enqueue R (Dequeue r P)) r, (Some r,PRE r))
+ | [::] => (IDLE OCycle0 P', NOP)
+ | r :: PP => (RUNNING OCycle0 (Enqueue R (Dequeue r P)) r,PRE r)
end
- else (RUNNING c' P' r, (None,NOP))
+ else (RUNNING c' P' r,NOP)
end.
#[export] Instance FIFO_implementation : Implementation_t :=
@@ -191,6 +178,4 @@ Module FIFO (SYS : SystemModule).
| RUNNING _ _ r => Some r
end.
- End FIFOSec.
-
End FIFO.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/FIFO/FIFO_extraction.v b/framework/DRAM/Implementations/TS/FIFO/FIFO_extraction.v
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/FIFO_extraction.v
rename to framework/DRAM/Implementations/TS/FIFO/FIFO_extraction.v
diff --git a/framework/DRAM/Implementations/FIFO/FIFO_proofs.v b/framework/DRAM/Implementations/TS/FIFO/FIFO_proofs.v
similarity index 51%
rename from framework/DRAM/Implementations/FIFO/FIFO_proofs.v
rename to framework/DRAM/Implementations/TS/FIFO/FIFO_proofs.v
index f0fc695..6b97ee8 100644
--- a/framework/DRAM/Implementations/FIFO/FIFO_proofs.v
+++ b/framework/DRAM/Implementations/TS/FIFO/FIFO_proofs.v
@@ -2,25 +2,16 @@ Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From mathcomp Require Import ssreflect ssrnat ssrbool eqtype seq zify fintype ssrZ zify.
-From DRAM Require Export FIFO.
+From DRAM Require Export Util FIFO.
From Coq Require Import Program.
-Module FIFOPROOFS (SYS : SystemModule).
-
- Module Import MFIFO := FIFO SYS.
-
- Import MImpInterface.
- Import MArbiter.
- Import MTrace.
- Import MBankMachine.
- Import MCommands.
- Import MRequests.
- Import MAddress.
- Import SYS.
-
- Section Proofs.
+Section Proofs.
+ Context {SYS_CFG : System_configuration}.
Context {FIFO_CFG : FIFO_configuration}.
+
+ Existing Instance REQUESTOR_CFG.
+
Context {AF : Arrival_function_t}.
Existing Instance ARBITER_CFG.
@@ -45,7 +36,19 @@ Module FIFOPROOFS (SYS : SystemModule).
(* --------------------- COUNTER PROOFS ----------------------------- *)
(* ------------------------------------------------------------------ *)
- Lemma FIFO_next_cycle_inc (c : MFIFO.Counter_t) : c < FIFO_CFG.(WAIT).-1 ->
+ Lemma FIFO_wait_neq_act :
+ (WAIT.-1 == OACT_date) = false.
+ Proof.
+ unfold OACT_date; simpl; specialize FIFO_WAIT_GT_SACT; lia.
+ Qed.
+
+ Lemma FIFO_wait_neq_cas :
+ (WAIT.-1 == OCAS_date) = false.
+ Proof.
+ unfold OCAS_date; simpl; specialize FIFO_WAIT_GT_SCAS; lia.
+ Qed.
+
+ Lemma FIFO_next_cycle_inc (c : Counter_t) : c < FIFO_CFG.(WAIT).-1 ->
nat_of_ord (Next_cycle c) = c.+1.
Proof.
intro; unfold Next_cycle; set (HH := c.+1 < WAIT); dependent destruction HH;
@@ -76,6 +79,7 @@ Module FIFOPROOFS (SYS : SystemModule).
try (discriminate Hrun); clear Hrun; simpl;
unfold FIFO_counter in Hc; subst;
try (move: Hend => /eqP Hend; lia);
+ rewrite -Hc; rewrite -Hc in H;
apply FIFO_next_cycle_inc; assumption.
Qed.
@@ -122,7 +126,7 @@ Module FIFOPROOFS (SYS : SystemModule).
Proof.
induction t; [ done | ]; simpl.
unfold Next_state.
- destruct_state t0; rewrite in_cons; intros Hi Hp; move: Hi => /orP [/eqP Hi | Hi];
+ destruct_state t; rewrite in_cons; intros Hi Hp; move: Hi => /orP [/eqP Hi | Hi];
try (by rewrite Hi in Hp);
try (by apply IHt in Hi);
try (unfold Kind_of_req in Hi; destruct r0.(Kind); by rewrite Hi in Hp);
@@ -139,7 +143,7 @@ Module FIFOPROOFS (SYS : SystemModule).
Proof.
induction t; [ done | ]; simpl.
unfold Next_state.
- destruct_state t0; rewrite in_cons; intros Hi Hp; move: Hi => /orP [/eqP Hi | Hi];
+ destruct_state t; rewrite in_cons; intros Hi Hp; move: Hi => /orP [/eqP Hi | Hi];
try (by rewrite Hi in Hp);
try (by apply IHt in Hi);
try (unfold Kind_of_req in Hi; destruct r0.(Kind); by rewrite Hi in Hp);
@@ -148,6 +152,21 @@ Module FIFOPROOFS (SYS : SystemModule).
split; trivial.
Qed.
+ Lemma FIFO_PRE_date t cmd:
+ cmd \in (# t).(Arbiter_Commands) -> isPRE cmd ->
+ (FIFO_counter # (cmd.(CDate)).(Implementation_State) = OCycle0) /\
+ (isRUNNING # (cmd.(CDate)).(Implementation_State)) /\
+ (FIFO_request # (cmd.(CDate)).(Implementation_State) == get_req cmd).
+ Proof.
+ induction t; [ done | ]; simpl.
+ unfold Next_state; destruct_state t; rewrite in_cons; intros Hi Hp; move: Hi => /orP [/eqP Hi | Hi];
+ try (by rewrite Hi in Hp);
+ try (by apply IHt in Hi);
+ try (unfold Kind_of_req in Hi; destruct r0.(Kind); by rewrite Hi in Hp);
+ rewrite Hi //= /Next_state Hs //= Hact Hcas //=.
+ move: Hend => /eqP Hend; rewrite !Hend eq_refl //=.
+ Qed.
+
Lemma FIFO_eq_counter t t' d:
isRUNNING (# t).(Implementation_State) -> t < t' ->
FIFO_counter (# t).(Implementation_State) = FIFO_counter (# t').(Implementation_State) ->
@@ -177,20 +196,162 @@ Module FIFOPROOFS (SYS : SystemModule).
specialize (@ltn_ord WAIT c0); lia.
Qed.
- Lemma FIFO_counter_bounded_ : forall (c : MFIFO.Counter_t),
+ Lemma FIFO_counter_bounded_ : forall (c : Counter_t),
c <= WAIT.-1.
Proof.
intro c; destruct c eqn:H; simpl; lia.
Qed.
-
- (*
- Ltac leqWAIT Hc Hrun :=
- rewrite Hc subnKC;
- ((apply FIFO_counter_bounded in Hrun; by rewrite Hc in Hrun) ||
- (rewrite - ltnS prednK; (apply ltnSn || exact FIFO_CFG.(WAIT_pos)))).
- *)
-
- Lemma FIFO_l_eq_bound ta tb (c : MFIFO.Counter_t) :
+
+ Lemma FIFO_l_counter_border t :
+ FIFO_counter # t.(Implementation_State) = WAIT.-1 ->
+ FIFO_counter # (t.+1).(Implementation_State) = 0.
+ Proof.
+ intros Hco; simpl.
+ unfold Next_state;
+ destruct_state t; simpl; try reflexivity;
+ simpl in Hco; unfold Next_cycle; set (HH := c.+1 < WAIT);
+ dependent destruction HH;
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e;
+ try reflexivity;
+ rewrite Hco in x; lia.
+ Qed.
+
+ Lemma isIDLE_fromstate ta c0 r:
+ (# ta).(Implementation_State) = IDLE c0 r ->
+ isIDLE (# ta).(Implementation_State).
+ Proof.
+ rewrite /isIDLE; intros H; by rewrite H.
+ Qed.
+
+ Lemma isIDLE_notRunning ta:
+ isIDLE (# ta).(Implementation_State) ->
+ isRUNNING (# ta).(Implementation_State) == false.
+ Proof.
+ intros; rewrite /isRUNNING; rewrite /isIDLE in H; simpl in H.
+ by destruct (# ta).(Implementation_State) eqn:Hs.
+ Qed.
+
+ Lemma FIFO_running ta tb (d : Counter_t):
+ isIDLE (Default_arbitrate ta).(Implementation_State)
+ -> isRUNNING (Default_arbitrate tb).(Implementation_State)
+ -> ta < tb
+ -> FIFO_counter (Default_arbitrate ta).(Implementation_State) = 0
+ (* Where still idle *)
+ -> ((ta + d < tb) && (isRUNNING (Default_arbitrate (ta + d)).(Implementation_State) == false))
+ (* There exists a moment r previous to d in which the counter was 0 (at the beginnin of RUNNING) *)
+ \/ (exists r, (ta + r <= tb) && (r <= d) && (isRUNNING # (ta + r).(Implementation_State))
+ && (FIFO_counter # (ta + r).(Implementation_State) == 0)).
+ Proof.
+ intros Hidle_a Hrun_b Hlt Hc.
+ destruct d as [d Hd].
+ induction d;
+ [ apply isIDLE_notRunning in Hidle_a; left; simpl; by rewrite addn0 Hlt andTb Hidle_a | ].
+ apply ltn_trans with (m := d) in Hd as Hd'; [ | lia ].
+ specialize IHd with (Hd := Hd') as [IH | IH]; simpl in IH.
+ { (* we're still idle after D cycles, next cycle could be IDLE, RUNNING or REFRESH *)
+ move : IH => /andP [IH Hrun_a'].
+ rewrite leq_eqVlt in IH; move : IH => /orP [/eqP IH | IH].
+ { (* tb is the cycle after *)
+ right. simpl. subst tb. exists (d.+1).
+ rewrite ltnSn andbT addnS Hrun_b andbT leqnn andTb /FIFO_counter.
+ rewrite /isRUNNING //= /Next_state in Hrun_b Hrun_a' *.
+ destruct ((Default_arbitrate (ta + d)).(Implementation_State)) eqn:HS, (r) eqn:HP; simpl; done. }
+ { (* now tb is in the future *)
+ simpl; rewrite /isIDLE in Hrun_a'.
+ destruct ((Default_arbitrate (ta + d)).(Implementation_State)) eqn:HS; simpl.
+ { (* from IDLE to REFRESH 1 *)
+ rewrite addnS IH andTb //= /Next_state HS.
+ destruct r; simpl; [ by left | ].
+ right; exists (d.+1); apply ltnW in IH.
+ rewrite addnS IH andTb ltnSn andTb.
+ by rewrite /isRUNNING /FIFO_counter //= HS.
+ }
+ by contradict Hrun_a'.
+ }
+ }
+ right. destruct IH as [r H]; move : H => /andP [/andP [/andP [Hlt' Hrd ] Hrun_a'] Hc'].
+ exists r; simpl.
+ rewrite Hlt' andTb; apply /andP; split.
+ { apply /andP. split.
+ { apply leq_trans with (n := d); (exact Hrd || apply ltnW, ltnSn). }
+ exact Hrun_a'.
+ }
+ exact Hc'.
+ Qed.
+
+ Lemma FIFO_counter_lt_WAIT t:
+ FIFO_counter (# t).(Implementation_State) < WAIT.
+ Proof.
+ set (c := FIFO_counter (Default_arbitrate t).(Implementation_State)).
+ unfold FIFO_counter in c; destruct_state t; subst c; try done.
+ Qed.
+
+ Lemma FIFO_running_at_zero_lt_at_c t t' d:
+ isRUNNING (# t).(Implementation_State) ->
+ t < t' -> FIFO_counter (# t).(Implementation_State) = 0 ->
+ d < FIFO_counter (# t').(Implementation_State) ->
+ t + d < t'.
+ Proof.
+ intros Hrun Hlt HcZ Hd.
+ induction d; [ by rewrite addn0 | ].
+ apply ltn_trans with (m := d) in Hd as IH; [ | lia ].
+ apply IHd in IH; clear IHd.
+ rewrite addnS ltn_neqAle IH andbT.
+ specialize (FIFO_counter_lt_WAIT t') as HW.
+ destruct ((t + d).+1 == t') eqn:H.
+ apply FIFO_add_counter with (c := OCycle0) (d := d.+1) in Hrun as [_ HcD].
+ 4: done.
+ 3: exact HcZ.
+ 2: rewrite add0n; apply ltn_trans with (n := FIFO_counter (Default_arbitrate t').(Implementation_State)); exact Hd || exact HW.
+ move : H => /eqP H; subst.
+ contradict Hd.
+ by rewrite -addnS HcD add0n ltnn.
+ Qed.
+
+ Lemma isRUNNING_fromstate ta c0 r r0:
+ (# ta).(Implementation_State) = RUNNING c0 r r0 ->
+ isRUNNING (# ta).(Implementation_State).
+ Proof.
+ rewrite /isRUNNING; intros H; by rewrite H.
+ Qed.
+
+ Lemma FIFO_l_helper_4 ta tb cb:
+ ta < tb ->
+ FIFO_counter # (ta.+1).(Implementation_State) = 0 ->
+ FIFO_counter # tb.(Implementation_State) = cb ->
+ cb > 0 -> ta.+1 < tb.
+ Proof.
+ intros Hlt Hca Hcb Hcb_pos.
+ rewrite ltn_neqAle Hlt andbT.
+ destruct (_ == tb) eqn:He; [ | done ].
+ move: He => /eqP He.
+ rewrite -He in Hcb; lia.
+ Qed.
+
+ Lemma FIFO_l_helper_3 ta tb d (cb : Counter_t) :
+ isRUNNING (# ta).(Implementation_State) ->
+ FIFO_counter (# ta).(Implementation_State) = 0 ->
+ FIFO_counter (# tb).(Implementation_State) = cb ->
+ d < cb -> ta < tb -> ta + d < tb.
+ Proof.
+ intros Hrun_a Hca Hcb Hd Hlt.
+ induction d; [ lia | ].
+ apply ltn_trans with (m:= d) in Hd as Hd'; [ | apply ltnSn ].
+ apply IHd in Hd' as H.
+ rewrite addnS ltn_neqAle H andbT.
+ destruct ( _ == tb) eqn:He; [ | done ].
+ move: He => /eqP He.
+ apply FIFO_add_counter with (d := d.+1) (c := Ordinal WAIT_pos) in Hrun_a as HH; simpl; try assumption.
+ 2: rewrite add0n; apply ltn_trans with (n := cb); (exact Hd || by destruct cb).
+ destruct HH as [Hrun_adp1 Hc_adp1]; simpl in Hc_adp1.
+ rewrite -He in Hcb.
+ rewrite add0n addnS in Hc_adp1.
+ rewrite Hc_adp1 in Hcb.
+ contradict Hcb; apply /eqP.
+ rewrite neq_ltn; apply /orP; left; exact Hd.
+ Qed.
+
+ Lemma FIFO_l_eq_bound ta tb (c : Counter_t) :
isRUNNING (# ta).(Implementation_State) ->
isRUNNING (# tb).(Implementation_State) ->
ta < tb ->
@@ -214,96 +375,87 @@ Module FIFOPROOFS (SYS : SystemModule).
[ rewrite subnKC; [ reflexivity | ]; apply (FIFO_counter_bounded_ c) | ].
rewrite H in Hc_a'; clear H.
- (* stopped here in the retrofitting *)
- apply FIFO_l_counter_border in Hc_a' as Hc_a''.
- destruct (FIFO_counter (Default_arbitrate tb).(Implementation_State) == 0) eqn:HcZ.
- { move : HcZ => /eqP HcZ.
- rewrite HcZ in Hc_b; rewrite -Hc_b subn0 -addnS prednK in Hlt'; exact WAIT_pos || exact Hlt'.
- }
- move : HcZ => /negbT HcZ; rewrite -lt0n in HcZ.
- destruct (Default_arbitrate (ta + (WAIT.-1 - c)).+1).(Implementation_State) eqn:Hs.
- { (* IDLE branch *)
- assert (FIFO_counter (Default_arbitrate (ta + (WAIT.-1 - c)).+1).(Implementation_State) = 0) as Haux.
- { rewrite /FIFO_counter Hs. by rewrite /FIFO_counter in Hc_a''. }
- clear Hc_a''; rename Haux into Hc_a''; apply isIDLE_fromstate in Hs as Hrun_a''.
- rewrite leq_eqVlt in Hlt'; move : Hlt' => /orP [/eqP Hlt' | Hlt'].
- { subst tb.
- rewrite Hc_b in Hc_a''.
- rewrite Hc_a'' subn0 -addnS prednK.
- 2: exact WAIT_pos.
- apply leqnn.
- }
- apply FIFO_running with (tb := tb) (d := c) in Hrun_a'' as [Hlt'' | Hlt''].
- 5: exact Hc_a''.
- 4: exact Hlt'.
- 3: exact Hrun_b.
- { (* Stays IDLE until the counter equals c again *)
- move : Hlt'' => /andP [Hlt'' _].
- rewrite -[(ta + _).+1]addnS -subSn in Hlt''.
- 2: rewrite -ltnS prednK; ( by destruct c) || exact WAIT_pos.
- rewrite prednK in Hlt''.
- 2: exact WAIT_pos.
- rewrite addnBA in Hlt''.
- 2: apply ltnW; by destruct c.
- rewrite subnK in Hlt''.
- 2: apply nat_leq_addl; apply ltnW; by destruct c.
- by apply ltnW.
- }
- move : Hlt'' => [r1 /andP [/andP [/andP [Hlt'' Hr ] Hrun_a'''] /eqP Hc_a''']].
- rewrite leq_eqVlt in Hlt''; move : Hlt'' => /orP [/eqP Hlt'' | Hlt''].
- { subst tb.
- rewrite Hc_b in Hc_a'''.
- rewrite Hc_a''' subn0 -addnS prednK.
- 2: exact WAIT_pos.
- apply leq_addr.
- }
- apply FIFO_running_at_zero_lt_at_c with (t' := tb) (d := (FIFO_counter (Default_arbitrate tb).(Implementation_State)).-1) in Hrun_a''' as Hlt'''.
- 4: rewrite ltn_predL; exact HcZ.
- 3: exact Hc_a'''.
- 2: exact Hlt''.
- rewrite Hc_b in Hlt'''.
- rewrite -[(ta + _).+1]addnS -subSn in Hlt'''.
- 2: rewrite -ltnS prednK; (by destruct c) || exact WAIT_pos.
- rewrite prednK in Hlt'''.
- 2: exact WAIT_pos.
- rewrite -subn1 addnBA in Hlt'''.
- 2: rewrite -Hc_b; exact HcZ.
- rewrite subn1 addnBA in Hlt'''.
- 2: apply ltnW; by destruct c.
- rewrite prednK in Hlt'''.
- 2: apply ltn_addl; by rewrite -Hc_b.
- rewrite addnBAC in Hlt'''.
- 2: apply nat_leq_addl; apply ltnW; (by destruct c) || exact WAIT_pos.
- rewrite subnK in Hlt'''.
- 2: apply nat_leq_addr, nat_leq_addl; apply ltnW; (by destruct c) || exact WAIT_pos.
- apply leq_trans with (m := ta + WAIT ) in Hlt'''.
- 2: by apply nat_leq_addr.
- exact Hlt'''.
- }
- { (* RUNNING branch *)
- assert (FIFO_counter (Default_arbitrate (ta + (WAIT.-1 - c)).+1).(Implementation_State) = 0) as Haux.
- { rewrite /FIFO_counter Hs. by rewrite /FIFO_counter in Hc_a''. }
- clear Hc_a''; rename Haux into Hc_a''.
- apply isRUNNING_fromstate in Hs as Hrun_a''.
- apply FIFO_l_helper_4 with (cb := c) in Hlt' as Hlt''.
- 4: by rewrite -Hc_b.
- 3: exact Hc_b.
- 2: exact Hc_a''.
- apply FIFO_l_helper_3 with (tb := tb) (d := c.-1) (cb := c) in Hrun_a'' as Hlt'''.
- 5: exact Hlt''.
- 4: by rewrite ltn_predL -Hc_b.
- 3: exact Hc_b.
- 2: exact Hc_a''.
- rewrite -addnS prednK in Hlt'''.
- 2: by rewrite -Hc_b.
- rewrite -addnS -subSS prednK in Hlt'''.
- 2: exact WAIT_pos.
- rewrite subnS prednK in Hlt'''.
- 2: rewrite subn_gt0; by destruct c.
- rewrite -addnA subnK in Hlt'''.
- 2: { destruct c; simpl; rewrite leq_eqVlt; apply /orP; by right. }
- exact Hlt'''.
- }
+ apply FIFO_l_counter_border in Hc_a' as Hc_a''.
+ destruct (FIFO_counter # tb.(Implementation_State) == 0) eqn:HcZ.
+ { move : HcZ => /eqP HcZ.
+ rewrite HcZ in Hc_b; rewrite -Hc_b subn0 -addnS prednK in Hlt'; exact WAIT_pos || exact Hlt'.
+ }
+ move : HcZ => /negbT HcZ; rewrite -lt0n in HcZ.
+ destruct # ((ta + (WAIT.-1 - c)).+1).(Implementation_State) eqn:Hs.
+ { (* IDLE branch *)
+ assert (Haux: FIFO_counter # ((ta + (WAIT.-1 - c)).+1).(Implementation_State) = 0);
+ [ rewrite /FIFO_counter Hs; by rewrite /FIFO_counter in Hc_a'' | ].
+
+ clear Hc_a''; rename Haux into Hc_a''; apply isIDLE_fromstate in Hs as Hrun_a''.
+ rewrite leq_eqVlt in Hlt'; move : Hlt' => /orP [/eqP Hlt' | Hlt'].
+ { subst tb.
+ rewrite Hc_b in Hc_a''.
+ rewrite Hc_a'' subn0 -addnS prednK; [ | exact WAIT_pos ].
+ apply leqnn.
+ }
+ apply FIFO_running with (tb := tb) (d := c) in Hrun_a'' as [Hlt'' | Hlt'']; try assumption.
+ { (* Stays IDLE until the counter equals c again *)
+ move : Hlt'' => /andP [Hlt'' _].
+ rewrite -[(ta + _).+1]addnS -subSn in Hlt''.
+ 2: rewrite -ltnS prednK; ( by destruct c) || exact WAIT_pos.
+ rewrite prednK in Hlt''.
+ 2: exact WAIT_pos.
+ rewrite addnBA in Hlt''.
+ 2: apply ltnW; by destruct c.
+ rewrite subnK in Hlt''.
+ 2: destruct c; simpl; lia.
+ by apply ltnW.
+ }
+ move : Hlt'' => [r1 /andP [/andP [/andP [Hlt'' Hr ] Hrun_a'''] /eqP Hc_a''']].
+ rewrite leq_eqVlt in Hlt''; move : Hlt'' => /orP [/eqP Hlt'' | Hlt''].
+ { subst tb.
+ rewrite Hc_b in Hc_a'''.
+ rewrite Hc_a''' subn0 -addnS prednK; [ | exact WAIT_pos ].
+ apply leq_addr.
+ }
+ apply FIFO_running_at_zero_lt_at_c with (t' := tb) (d := (FIFO_counter (# tb).(Implementation_State)).-1) in Hrun_a''' as Hlt''';
+ try (by rewrite ltn_predL; exact HcZ); try assumption.
+ rewrite Hc_b in Hlt'''.
+ rewrite -[(ta + _).+1]addnS -subSn in Hlt'''.
+ 2: rewrite -ltnS prednK; (by destruct c) || exact WAIT_pos.
+ rewrite prednK in Hlt'''.
+ 2: exact WAIT_pos.
+ rewrite -subn1 addnBA in Hlt'''.
+ 2: rewrite -Hc_b; exact HcZ.
+ rewrite subn1 addnBA in Hlt'''.
+ 2: apply ltnW; by destruct c.
+ rewrite prednK in Hlt'''.
+ 2: apply ltn_addl; by rewrite -Hc_b.
+ rewrite addnBAC in Hlt'''.
+ 2: destruct c; simpl; lia.
+ rewrite subnK in Hlt'''.
+ 2: destruct c; simpl; lia.
+ apply leq_trans with (m := ta + WAIT ) in Hlt'''.
+ 2: destruct c; simpl; lia.
+ exact Hlt'''.
+ }
+ { (* RUNNING branch *)
+ assert (FIFO_counter (Default_arbitrate (ta + (WAIT.-1 - c)).+1).(Implementation_State) = 0) as Haux.
+ { rewrite /FIFO_counter Hs. by rewrite /FIFO_counter in Hc_a''. }
+ clear Hc_a''; rename Haux into Hc_a''.
+ apply isRUNNING_fromstate in Hs as Hrun_a''.
+ apply FIFO_l_helper_4 with (cb := c) in Hlt' as Hlt''; try assumption.
+ 2: by rewrite -Hc_b.
+ apply FIFO_l_helper_3 with (tb := tb) (d := c.-1) (cb := c) in Hrun_a'' as Hlt'''.
+ 5: exact Hlt''.
+ 4: by rewrite ltn_predL -Hc_b.
+ 3: exact Hc_b.
+ 2: exact Hc_a''.
+ rewrite -addnS prednK in Hlt'''.
+ 2: by rewrite -Hc_b.
+ rewrite -addnS -subSS prednK in Hlt'''.
+ 2: exact WAIT_pos.
+ rewrite subnS prednK in Hlt'''.
+ 2: rewrite subn_gt0; by destruct c.
+ rewrite -addnA subnK in Hlt'''.
+ 2: { destruct c; simpl; rewrite leq_eqVlt; apply /orP; by right. }
+ exact Hlt'''.
+ }
Qed.
Lemma FIFO_l_eq_bound_or ta tb (c : Counter_t) :
@@ -315,20 +467,29 @@ Module FIFOPROOFS (SYS : SystemModule).
Proof.
intros Hrun_a Hc_a Hrun_b Hc_b.
destruct (ta < tb) eqn:Hlt.
- { apply FIFO_l_eq_bound with (ta := ta) (c := c) in Hrun_b.
- all: try done.
- right. by left. }
+ { apply FIFO_l_eq_bound with (ta := ta) (c := c) in Hrun_b; try done;
+ right; by left. }
{ rewrite ltnNge in Hlt; apply negbFE in Hlt.
- rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP Heq | Hlt].
- { by left. }
- apply FIFO_l_eq_bound with (ta := tb) (c := c) in Hrun_a.
- all: try done.
- right. by right. }
+ rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP Heq | Hlt]; [ by left | ].
+ apply FIFO_l_eq_bound with (ta := tb) (c := c) in Hrun_a; try done.
+ right; by right. }
Qed.
+
+ Lemma FIFO_date_gt_0 cmd t:
+ cmd \in (# t).(Arbiter_Commands) -> cmd.(CDate) > 0.
+ Proof.
+ induction t; simpl; [ intros H; inversion H | ].
+ unfold Next_state; destruct_state t; rewrite in_cons; intros H; move: H => /orP [/eqP H | H];
+ try (by rewrite H //=);
+ by apply IHt in H.
+ Qed.
+ (* ------------------------------------------------------------------ *)
+ (* --------------------- TIMING PROOFS ------------------------------ *)
+ (* ------------------------------------------------------------------ *)
Theorem Cmds_T_RCD_ok t a b:
a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
- isACT a -> isCAS b -> (get_bank a == get_bank b) -> Before a b ->
+ isACT a -> isCAS b -> Same_Bank a b -> Before a b ->
Apart_at_least a b T_RCD.
Proof.
intros Ha Hb iAa iCb SB aBb; rewrite /Apart_at_least.
@@ -339,165 +500,307 @@ Module FIFOPROOFS (SYS : SystemModule).
2: {
unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
rewrite subnKC; [ exact FIFO_WAIT_GT_SCAS | ].
- unfold CAS_date; lia. }
+ unfold CAS_date; lia.
+ }
unfold d in Hc_a'; rewrite subnKC in Hc_a'.
2 : rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS; unfold CAS_date; lia.
-
- apply FIFO_l_eq_bound_or with (ta := a.(CDate) + d) (c := Next_cycle OCAS_date) in Hrun_b as H.
- 2-4: done.
+ apply FIFO_l_eq_bound_or with (ta := a.(CDate) + d) (c := Next_cycle OCAS_date) in Hrun_b as H; try done.
destruct H as [H0 | [H1 | H2]].
- { rewrite -H0 leq_add2l. unfold d.
- rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS /CAS_date /ACT_date.
- rewrite prednK.
- 2: { rewrite lt0n. exact T_RP_pos. }
- rewrite -addnS addnC -addn1. rewrite -addnA [1 + T_RP.-1]addnC addn1 prednK.
- 2: { rewrite lt0n. exact T_RP_pos. }
- rewrite -addnBA.
- 2: by rewrite leqnn.
- 1: apply leq_addr. }
- { unfold d in H1; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS in H1.
- apply leq_trans with (m := a.(CDate) + T_RCD) in H1.
- exact H1.
- rewrite -addnA leq_add2l /CAS_date /ACT_date prednK.
- rewrite [T_RP.-1 + _]addnC -addnS prednK.
- 2,3: rewrite lt0n; exact T_RP_pos.
- rewrite addnBAC.
- 2: by rewrite addnC leq_addr.
- rewrite leq_subRL.
- 2: by rewrite [T_RCD + T_RP]addnC -addnA leq_addr.
- by rewrite addnC leq_addr. }
- { unfold d in H2; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS in H2.
- contradict H2. apply /negP. rewrite -ltnNge addnC -ltn_subRL.
- unfold Before in aBb. apply ltn_trans with (n := b.(CDate)).
- exact aBb.
- rewrite subnBA.
- 2: { rewrite /CAS_date /ACT_date -addnS. by apply nat_ltn_add. }
- rewrite ltn_subRL addnC -addnA ltn_add2l.
- rewrite /CAS_date /ACT_date prednK.
- rewrite addnC -addnS prednK.
- 3,2: rewrite lt0n; exact T_RP_pos.
- rewrite ltn_add2r.
- apply nat_add_ltn with (m := T_RP.-1).
- { rewrite ltn_predRL. exact T_RP_GT_ONE. }
- specialize WAIT_CAS; by rewrite /CAS_date /ACT_date. }
+ { rewrite -H0 leq_add2l. unfold d.
+ rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS /CAS_date /ACT_date.
+ rewrite prednK; [ | specialize T_RP_pos; lia ].
+ rewrite -addnS addnC -addn1 -addnA [1 + T_RP.-1]addnC addn1 prednK; [ | specialize T_RP_pos; lia ].
+ rewrite -addnBA; [ | lia ].
+ apply leq_addr. }
+ { unfold d in H1; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS in H1.
+ apply leq_trans with (m := a.(CDate) + T_RCD) in H1; try assumption.
+ rewrite -addnA leq_add2l /CAS_date /ACT_date prednK.
+ rewrite [T_RP.-1 + _]addnC -addnS prednK.
+ 2,3: rewrite lt0n; exact T_RP_pos.
+ rewrite addnBAC; [ | lia ].
+ rewrite leq_subRL; [ | lia ].
+ lia. }
+ { unfold d in H2; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS in H2.
+ contradict H2. apply /negP. rewrite -ltnNge addnC -ltn_subRL.
+ unfold Before in aBb. apply ltn_trans with (n := b.(CDate)); [ assumption | ].
+ rewrite subnBA; [ | rewrite /CAS_date /ACT_date -addnS; lia].
+ rewrite ltn_subRL addnC -addnA ltn_add2l.
+ rewrite /CAS_date /ACT_date prednK; [ | by specialize T_RP_pos; lia].
+ rewrite addnC -addnS prednK; [ | by specialize T_RP_pos; lia].
+ rewrite ltn_add2r.
+ apply nat_add_ltn with (m := T_RP.-1);
+ [ specialize T_RP_GT_ONE; lia | ].
+ specialize WAIT_CAS; by rewrite /CAS_date /ACT_date.
+ }
Qed.
-
-
-
-
-
-
- Lemma isIDLE_notRunning ta:
- isIDLE (Default_arbitrate ta).(Implementation_State) -> isRUNNING (Default_arbitrate ta).(Implementation_State) == false.
+ Theorem Cmds_T_RP_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isPRE a -> isACT b -> Same_Bank a b -> Before a b ->
+ Apart_at_least a b T_RP.
Proof.
- intros.
- rewrite /isRUNNING; rewrite /isIDLE in H; simpl in H.
- by destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
+ intros Ha Hb iPa iAb SB aBb; rewrite /Apart_at_least.
+ apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]]; [ | assumption ].
+ apply FIFO_PRE_date in Ha as [Hc_a [Hrun_a _]]; [ | assumption ].
+ apply FIFO_running_at_zero_lt_at_c with (t':= b.(CDate)) (d := ACT_date) in Hc_a as H; try assumption.
+ 2: rewrite Hc_b; by rewrite FIFO_nextcycle_act_eq_actS.
+ unfold ACT_date in H.
+ rewrite -addnS prednK in H; [ assumption | specialize T_RP_pos; lia ].
Qed.
- Lemma isIDLE_fromstate ta c0 r:
- (Default_arbitrate ta).(Implementation_State) = IDLE c0 r ->
- isIDLE (Default_arbitrate ta).(Implementation_State).
+ Theorem Cmds_T_RC_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isACT a -> isACT b -> Same_Bank a b -> Before a b ->
+ Apart_at_least a b T_RC.
Proof.
- rewrite /isIDLE.
- intros H; by rewrite H.
+ intros Ha Hb iAa iAb SB aBb; rewrite /Apart_at_least.
+ apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]]; [ | assumption ].
+ apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]]; [ | assumption ].
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt; try done.
+ apply leq_trans with (n := (a.(CDate) + WAIT)); [ | assumption ].
+ rewrite leq_add2l; specialize RC_WAIT; lia.
Qed.
-
- Lemma isRUNNING_fromstate ta c0 r r0:
- (Default_arbitrate ta).(Implementation_State) = RUNNING c0 r r0 ->
- isRUNNING (Default_arbitrate ta).(Implementation_State).
+
+ Theorem Cmds_T_RAS_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isACT a -> isPRE b -> Same_Bank a b -> Before a b ->
+ Apart_at_least a b T_RAS.
Proof.
- rewrite /isRUNNING; intros H; by rewrite H.
+ intros Ha Hb iAa iPb SB aBb; rewrite /Apart_at_least.
+ apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]]; [ | assumption ].
+ apply FIFO_PRE_date in Hb as [Hc_b [Hrun_b _]]; [ | assumption ]; clear iAa iPb.
+ apply FIFO_add_counter with (d := Next_cycle OACT_date) in Hc_b as H; try done.
+ 2: by rewrite /OCycle0 add0n FIFO_nextcycle_act_eq_actS FIFO_WAIT_GT_SACT.
+ destruct H as [Hrun_b' Hc_b'].
+ set (d := Next_cycle OACT_date); fold d in Hc_b', Hrun_b'; rewrite /OCycle0 add0n in Hc_b'.
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (c := d) (tb := b.(CDate) + d) in Hrun_a as Hlt; try done.
+ 2: {
+ rewrite /Before in aBb. apply ltn_trans with (p := b.(CDate) + d) in aBb. exact aBb.
+ apply nat_ltn_add; unfold d; by rewrite FIFO_nextcycle_act_eq_actS.
+ }
+ rewrite [_ + d]addnC -leq_subLR in Hlt; unfold d in Hlt.
+ apply leq_trans with (m := a.(CDate) + T_RAS) in Hlt; [ exact Hlt | ].
+ rewrite -addnBA.
+ 2: rewrite FIFO_nextcycle_act_eq_actS; specialize FIFO_WAIT_GT_SACT; apply ltnW.
+ rewrite leq_add2l leq_subRL.
+ 2: rewrite FIFO_nextcycle_act_eq_actS; specialize FIFO_WAIT_GT_SACT; apply ltnW.
+ rewrite FIFO_nextcycle_act_eq_actS /ACT_date prednK.
+ 2: by rewrite lt0n T_RP_pos.
+ by rewrite leq_eqVlt RAS_WAIT orbT.
Qed.
- Lemma FIFO_wait_neq_act :
- (WAIT.-1 == OACT_date) = false.
+ Theorem Cmds_T_RTP_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isCRD a -> isPRE b -> Same_Bank a b -> Before a b -> Apart_at_least a b T_RTP.
Proof.
- apply /negbTE; rewrite neq_ltn.
- apply /orP; right.
- rewrite ltn_predRL.
- apply ltn_trans with (n := OCAS_date).
- 2: exact WAIT_CAS.
- unfold OCAS_date, OACT_date; simpl; unfold CAS_date.
- rewrite -ltn_subLR.
- 2: auto.
- rewrite subSnn.
- exact T_RCD_GT_ONE.
+ intros Ha Hb iCa iPb sB aBb; rewrite /Apart_at_least.
+ apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
+ 2: unfold isCAS; unfold isCRD in iCa; apply /orP; left; exact iCa.
+ apply FIFO_PRE_date in Hb as [Hc_b [Hrun_b _]]; [ | assumption ].
+ apply FIFO_add_counter with (c := OCycle0) (d := CAS_date.+1) in Hrun_b as [Hrun_b' Hc_b']; try assumption.
+ 2: simpl; rewrite add0n; exact FIFO_WAIT_GT_SCAS.
+ rewrite -{2}FIFO_next_cycle_cas_eq_casS in Hc_b'; simpl in Hc_b'; rewrite add0n in Hc_b'.
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate) + CAS_date.+1) (c := Next_cycle OCAS_date) in Hrun_a as H; try assumption.
+ 2: unfold Before in aBb; apply ltn_trans with (p := b.(CDate) + CAS_date.+1) in aBb; exact aBb || (by rewrite nat_ltn_add).
+ rewrite [b.(CDate) + _]addnC -leq_subLR in H.
+ apply leq_trans with (n := a.(CDate) + WAIT - CAS_date.+1); [ | assumption ].
+ rewrite -addnBA; [ | exact WAIT_CAS].
+ rewrite leq_add2l leq_subRL; [ | exact WAIT_CAS ].
+ rewrite addnC addnS addnC; exact WAIT_END_READ.
Qed.
- Lemma FIFO_wait_neq_cas :
- (WAIT.-1 == OCAS_date) = false.
+ Theorem Cmds_T_WTP_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ isCWR a -> isPRE b -> Same_Bank a b -> Before a b ->
+ Apart_at_least a b (T_WR + T_WL + T_BURST).
Proof.
- apply /negbTE; rewrite neq_ltn.
- apply /orP; right.
- rewrite ltn_predRL.
- apply ltn_trans with (n := CAS_date + T_RTP).
- 2: exact WAIT_END_READ.
- rewrite -ltn_subLR.
- 2: auto.
- rewrite subSnn.
- exact T_RTP_GT_ONE.
+ intros Ha Hb iCa iPb sB aBb; rewrite /Apart_at_least.
+ apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
+ 2: unfold isCAS; unfold isCWR in iCa; apply /orP; right; exact iCa.
+ apply FIFO_PRE_date in Hb as [Hc_b [Hrun_b _]]; [ | assumption ].
+ apply FIFO_add_counter with (c := OCycle0) (d := CAS_date.+1) in Hrun_b as [Hrun_b' Hc_b']; try assumption.
+ 2: simpl; rewrite add0n; exact FIFO_WAIT_GT_SCAS.
+ rewrite -{2}FIFO_next_cycle_cas_eq_casS in Hc_b'; simpl in Hc_b'; rewrite add0n in Hc_b'.
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate) + CAS_date.+1) (c := Next_cycle OCAS_date) in Hrun_a as H; try done.
+ 2: unfold Before in aBb; apply ltn_trans with (p := b.(CDate) + CAS_date.+1) in aBb; exact aBb || (by rewrite nat_ltn_add).
+ rewrite [b.(CDate) + _]addnC -leq_subLR in H.
+ apply leq_trans with (n := a.(CDate) + WAIT - CAS_date.+1); [ | assumption ].
+ rewrite -addnBA; [ | exact WAIT_CAS ].
+ rewrite leq_add2l leq_subRL; [ | exact WAIT_CAS ].
+ rewrite addnC addnS addnC !addnA.
+ exact WAIT_END_WRITE.
Qed.
- Lemma FIFO_counter_lt_WAIT t:
- FIFO_counter (Default_arbitrate t).(Implementation_State) < WAIT.
+ Theorem Cmds_T_RtoW_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isCRD a -> isCWR b -> Before a b -> Apart_at_least a b T_RTW.
Proof.
- set (c := FIFO_counter (Default_arbitrate t).(Implementation_State)).
- unfold FIFO_counter in c.
- destruct (Default_arbitrate t).(Implementation_State) eqn:HS.
- all: subst c; (done || by destruct c0).
+ intros Ha Hb iCRa iCWb aBb; rewrite /Apart_at_least.
+ apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
+ 2 : unfold isCAS; rewrite iCRa; done.
+ apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]].
+ 2 : unfold isCAS; rewrite iCWb orbT; done.
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OCAS_date) in Hrun_a as H; try done.
+ apply leq_trans with (n := a.(CDate) + WAIT); [ | assumption ].
+ by rewrite leq_add2l leq_eqVlt RTW_WAIT orbT.
Qed.
-
+ Theorem Cmds_T_WtoR_SBG_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isCWR a -> isCRD b -> Before a b -> Same_Bankgroup a b->
+ Apart_at_least a b (T_WTR_l + T_WL + T_BURST).
+ Proof.
+ intros Ha Hb iCWa iCRb abB SBG; rewrite /Apart_at_least.
+ apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]]; [ | by unfold isCAS; rewrite iCWa orbT; done ].
+ apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]]; [ | by unfold isCAS; rewrite iCRb; done ].
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OCAS_date) in Hrun_a as H; try done.
+ apply leq_trans with (n := a.(CDate) + WAIT); [ | assumption ].
+ by rewrite leq_add2l leq_eqVlt WTR_WAIT orbT.
+ Qed.
+
+ (* if they always respect the long then they should also always respect the small *)
+ Theorem Cmds_T_WtoR_DBG_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isCWR a -> isCRD b -> Before a b -> ~~ Same_Bankgroup a b ->
+ Apart_at_least a b (T_WTR_s + T_WL + T_BURST).
+ Proof.
+ intros Ha Hb iCWa iCRb abB nSBG; rewrite /Apart_at_least.
+ apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]]; [ | by unfold isCAS; rewrite iCWa orbT; done ].
+ apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]]; [ | by unfold isCAS; rewrite iCRb; done ].
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OCAS_date) in Hrun_a as H; try done.
+ apply leq_trans with (n := a.(CDate) + WAIT); [ | assumption ].
+ rewrite leq_add2l; specialize WTR_WAIT; specialize T_WTR_bgs; lia.
+ Qed.
- Lemma FIFO_date_gt_0 cmd t:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> cmd.(CDate) > 0.
+ Theorem Cmds_T_CCD_SBG_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ (isCRD a /\ isCRD b) \/ (isCWR a /\ isCWR b) -> Before a b -> Same_Bankgroup a b ->
+ Apart_at_least a b T_CCD_l.
+ Proof.
+ intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
+ destruct Htype as [[iRa iRb] | [iWa iWb]];
+ apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]];
+ apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]]; try unfold isCAS;
+ try rewrite iRb; try rewrite iRa; try rewrite iWa; try rewrite iWb; try (done || by rewrite orbT);
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OCAS_date) in Hrun_a as H; try done;
+ apply leq_trans with (n := a.(CDate) + WAIT); try assumption;
+ by rewrite leq_add2l leq_eqVlt CCD_WAIT orbT.
+ Qed.
+
+ Theorem Cmds_T_CCD_DBG_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ (isCRD a /\ isCRD b) \/ (isCWR a /\ isCWR b) -> Before a b -> ~~ Same_Bankgroup a b ->
+ Apart_at_least a b T_CCD_s.
+ Proof.
+ intros Ha Hb Htype aBb sBG; unfold Apart_at_least;
+ destruct Htype as [[iRa iRb] | [iWa iWb]];
+ apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]];
+ apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]]; try unfold isCAS;
+ try rewrite iRb; try rewrite iRa; try rewrite iWa; try rewrite iWb; try (done || by rewrite orbT);
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OCAS_date) in Hrun_a as H; try done;
+ apply leq_trans with (n := a.(CDate) + WAIT); try assumption.
+ all: rewrite leq_add2l; specialize CCD_WAIT; specialize T_CCD_bgs; lia.
+ Qed.
+
+ Theorem Cmds_T_FAW_ok t a b c d:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ c \in (# t).(Arbiter_Commands) -> d \in (# t).(Arbiter_Commands) ->
+ isACT a -> isACT b -> isACT c -> isACT d -> Diff_Bank [::a;b;c;d] ->
+ Before a b -> Before b c -> Before c d ->
+ Apart_at_least a d T_FAW.
Proof.
- induction t.
- { simpl; intros H; inversion H. }
- simpl.
- unfold Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:HS, r eqn:HR; simpl.
- all: try (intros H; rewrite in_cons in H; move: H => /orP [/eqP H | H]).
- all: try (by rewrite H).
- all: try (by apply IHt in H).
- all: try (destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait); simpl.
- all: try (intros H; rewrite in_cons in H; move: H => /orP [/eqP H | H]).
- all: try (by rewrite H).
- all: try (by apply IHt in H).
+ intros Ha Hb Hc Hd iAa iAb iAc iAd dB aBb bBc cBd; rewrite /Apart_at_least.
+ apply FIFO_date_gt_0 in Ha as Ha_pos, Hb as Hb_pos, Hc as Hc_pos, Hd as Hd_pos.
+ apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]], Hb as [Hc_b [Hrun_b _]], Hc as [Hc_c [Hrun_c _]], Hd as [Hc_d [Hrun_d _]];
+ try assumption; clear iAa iAb iAc iAd.
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt_ab; try done.
+ apply FIFO_l_eq_bound with (ta := b.(CDate)) (tb := c.(CDate)) (c := Next_cycle OACT_date) in Hrun_b as Hlt_bc; try done.
+ apply FIFO_l_eq_bound with (ta := c.(CDate)) (tb := d.(CDate)) (c := Next_cycle OACT_date) in Hrun_c as Hlt_cd; try done.
+ apply leq_trans with (p := c.(CDate) - WAIT) in Hlt_ab as Hlt_ac.
+ 2: rewrite leq_psubRL; (rewrite -addnC; exact Hlt_bc) || exact Hb_pos.
+ rewrite leq_psubRL addnC in Hlt_ac.
+ 2: rewrite addn_gt0; apply /orP; left; exact WAIT_pos.
+ apply leq_trans with (p := d.(CDate) - WAIT) in Hlt_ac as Hlt_ad.
+ 2: rewrite leq_psubRL; (by rewrite -addnC) || exact Hc_pos.
+ rewrite leq_psubRL addnC in Hlt_ad.
+ 2: rewrite addn_gt0; apply /orP; left; exact WAIT_pos.
+ apply leq_trans with (n := (a.(CDate) + WAIT + WAIT + WAIT)); [ | assumption ].
+ by rewrite -addnA -addnA leq_add2l addnA leq_eqVlt FAW_WAIT orbT.
Qed.
- Lemma FIFO_in_the_past t t' a:
- t <= t' ->
- a \in (Default_arbitrate t).(Arbiter_Commands) ->
- a \in (Default_arbitrate t').(Arbiter_Commands).
- Proof.
- intros. rewrite leq_eqVlt in H; move: H => /orP [/eqP H | H]. { by rewrite -H. }
- induction t'.
- { inversion H. }
- rewrite leq_eqVlt in H; move: H => /orP [/eqP H | H].
- { apply eq_add_S in H.
- simpl; rewrite /Next_state //=.
- destruct (Default_arbitrate t').(Implementation_State), r eqn:HP; simpl.
- all: try (rewrite in_cons; apply /orP; right; subst t; exact H0).
- all: try (destruct (nat_of_ord c == ACT_date), (nat_of_ord c == CAS_date), (nat_of_ord c == WAIT.-1); simpl).
- all: try (rewrite in_cons; apply /orP; right; subst t; exact H0).
- }
- apply ltnSE in H; apply IHt' in H; simpl; rewrite /Next_state //=.
- destruct (Default_arbitrate t').(Implementation_State), r; simpl.
- all: try (rewrite in_cons; apply /orP; right; exact H).
- all: try (destruct (nat_of_ord c == ACT_date), (nat_of_ord c == CAS_date), (nat_of_ord c == WAIT.-1); simpl).
- all: try (rewrite in_cons; apply /orP; right; exact H).
+ Theorem Cmds_T_RRD_SBG_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isACT a -> isACT b -> ~~ Same_Bank a b -> Before a b -> Same_Bankgroup a b ->
+ Apart_at_least a b T_RRD_l.
+ Proof.
+ intros Ha Hb iAa iAb nSb aBb sBG; rewrite /Apart_at_least.
+ apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]], Hb as [Hc_b [Hrun_b _]]; try assumption; clear iAa iAb.
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt; try done.
+ apply leq_trans with (n := (a.(CDate) + WAIT)); [ | assumption ].
+ by rewrite leq_add2l leq_eqVlt RRD_WAIT orbT.
Qed.
- Lemma Cmd_in_trace cmd t:
+ Theorem Cmds_T_RRD_DBG_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isACT a -> isACT b -> ~~ Same_Bank a b -> Before a b -> ~~ Same_Bankgroup a b ->
+ Apart_at_least a b T_RRD_s.
+ Proof.
+ intros Ha Hb iAa iAb nSb aBb sBG; rewrite /Apart_at_least.
+ apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]], Hb as [Hc_b [Hrun_b _]]; try assumption; clear iAa iAb.
+ apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt; try done.
+ apply leq_trans with (n := (a.(CDate) + WAIT)); [ | assumption ].
+ rewrite leq_add2l; specialize RRD_WAIT; specialize T_RRD_bgs; lia.
+ Qed.
+
+ (* ------------------------------------------------------------------ *)
+ (* -------------------- REQUEST CORRECTNESS ------------------------- *)
+ (* ------------------------------------------------------------------ *)
+
+ Lemma FIFO_in_the_past t t' a : t <= t' ->
+ a \in (# t).(Arbiter_Commands) -> a \in (# t').(Arbiter_Commands).
+ Proof.
+ intros; rewrite leq_eqVlt in H; move: H => /orP [/eqP H | H]; [ by rewrite -H | ].
+ induction t'; [ inversion H | ].
+ rewrite leq_eqVlt in H; move: H => /orP [/eqP H | H].
+ { apply eq_add_S in H.
+ simpl; rewrite /Next_state //=.
+ destruct (Default_arbitrate t').(Implementation_State), r eqn:HP; simpl.
+ all: try (rewrite in_cons; apply /orP; right; subst t; exact H0);
+ try (destruct (nat_of_ord c == ACT_date), (nat_of_ord c == CAS_date), (nat_of_ord c == WAIT.-1); simpl);
+ try (rewrite in_cons; apply /orP; right; subst t; exact H0).
+ }
+ apply ltnSE in H; apply IHt' in H; simpl; rewrite /Next_state //=.
+ destruct (Default_arbitrate t').(Implementation_State), r; simpl.
+ all: try (rewrite in_cons; apply /orP; right; exact H);
+ try (destruct (nat_of_ord c == ACT_date), (nat_of_ord c == CAS_date), (nat_of_ord c == WAIT.-1); simpl);
+ try (rewrite in_cons; apply /orP; right; exact H).
+ Qed.
+
+ Lemma Date_gt_counter t:
+ isRUNNING (# t).(Implementation_State) ->
+ FIFO_counter (# t).(Implementation_State) < t.
+ Proof.
+ intros Hrun; induction t; [ done | ].
+ simpl in *; unfold Next_state in *.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs;
+ [ destruct r eqn:Hpp; simpl in *; done | ].
+ destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl in *;
+ rewrite Hact //= in Hrun;
+ rewrite Hact //=; try (rewrite Hcas //=).
+ 7: destruct r eqn:Hpp; simpl.
+ all:
+ try done;
+ try (apply IHt in Hrun);
+ unfold Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc;
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e;
+ try done; try rewrite Hcas //= in Hrun.
+ Qed.
+
+ Lemma Cmd_in_trace cmd t:
cmd \in (Default_arbitrate t).(Arbiter_Commands) ->
cmd.(CDate) <= t.
Proof.
- intros H.
- induction t.
- { by simpl in H. }
+ intros H; induction t; [ by simpl in H | ].
simpl in H; rewrite /Next_state in H.
destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
{ destruct r eqn:Hpp.
@@ -519,869 +822,701 @@ Module FIFOPROOFS (SYS : SystemModule).
all: try (apply IHt in H; by apply ltnW). }
Qed.
- Lemma Date_gt_counter t:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) < t.
- Proof.
- intros Hrun.
- induction t.
- { by simpl in Hrun. }
- simpl in *; unfold Next_state in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- { destruct r eqn:Hpp; simpl in *.
- all: done. }
- { destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl in *.
- all: rewrite Hact //= in Hrun.
- all: rewrite Hact //=; try (rewrite Hcas //=).
- 7: destruct r eqn:Hpp; simpl.
- all: try done.
- all: try (apply IHt in Hrun).
- all: unfold Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc.
- all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
- all: try done.
- all: try rewrite Hcas //= in Hrun. }
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* --------------------- PROOFS ABOUT THE COUNTER ------------------- *)
- (* ------------------------------------------------------------------ *)
-
- Lemma FIFO_inc_run (c : Counter_t) t:
- isRUNNING (Default_arbitrate t).(Implementation_State) -> FIFO_counter (Default_arbitrate t).(Implementation_State) = c ->
- c < WAIT.-1 -> isRUNNING (Default_arbitrate t.+1).(Implementation_State).
- Proof.
- intros Hrun Hc Hw.
- apply FIFO_inc_counter with (t := t) (c := c) in Hrun as Hc'.
- all: try done.
- simpl; unfold Next_state, isRUNNING.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (r) eqn:HP; simpl.
- all: try (by discriminate Hrun).
- all: destruct (nat_of_ord c0 == ACT_date) eqn:Hact, (nat_of_ord c0 == CAS_date) eqn:Hcas, (nat_of_ord c0 == WAIT.-1) eqn:Hwait; simpl.
- all: try done.
- all: try (unfold FIFO_counter in Hc; rewrite Hc in Hwait; move: Hwait => /eqP Hwait; rewrite Hwait in Hw; by rewrite ltnn in Hw).
- Qed.
-
- Lemma FIFO_l_counter_border t :
- FIFO_counter (Default_arbitrate t).(Implementation_State) = WAIT.-1 ->
- FIFO_counter (Default_arbitrate t.+1).(Implementation_State) = 0.
+ Lemma Request_starts_idle ra ta:
+ let S := (# ta).(Implementation_State) in
+ isIDLE S ->
+ ra \in FIFO_pending (S) ->
+ index ra (FIFO_pending S) = 0 ->
+ (FIFO_request (Default_arbitrate ta.+1).(Implementation_State) == Some ra) &&
+ (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0) &&
+ (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)).
Proof.
- intros Hco; simpl.
- unfold Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (r) eqn:HP; simpl.
- all: try done.
- all: destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas,
- (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl; intros.
- all: try done.
- all: unfold Next_cycle; set (HH := c.+1 < WAIT).
- all: dependent destruction HH.
- all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
- all: try done.
- all: try (move: Hwait => /eqP Hwait; rewrite Hwait prednK in x; (exact WAIT_pos || by rewrite ltnn in x)).
- all: try (unfold FIFO_counter in Hco; move: Hwait => /eqP Hwait; contradict Hwait; exact Hco).
+ intros S Hidle HP Hi.
+ unfold S in *; clear S.
+ destruct (# ta).(Implementation_State) eqn:Hs; [ | discriminate Hidle ].
+ rewrite //= /Next_state Hs.
+ destruct r eqn:HPP; [ discriminate HP | ].
+ rewrite //= eq_refl !andbT.
+ rewrite /FIFO_pending in Hi.
+ destruct (r0 == ra) eqn:Heq; [ move: Heq => /eqP Heq; by rewrite Heq | ].
+ by rewrite //= Heq in Hi.
Qed.
- Lemma FIFO_l_counter_border_run t :
- FIFO_pending (Default_arbitrate t).(Implementation_State) != [::] ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) = WAIT.-1 ->
- FIFO_counter (Default_arbitrate t.+1).(Implementation_State) = 0 /\ isRUNNING (Default_arbitrate t.+1).(Implementation_State).
+ Lemma Request_running_in_slot ra ta d:
+ FIFO_request (# ta).(Implementation_State) == Some ra ->
+ FIFO_counter (# ta).(Implementation_State) == OCycle0 ->
+ d < WAIT ->
+ (FIFO_request # (ta + d).(Implementation_State) == Some ra).
Proof.
- intros HP Hc; simpl.
- rewrite /Next_state //=.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs; simpl.
- { destruct r eqn:HPP; simpl.
- 2: done.
- by rewrite /FIFO_pending in HP.
- }
- { destruct c; simpl. destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait, r eqn:HPP; simpl in *.
- all: try done.
- all: unfold Next_cycle; simpl; set (H := m.+1 < WAIT); dependent destruction H.
- all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
- all: try done.
- all: rewrite Hc prednK in x.
- all: try exact WAIT_pos.
- all: by rewrite ltnn in x.
+ intros Hreq Hc Hd; induction d; [ by rewrite addn0 Hreq | ].
+ apply ltn_trans with (m := d) in Hd as Hd'; [ | done ].
+ apply IHd in Hd' as IH. clear IHd.
+ assert (isRUNNING (# ta).(Implementation_State)) as Hrun.
+ { destruct (Default_arbitrate ta).(Implementation_State); [ | done ].
+ rewrite /FIFO_request //= in Hreq.
}
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* --------------------- PROOFS ------------------------------------- *)
- (* ------------------------------------------------------------------ *)
-
- Lemma FIFO_PRE_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isPRE cmd ->
- (FIFO_counter (Default_arbitrate cmd.(CDate)).(Implementation_State) = OCycle0) /\
- (isRUNNING (Default_arbitrate cmd.(CDate)).(Implementation_State)) /\
- (FIFO_request (Default_arbitrate cmd.(CDate)).(Implementation_State) == Some cmd.(Request)).
- Proof.
- induction t.
- { done. }
- intros Hi Hp; simpl in *.
- rewrite /Next_state //= in Hi.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs; simpl in Hi.
- { destruct r eqn:HPP; simpl in Hi.
- all: rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi].
- all: try (contradict Hp; by rewrite Hi).
- all: try (apply IHt in Hi; (exact Hp || exact Hi)).
- rewrite Hi //= Hs //=. }
- { destruct c; simpl in *; destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl in Hi.
- 7: destruct r eqn: HPP.
- all: try (rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi]).
- all: try (apply IHt in Hi; (exact Hp || exact Hi)).
- all: try (rewrite Hi /isPRE /Kind_of_req //= in Hp; contradict Hp; by case (r0.(Kind))).
- rewrite Hi //= Hs //= Hact Hcas Hwait //=. }
- Qed.
+ destruct (Default_arbitrate (ta + d)).(Implementation_State) eqn:Hs;
+ [ rewrite /FIFO_request //= in IH | ].
+ apply FIFO_add_counter with (c := OCycle0) (d := d) in Hrun as H. destruct H as [Hrun' Hc'].
+ 3: apply /eqP; exact Hc.
+ 2: rewrite /OCycle0 //= add0n.
+ rewrite /OCycle0 //= add0n in Hc'.
+ rewrite addnS; simpl; rewrite /Next_state Hs //=.
+ destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl;
+ try by rewrite /FIFO_request in IH;
+ destruct r eqn:HPP; simpl.
+ rewrite Hs /FIFO_counter in Hc'; move: Hwait => /eqP Hwait; rewrite Hc' in Hwait; rewrite Hwait prednK in Hd;
+ try exact WAIT_pos; by rewrite ltnn in Hd.
+ Qed.
+
+ Lemma Request_starts_running ra ta:
+ let S := (Default_arbitrate ta).(Implementation_State) in
+ isRUNNING (S) ->
+ FIFO_counter (S) == WAIT.-1 ->
+ ra \in FIFO_pending (S) ->
+ index ra (FIFO_pending S) = 0 ->
+ (FIFO_request (Default_arbitrate ta.+1).(Implementation_State) == Some ra) &&
+ (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0) &&
+ (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)).
+ Proof.
+ intros S Hrun Hc HP Hi.
+ unfold S in *; clear S.
+ destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
+ 1: discriminate Hrun.
+ simpl; rewrite /Next_state Hs.
+ destruct (nat_of_ord c == OACT_date) eqn:Hact, (nat_of_ord c == OCAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl.
+ all: rewrite /FIFO_counter in Hc.
+ all: try by rewrite Hc in Hwait.
+ 4: destruct r eqn:HPP; simpl.
+ 4: { discriminate HP. }
+ 4: {
+ destruct (r1 == ra) eqn:Heq.
+ { move: Heq => /eqP Heq. by rewrite Heq eq_refl. }
+ { simpl in Hi. rewrite Heq in Hi. discriminate Hi. }
+ }
+ 1,2: move: Hc => /eqP Hc; rewrite Hc in Hact; by rewrite FIFO_wait_neq_act in Hact.
+ move: Hc => /eqP Hc; rewrite Hc in Hcas; by rewrite FIFO_wait_neq_cas in Hcas.
+ Qed.
- Lemma FIFO_CAS_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isCAS cmd ->
- (FIFO_counter (Default_arbitrate cmd.(CDate)).(Implementation_State)) = Next_cycle OCAS_date /\
- (isRUNNING (Default_arbitrate cmd.(CDate)).(Implementation_State)) /\
- (FIFO_request (Default_arbitrate cmd.(CDate)).(Implementation_State) == Some cmd.(Request)).
+ Lemma Request_PRE_bounded t ra:
+ isRUNNING (# t).(Implementation_State) ->
+ FIFO_request (# t).(Implementation_State) == Some ra ->
+ (PRE_of_req ra (Slot_start t)) \in (Default_arbitrate (Slot_start t)).(Arbiter_Commands).
Proof.
- induction t.
- { done. }
- intros Hi Hp; simpl in *.
- unfold Next_state in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs; simpl in Hi.
- { destruct r; simpl in Hi.
- all: rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi].
- all: try (contradict Hp; by rewrite Hi).
- all: try (apply IHt in Hi; (exact Hp || exact Hi)). }
- { destruct c; simpl in *; destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl in Hi.
+ intros Hrun Hreq.
+ induction t; [ by simpl in Hrun | ].
+ rewrite /Slot_start; simpl in *; unfold Next_state in *; simpl in *.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
+ { destruct r eqn:HPP; simpl in *; [ by simpl in Hrun | ].
+ clear Hrun IHt.
+ rewrite /Next_state Hs //= subn0 in_cons /PRE_of_req.
+ rewrite inj_eq in Hreq ; [ | exact ssrfun.Some_inj ].
+ move: Hreq => /eqP Hreq; by rewrite Hreq eq_refl orTb.
+ }
+ { destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl in *.
7: destruct r eqn:HPP.
- all: rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi].
- all: try (apply IHt in Hi; (exact Hp || exact Hi)).
- all: try (contradict Hp; by rewrite Hi).
- all: rewrite Hi //= Hs //= Hact Hcas //=; move: Hcas => /eqP Hcas; unfold Next_cycle; simpl; by rewrite Hcas eq_refl. }
- Qed.
-
- Lemma FIFO_l_helper_4 ta tb cb:
- ta < tb ->
- FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) = 0 ->
- FIFO_counter (Default_arbitrate tb).(Implementation_State) = cb ->
- cb > 0 ->
- ta.+1 < tb.
- Proof.
- intros Hlt Hca Hcb Hcb_pos.
- rewrite ltn_neqAle Hlt andbT.
- destruct (_ == tb) eqn:He.
- 2: done.
- move: He => /eqP He.
- rewrite -He in Hcb.
- rewrite Hcb in Hca.
- contradict Hca.
- apply /eqP.
- rewrite neq_ltn; apply /orP; right; exact Hcb_pos.
- Qed.
-
- Lemma FIFO_l_helper_3 ta tb d (cb : Counter_t) :
- isRUNNING (Default_arbitrate ta).(Implementation_State) ->
- FIFO_counter (Default_arbitrate ta).(Implementation_State) = 0 ->
- FIFO_counter (Default_arbitrate tb).(Implementation_State) = cb ->
- d < cb -> ta < tb -> ta + d < tb.
+ 7: by simpl in Hrun.
+ 7: {
+ simpl; rewrite /Next_state Hs Hact Hcas Hwait //=.
+ rewrite in_cons subn0; apply /orP; left.
+ simpl in Hreq; rewrite /PRE_of_req.
+ rewrite inj_eq in Hreq; [ | exact ssrfun.Some_inj ].
+ move: Hreq => /eqP Hreq; by rewrite Hreq.
+ }
+ all:
+ apply IHt in Hreq as IH;
+ try trivial; clear IHt;
+ rewrite /Slot_start Hs in IH;
+ try (rewrite {1}/Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc);
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e;
+ try (rewrite {1}/Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc);
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e;
+ try (rewrite subSS; by exact IH);
+ try (contradict x; by apply Bool.not_true_iff_false);
+ try (contradict x0; by apply Bool.not_true_iff_false);
+ try (move: Hact => /eqP Hact; by rewrite Hact FIFO_WAIT_GT_SACT in x);
+ try (move: Hcas => /eqP Hcas; by rewrite Hcas FIFO_WAIT_GT_SCAS in x).
+ clear Hc0 Hc1 x0.
+ rewrite ltnNge in x; apply negbFE in x.
+ rewrite leq_eqVlt in x; move: x => /orP [x | x]; [ lia | ].
+ destruct c; simpl in *; contradict x; lia.
+ }
+ Qed.
+
+ Lemma Request_ACT_bounded t ra:
+ isRUNNING (Default_arbitrate t).(Implementation_State) ->
+ FIFO_request (Default_arbitrate t).(Implementation_State) == Some ra ->
+ let tact := (Slot_start t + Next_cycle OACT_date) in
+ (ACT_of_req ra tact) \in (Default_arbitrate tact).(Arbiter_Commands).
Proof.
- intros Hrun_a Hca Hcb Hd Hlt.
- induction d.
- { by rewrite addn0. }
- apply ltn_trans with (m:= d) in Hd as Hd'.
- 2: apply ltnSn.
- apply IHd in Hd' as H.
- rewrite addnS ltn_neqAle H andbT.
- destruct ( _ == tb) eqn:He.
- 2: done.
- move: He => /eqP He.
- apply FIFO_add_counter with (d := d.+1) (c := Ordinal WAIT_pos) in Hrun_a as HH.
- 3: { simpl; exact Hca. }
- 2: { simpl; rewrite add0n. apply ltn_trans with (n := cb); (exact Hd || by destruct cb). }
- destruct HH as [Hrun_adp1 Hc_adp1]; simpl in Hc_adp1.
- rewrite -He in Hcb.
- rewrite add0n addnS in Hc_adp1.
- rewrite Hc_adp1 in Hcb.
- contradict Hcb; apply /eqP.
- rewrite neq_ltn; apply /orP; left; exact Hd.
- Qed.
+ intros Hrun Hreq; simpl.
+ induction t.
+ { by simpl in Hrun. }
+ rewrite /Slot_start; simpl in *; unfold Next_state in *; simpl in *.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
+ { destruct r eqn:HPP; simpl in *.
+ { done. }
+ { clear Hrun IHt.
+ rewrite /Next_state //=.
+ assert (isIDLE (Default_arbitrate t).(Implementation_State)) as Hidle.
+ { by rewrite Hs. }
+ apply Request_starts_idle with (ra := r0) in Hidle.
+ 3,2: rewrite Hs /FIFO_pending; (by apply index_head || by apply mem_head).
+ rename Hidle into H; move: H => /andP [/andP [Hreq' Hc'] Hrun']; move: Hc' => /eqP Hc'.
+ apply FIFO_add_counter with (d := ACT_date) in Hc' as H. destruct H as [Hrun'' Hc''].
+ 3: rewrite /OCycle0 add0n //=; specialize FIFO_WAIT_GT_SACT; by apply ltnW.
+ 2: done.
+ apply Request_running_in_slot with (d := ACT_date) in Hreq' as Hreq''.
+ 3: specialize FIFO_WAIT_GT_SACT; by apply ltnW.
+ 2: by apply /eqP.
+ rewrite -addn1 -addnA [1 + _]addnC addn1 in Hc'',Hrun'', Hreq''.
+ rewrite FIFO_nextcycle_act_eq_actS.
+ destruct (Default_arbitrate (t + ACT_date.+1)).(Implementation_State) eqn:Hs_act.
+ { by simpl in Hrun''. }
+ clear Hrun''; rewrite /FIFO_counter /OCycle0 add0n in Hc''.
+ assert ((ACT_date == ACT_date) = true).
+ { by rewrite eq_refl. }
+ rewrite Hc'' H //= in_cons /ACT_of_req subn0.
+ rewrite -addn1 -addnA [1 + _]addnC addn1 addnS.
+ rewrite /FIFO_request inj_eq in Hreq''.
+ 2: exact ssrfun.Some_inj.
+ move: Hreq'' => /eqP Hreq''; rewrite -Hreq'' in Hreq.
+ rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
+ 2: exact ssrfun.Some_inj.
+ by rewrite Hreq eq_refl orTb. }}
+ { destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl in *.
+ all: rewrite FIFO_nextcycle_act_eq_actS.
+ 7: destruct r eqn:HPP; simpl.
+ 7: discriminate Hrun.
+ 7: {
+ simpl in *; clear IHt Hrun; rewrite /Next_state.
+ assert (isRUNNING (Default_arbitrate t).(Implementation_State)).
+ { by rewrite Hs. }
+ rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
+ 2: exact ssrfun.Some_inj.
+ apply Request_starts_running with (ra := ra) in H. move: H => /andP [/andP [Hreq' Hc']Hrun'].
+ 4: rewrite Hs /FIFO_pending Hreq; apply index_head.
+ 3: rewrite /FIFO_pending Hs Hreq; apply mem_head.
+ 2: move: Hwait => /eqP Hwait; by rewrite /FIFO_counter Hs Hwait eq_refl.
+ move: Hc' => /eqP Hc'.
+ apply FIFO_add_counter with (d := ACT_date) in Hc' as H.
+ 3: rewrite /OCycle0 add0n //=; specialize FIFO_WAIT_GT_SACT; by apply ltnW.
+ 2: done.
+ apply Request_running_in_slot with (d := ACT_date) in Hreq' as Hreq''.
+ 3: specialize FIFO_WAIT_GT_SACT; by apply ltnW.
+ 2: by apply /eqP.
+ destruct H as [Hrun'' Hc''].
+ rewrite -addn1 -addnA [1 + _]addnC addn1 in Hc'',Hrun'', Hreq''.
+ destruct (Default_arbitrate (t + ACT_date.+1)).(Implementation_State) eqn:Hs_act.
+ { by simpl in Hrun''. }
+ clear Hrun''; rewrite /FIFO_counter /OCycle0 add0n in Hc''.
+ assert ((ACT_date == ACT_date) = true).
+ { by rewrite eq_refl. }
+ rewrite Hc'' H //= in_cons /ACT_of_req subn0.
+ rewrite -addn1 -addnA [1 + _]addnC addn1 addnS.
+ rewrite /FIFO_request inj_eq in Hreq''.
+ 2: exact ssrfun.Some_inj.
+ move: Hreq'' => /eqP Hreq''; by rewrite -Hreq'' eq_refl orTb.
+ }
+ all: rewrite /Slot_start Hs in IHt.
+ all: try (rewrite {1}/Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc).
+ all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
+ all: try (apply IHt in Hreq); try done.
+ all: try (rewrite {1}/Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc).
+ all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
+ all: try (contradict x; by apply Bool.not_true_iff_false).
+ all: try (contradict x0; by apply Bool.not_true_iff_false); try (clear x0 Hc0 Hc1).
+ all: assert (t.+1 - c.+1 + ACT_date.+1 = t - c + Next_cycle OACT_date) as H.
+ all: try (rewrite -FIFO_nextcycle_act_eq_actS -addn1 -[c.+1]addn1 subnDA -subnAC subn1 addn1 -pred_Sn; reflexivity).
+ all: try (by rewrite H); clear H.
+ all: try (move: Hact => /eqP Hact; rewrite Hact in x; contradict x;
+ apply Bool.not_false_iff_true; by rewrite FIFO_WAIT_GT_SACT).
+ all: try (move: Hcas => /eqP Hcas; rewrite Hcas in x; contradict x;
+ apply Bool.not_false_iff_true; by rewrite FIFO_WAIT_GT_SCAS).
+ clear Hrun IHt.
+ rewrite ltnNge in x; apply negbFE in x.
+ rewrite leq_eqVlt in x; move: x => /orP [x | x].
+ { move: Hwait => /eqP Hwait; contradict Hwait. apply eq_add_S; rewrite prednK.
+ 2: exact WAIT_pos.
+ move: x => /eqP x.
+ by apply Logic.eq_sym. }
+ { destruct c; simpl in *; contradict x.
+ apply /negP.
+ by rewrite -leqNgt. } }
+ Qed.
- Lemma FIFO_running ta tb (d : Counter_t):
- isIDLE (Default_arbitrate ta).(Implementation_State)
- -> isRUNNING (Default_arbitrate tb).(Implementation_State)
- -> ta < tb
- -> FIFO_counter (Default_arbitrate ta).(Implementation_State) = 0
- -> ((ta + d < tb) && (isRUNNING (Default_arbitrate (ta + d)).(Implementation_State) == false))
- \/ (exists r, (ta + r <= tb) && (r <= d) && (isRUNNING (Default_arbitrate (ta + r)).(Implementation_State))
- && (FIFO_counter ((Default_arbitrate (ta + r)).(Implementation_State)) == 0)).
+ Theorem Cmds_ACT_ok t a b:
+ a \in (# t).(Arbiter_Commands) -> b \in (# t).(Arbiter_Commands) ->
+ isACT a \/ isCAS a -> isACT b -> Same_Bank a b -> Before a b ->
+ exists c, (c \in (Default_arbitrate t).(Arbiter_Commands)) && isPRE c && Same_Bank b c && Same_Bank a c && After c a && Before c b.
Proof.
- intros Hidle_a Hrun_b Hlt Hc.
- destruct d as [d Hd].
- induction d.
- { apply isIDLE_notRunning in Hidle_a; left; simpl; by rewrite addn0 Hlt andTb Hidle_a. }
- apply ltn_trans with (m := d) in Hd as Hd'.
- 2: apply ltnSn.
- specialize IHd with (Hd := Hd') as [IH | IH]; simpl in IH.
- { (* we're still idle after D cycles, next cycle could be IDLE, RUNNING or REFRESH *)
- move : IH => /andP [IH Hrun_a'].
- rewrite leq_eqVlt in IH; move : IH => /orP [/eqP IH | IH].
- { (* tb is the cycle after *)
- right. simpl. subst tb. exists (d.+1).
- rewrite ltnSn andbT addnS Hrun_b andbT leqnn andTb /FIFO_counter.
- rewrite /isRUNNING //= /Next_state in Hrun_b Hrun_a' *.
- destruct ((Default_arbitrate (ta + d)).(Implementation_State)) eqn:HS, (r) eqn:HP; simpl.
- all: done.
- }
- { (* now tb is in the future *)
- simpl; rewrite /isIDLE in Hrun_a'.
- destruct ((Default_arbitrate (ta + d)).(Implementation_State)) eqn:HS; simpl.
- { (* from IDLE to REFRESH 1 *)
- rewrite addnS IH andTb //= /Next_state HS.
- destruct r; simpl.
- { by left. }
- right; exists (d.+1); apply ltnW in IH.
- rewrite addnS IH andTb ltnSn andTb.
- by rewrite /isRUNNING /FIFO_counter //= HS.
+ intros Ha Hb iA iAb SB aBb.
+ apply FIFO_ACT_date in Hb as H. destruct H as [Hcb [Hrun_b Hreq_b]].
+ all: try done.
+ destruct (Default_arbitrate b.(CDate)).(Implementation_State) eqn:Hsb.
+ 1: by simpl in Hrun_b.
+ rewrite -Hsb in Hreq_b.
+ unfold get_req in Hreq_b; destruct b.(CKind) eqn:H_kind;
+ try (by unfold isACT in iAb; rewrite H_kind in iAb).
+ apply Request_PRE_bounded in Hreq_b.
+ 2: by rewrite -Hsb in Hrun_b.
+ rewrite /Slot_start Hsb in Hreq_b.
+ exists (PRE_of_req r1 (b.(CDate) - c)).
+ rewrite /Same_Bank in SB; move: SB => /eqP SB.
+ rewrite /isPRE /Same_Bank //= andbT SB /PRE_of_req /get_bank H_kind //= eq_refl !andbT.
+ rewrite /Before /After.
+ (* Solving Before c b*)
+ apply /andP; split.
+ 2: {
+ rewrite /FIFO_counter in Hcb; rewrite Hcb.
+ rewrite ltn_subLR.
+ 2: { rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b; rewrite -Hcb.
+ rewrite /FIFO_counter Hsb in Hrun_b. by rewrite leq_eqVlt Hrun_b orbT.
+ }
+ rewrite addnC.
+ apply nat_ltn_add; by rewrite FIFO_nextcycle_act_eq_actS.
+ }
+
+ (* Solving ~~ Before_at a c*)
+ apply /andP; split.
+ 2:{ destruct iA as [iAa | iCa].
+ { apply FIFO_ACT_date in Ha as H. destruct H as [Hca [Hrun_a Hreq_a]].
+ 2: done.
+ rewrite -Hsb in Hcb.
+ specialize FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) as HH; apply HH in Hrun_a as Hlt.
+ all: try (done || by rewrite -Hsb in Hrun_b).
+ clear HH. rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP H0 | H1].
+ { rewrite -H0 -addnBA.
+ 2: by destruct c; simpl; rewrite leq_eqVlt i orbT.
+ apply nat_ltn_add; rewrite subn_gt0; destruct c; simpl; exact i. }
+ { apply ltn_trans with (n := b.(CDate) - WAIT).
+ 2: {
+ apply ltn_sub2l.
+ 2: destruct c; simpl; exact i.
+ by rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b; rewrite /FIFO_counter Hsb in Hrun_b.
}
- by contradict Hrun_a'.
+ rewrite ltn_subRL addnC; exact H1.
}
}
- right. destruct IH as [r H]; move : H => /andP [/andP [/andP [Hlt' Hrd ] Hrun_a'] Hc'].
- exists (r); simpl.
- rewrite Hlt' andTb; apply /andP; split.
- { apply /andP. split.
- { apply leq_trans with (n := d); (exact Hrd || apply ltnW, ltnSn). }
- exact Hrun_a'.
- }
- exact Hc'.
+ { apply FIFO_CAS_date in Ha as H. destruct H as [Hca [Hrun_a Hreq_a]].
+ 2: done.
+ rewrite -Hsb in Hcb.
+ apply FIFO_add_counter with (d := Next_cycle OCAS_date - Next_cycle OACT_date) in Hcb as H.
+ 3: { rewrite subnKC. by rewrite FIFO_next_cycle_cas_eq_casS FIFO_WAIT_GT_SCAS.
+ rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite /CAS_date /ACT_date -addnS. by apply nat_ltn_add. }
+ 2: by rewrite -Hsb in Hrun_b.
+ destruct H as [Hrun_b' Hcb'].
+ set (d := Next_cycle OCAS_date - Next_cycle OACT_date); fold d in Hrun_b',Hcb'.
+ assert (Next_cycle OACT_date + d = Next_cycle OCAS_date).
+ { unfold d; rewrite subnKC. reflexivity.
+ rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS /CAS_date /ACT_date -addnS.
+ by apply nat_ltn_add. }
+ rewrite H in Hcb'.
+ specialize FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate) + d) (c := Next_cycle OCAS_date) as HH.
+ apply HH in Hrun_a as Hlt; clear HH; try done.
+ 2 : {
+ unfold Before in aBb; apply ltn_trans with (n := b.(CDate)).
+ exact aBb. apply nat_ltn_add. unfold d.
+ rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS /CAS_date /ACT_date prednK.
+ 2: by rewrite lt0n T_RP_pos.
+ rewrite subSn; [ trivial | specialize T_RCD_pos; lia ].
+ }
+ assert ((a.(CDate) < b.(CDate) - c) == (a.(CDate) + WAIT < b.(CDate) - c + WAIT));
+ [ apply /eqP; by rewrite ltn_add2r | ].
+ move: H0 => /eqP H0; rewrite H0; clear H0.
+ rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP Hlt | Hlt].
+ { rewrite Hlt addnBAC.
+ 2: { rewrite -Hsb in Hrun_b. apply Date_gt_counter in Hrun_b.
+ rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT.
+ }
+ rewrite -addnBA.
+ 2: by destruct c; simpl; rewrite leq_eqVlt i orbT.
+ rewrite ltn_add2l ltn_subRL.
+ rewrite /FIFO_counter Hsb in Hcb; rewrite Hcb; unfold d.
+ rewrite subnKC.
+ 2: { rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite /CAS_date /ACT_date -addnS. apply nat_ltnn_add. by specialize T_RCD_GT_ONE.
+ }
+ by rewrite FIFO_next_cycle_cas_eq_casS FIFO_WAIT_GT_SCAS. }
+ { apply ltn_trans with (n := b.(CDate) + d). exact Hlt.
+ rewrite addnBAC.
+ 2: { rewrite -Hsb in Hrun_b. apply Date_gt_counter in Hrun_b.
+ rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT.
+ }
+ rewrite -addnBA.
+ 2: by destruct c; simpl; rewrite leq_eqVlt i orbT.
+ rewrite ltn_add2l ltn_subRL.
+ rewrite /FIFO_counter Hsb in Hcb; rewrite Hcb; unfold d.
+ rewrite subnKC.
+ 2: { rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite /CAS_date /ACT_date -addnS. apply nat_ltnn_add. by specialize T_RCD_GT_ONE.
+ }
+ by rewrite FIFO_next_cycle_cas_eq_casS FIFO_WAIT_GT_SCAS. }
+ }
+ }
+ apply FIFO_in_the_past with (t := b.(CDate)); [ by apply Cmd_in_trace | ].
+ apply FIFO_in_the_past with (t := b.(CDate) - c); [ by apply leq_subr | assumption ].
Qed.
- Lemma FIFO_running_at_zero_lt_at_c t t' d:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- t < t' -> FIFO_counter (Default_arbitrate t).(Implementation_State) = 0 ->
- d < FIFO_counter (Default_arbitrate t').(Implementation_State) ->
- t + d < t'.
+ Lemma Request_exists b c0 r r0 :
+ isCAS b ->
+ # (b.(CDate)).(Implementation_State) = RUNNING c0 r r0 ->
+ FIFO_request # (b.(CDate)).(Implementation_State) == get_req b ->
+ FIFO_request # (b.(CDate)).(Implementation_State) == Some r0.
+ Proof.
+ intros iCb H Hreq_b.
+ unfold get_req, FIFO_request in *; rewrite H in Hreq_b.
+ destruct b.(CKind) eqn:Hkind;
+ try (by unfold isCAS,isCRD,isCWR in iCb; rewrite Hkind in iCb);
+ by rewrite H eq_refl.
+ Qed.
+
+ Theorem Cmds_row_ok t b c:
+ b \in (# t).(Arbiter_Commands) -> c \in (# t).(Arbiter_Commands) ->
+ isCAS b -> isPRE c -> Same_Bank b c -> Before c b ->
+ exists a, (a \in (Default_arbitrate t).(Arbiter_Commands))
+ && isACT a && Same_Row a b && After a c && Before a b.
Proof.
- intros Hrun Hlt HcZ Hd.
- induction d.
- - by rewrite addn0.
- - apply ltn_trans with (m := d) in Hd as IH.
- 2: apply ltnSn.
- apply IHd in IH; clear IHd.
- rewrite addnS ltn_neqAle IH andbT.
- specialize (FIFO_counter_lt_WAIT t') as HW.
- destruct ((t + d).+1 == t') eqn:H.
- - apply FIFO_add_counter with (c := OCycle0) (d := d.+1) in Hrun as [_ HcD].
- 3: exact HcZ.
- 2: rewrite add0n; apply ltn_trans with (n := FIFO_counter (Default_arbitrate t').(Implementation_State)); exact Hd || exact HW.
- move : H => /eqP H; subst.
- contradict Hd.
- by rewrite -addnS HcD add0n ltnn.
- - trivial.
- Qed.
-
+ intros Hb Hc iCb iPc SB cBb.
+ apply FIFO_CAS_date in Hb as H; [ | done ].
+ destruct H as [Hcb [Hrun_b Hreq_b]].
- (* ------------------------------------------------------------------ *)
- (* --------------------- TIMING PROOFS ------------------------------ *)
- (* ------------------------------------------------------------------ *)
+ destruct # (b.(CDate)).(Implementation_State) eqn:Hsb; [ done | ].
- Theorem Cmds_T_RCD_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_CAS a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RCD.
- Proof.
- intros Ha Hb AtC SB aBb; rewrite /Apart_at_least.
- move : AtC => /andP [Aa Cb].
- apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]].
- 2: exact Aa; clear Aa.
- apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]].
- 2: exact Cb; clear Cb.
- set (d := Next_cycle OCAS_date - Next_cycle OACT_date).
- apply FIFO_add_counter with (c := Next_cycle OACT_date) (d := d) in Hrun_a as H.
- 3: exact Hc_a.
- 2: {
- unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite subnKC. exact FIFO_WAIT_GT_CASp1.
- rewrite /CAS_date /ACT_date -addnS. apply nat_ltnn_add. by specialize T_RCD_GT_ONE. }
- destruct H as [Hrun_a' Hc_a'].
- unfold d in Hc_a'; rewrite subnKC in Hc_a'.
- 2: {
- rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite /CAS_date /ACT_date -addnS. apply nat_ltnn_add. by specialize T_RCD_GT_ONE. }
- apply FIFO_l_eq_bound_or with (ta := a.(CDate) + d) (c := Next_cycle OCAS_date) in Hrun_b as H.
- 2-4: done.
- destruct H as [H0 | [H1 | H2]].
- { rewrite -H0 leq_add2l. unfold d.
- rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS /CAS_date /ACT_date.
- rewrite prednK.
- 2: { rewrite lt0n. exact T_RP_pos. }
- rewrite -addnS addnC -addn1. rewrite -addnA [1 + T_RP.-1]addnC addn1 prednK.
- 2: { rewrite lt0n. exact T_RP_pos. }
- rewrite -addnBA.
- 2: by rewrite leqnn.
- 1: apply leq_addr. }
- { unfold d in H1; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS in H1.
- apply leq_trans with (m := a.(CDate) + T_RCD) in H1.
- exact H1.
- rewrite -addnA leq_add2l /CAS_date /ACT_date prednK.
- rewrite [T_RP.-1 + _]addnC -addnS prednK.
- 2,3: rewrite lt0n; exact T_RP_pos.
- rewrite addnBAC.
- 2: by rewrite addnC leq_addr.
- rewrite leq_subRL.
- 2: by rewrite [T_RCD + T_RP]addnC -addnA leq_addr.
- by rewrite addnC leq_addr. }
- { unfold d in H2; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS in H2.
- contradict H2. apply /negP. rewrite -ltnNge addnC -ltn_subRL.
- unfold Before in aBb. apply ltn_trans with (n := b.(CDate)).
- exact aBb.
- rewrite subnBA.
- 2: { rewrite /CAS_date /ACT_date -addnS. by apply nat_ltn_add. }
- rewrite ltn_subRL addnC -addnA ltn_add2l.
- rewrite /CAS_date /ACT_date prednK.
- rewrite addnC -addnS prednK.
- 3,2: rewrite lt0n; exact T_RP_pos.
- rewrite ltn_add2r.
- apply nat_add_ltn with (m := T_RP.-1).
- { rewrite ltn_predRL. exact T_RP_GT_ONE. }
- specialize WAIT_CAS; by rewrite /CAS_date /ACT_date. }
- Qed.
+ apply Request_exists in Hsb as H; try assumption; [ | by rewrite <- Hsb in Hreq_b].
- Theorem Cmds_T_RP_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- PRE_to_ACT a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RP.
- Proof.
- intros Ha Hb pTa sB aBb.
- rewrite /PRE_to_ACT in pTa; move: pTa => /andP [iPa iAb].
- apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]].
- 2: exact iAb.
- apply FIFO_PRE_date in Ha as [Hc_a [Hrun_a _]].
- 2: exact iPa.
- unfold Apart_at_least.
- apply FIFO_running_at_zero_lt_at_c with (t':= b.(CDate)) (d := ACT_date) in Hc_a as H.
- 4: rewrite Hc_b; by rewrite FIFO_nextcycle_act_eq_actS.
- 3: by unfold Before in aBb.
- 2: exact Hrun_a.
- unfold ACT_date in H.
- rewrite -addnS prednK in H.
- 2: specialize T_RP_GT_ONE as H; apply ltn_trans with (n := 1); done || exact H.
- exact H.
- Qed.
+ rewrite -Hsb in Hreq_b.
- Theorem Cmds_T_RC_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RC.
- Proof.
- intros Ha Hb AtA SB aBb; rewrite /Apart_at_least.
- move : AtA => /andP [Aa Ab].
- apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]].
- 2: exact Aa; clear Aa.
- apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]].
- 2: exact Ab; clear Ab.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt.
- 2-5: done.
- apply leq_trans with (n := (a.(CDate) + WAIT)).
- 2: exact Hlt.
- rewrite leq_add2l.
- by rewrite leq_eqVlt RC_WAIT orbT.
- Qed.
+ apply Request_ACT_bounded in H as H'; try (by rewrite -Hsb in Hrun_b);
+ rewrite /Slot_start Hsb in H'.
+
+ exists (ACT_of_req r0 (b.(CDate) - c0 + Next_cycle OACT_date)).
+
+ rewrite /Same_Bank in SB; move: SB => /eqP SB;
+ rewrite /isACT //= andbT /Before /After //= /Same_Row /get_row /ACT_of_req //=.
+ apply /andP; split; [ apply /andP; split; [ apply /andP; split | ] | ].
+ 2: {
+ unfold FIFO_request, get_req in *.
+ destruct b.(CKind) eqn:Hkind;
+ try (by unfold isCAS,isCRD,isCWR in iCb; rewrite Hkind in iCb);
+ rewrite Hsb in H,Hreq_b; rewrite inj_eq; try (exact ssrfun.Some_inj);
+ rewrite inj_eq in Hreq_b; try (exact ssrfun.Some_inj); move: Hreq_b => /eqP Hreq_b;
+ subst r0; by rewrite eq_refl.
+ }
+
+ 3: {
+ rewrite /FIFO_counter in Hcb; rewrite Hcb FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS;
+ rewrite -Hsb in Hrun_b;
+ rewrite -subnA.
+ 3 : {
+ clear H.
+ apply Date_gt_counter in Hrun_b as H; rewrite Hsb /FIFO_counter Hcb FIFO_next_cycle_cas_eq_casS in H;
+ apply ltn_trans with (m := CAS_date) in H; [ exact H | done ].
+ }
+ 2 : {
+ rewrite /CAS_date /ACT_date -addnS; by apply nat_ltn_add.
+ }
+ rewrite ltn_subrL;
+ apply FIFO_date_gt_0 in Hb; rewrite subn_gt0 Hb andbT -addn1 -[CAS_date.+1]addn1 leq_add2r;
+ rewrite /CAS_date /ACT_date; apply nat_ltn_add; by rewrite lt0n T_RCD_pos.
+ }
- Theorem Cmds_T_RAS_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_PRE a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RAS.
- Proof.
- intros Ha Hb Hty SB aBb; rewrite /Apart_at_least.
- rewrite /ACT_to_PRE in Hty; move : Hty => /andP [iAa iPb].
- apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]].
- apply FIFO_PRE_date in Hb as [Hc_b [Hrun_b _]].
- 3,2: done.
- clear iAa iPb.
- apply FIFO_add_counter with (d := Next_cycle OACT_date) in Hc_b as H. destruct H as [Hrun_b' Hc_b'].
- 3: by rewrite /OCycle0 add0n FIFO_nextcycle_act_eq_actS FIFO_WAIT_GT_ACTp1.
- 2: done.
- set (d := Next_cycle OACT_date); fold d in Hc_b', Hrun_b'; rewrite /OCycle0 add0n in Hc_b'.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (c := d) (tb := b.(CDate) + d) in Hrun_a as Hlt.
- all: try done.
- 2: { rewrite /Before in aBb. apply ltn_trans with (p := b.(CDate) + d) in aBb. exact aBb.
- apply nat_ltn_add; unfold d; by rewrite FIFO_nextcycle_act_eq_actS.
- }
- rewrite [_ + d]addnC -leq_subLR in Hlt; unfold d in Hlt.
- apply leq_trans with (m := a.(CDate) + T_RAS) in Hlt. exact Hlt.
- rewrite -addnBA.
- 2: rewrite FIFO_nextcycle_act_eq_actS; specialize FIFO_WAIT_GT_ACTp1; apply ltnW.
- rewrite leq_add2l leq_subRL.
- 2: rewrite FIFO_nextcycle_act_eq_actS; specialize FIFO_WAIT_GT_ACTp1; apply ltnW.
- rewrite FIFO_nextcycle_act_eq_actS /ACT_date prednK.
- 2: by rewrite lt0n T_RP_pos.
- by rewrite leq_eqVlt RAS_WAIT orbT.
- Qed.
-
- Theorem Cmds_T_RTP_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_PRE a b -> Same_Bank a b -> Before a b -> Apart_at_least a b T_RTP.
- Proof.
- intros Ha Hb Htype sB aBb.
- rewrite /CRD_to_PRE in Htype; move: Htype => /andP [iCa iPb].
- apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
- 2: unfold isCAS; unfold isCRD in iCa; apply /orP; left; exact iCa.
- apply FIFO_PRE_date in Hb as [Hc_b [Hrun_b _]].
- 2: exact iPb.
- unfold Apart_at_least.
- apply FIFO_add_counter with (c := OCycle0) (d := CAS_date.+1) in Hrun_b as [Hrun_b' Hc_b'].
- 3: exact Hc_b.
- 2: simpl; rewrite add0n; exact FIFO_WAIT_GT_CASp1.
- rewrite -{2}FIFO_next_cycle_cas_eq_casS in Hc_b'; simpl in Hc_b'; rewrite add0n in Hc_b'.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate) + CAS_date.+1) (c := Next_cycle OCAS_date) in Hrun_a as H.
- 5: exact Hc_b'.
- 4: exact Hc_a.
- 3: unfold Before in aBb; apply ltn_trans with (p := b.(CDate) + CAS_date.+1) in aBb; exact aBb || (by rewrite nat_ltn_add).
- 2: exact Hrun_b'.
- rewrite [b.(CDate) + _]addnC -leq_subLR in H.
- apply leq_trans with (n := a.(CDate) + WAIT - CAS_date.+1).
- 2: exact H.
- rewrite -addnBA.
- 2: exact WAIT_CAS.
- rewrite leq_add2l leq_subRL.
- 2: exact WAIT_CAS.
- rewrite addnC addnS addnC.
- exact WAIT_END_READ.
- Qed.
-
- Theorem Cmds_T_WTP_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CWR_to_PRE a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b (T_WR + T_WL + T_BURST).
- Proof.
- intros Ha Hb Htype sB aBb.
- rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iCa iPb].
- apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
- 2: { unfold isCAS. unfold isCWR in iCa. apply /orP. right. exact iCa. }
- apply FIFO_PRE_date in Hb as [Hc_b [Hrun_b _]].
- 2: exact iPb.
- unfold Apart_at_least.
- apply FIFO_add_counter with (c := OCycle0) (d := CAS_date.+1) in Hrun_b as [Hrun_b' Hc_b'].
- 3: exact Hc_b.
- 2: simpl; rewrite add0n; exact FIFO_WAIT_GT_CASp1.
- rewrite -{2}FIFO_next_cycle_cas_eq_casS in Hc_b'; simpl in Hc_b'; rewrite add0n in Hc_b'.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate) + CAS_date.+1) (c := Next_cycle OCAS_date) in Hrun_a as H.
- all: try done.
- 2: unfold Before in aBb; apply ltn_trans with (p := b.(CDate) + CAS_date.+1) in aBb; exact aBb || (by rewrite nat_ltn_add).
- rewrite [b.(CDate) + _]addnC -leq_subLR in H.
- apply leq_trans with (n := a.(CDate) + WAIT - CAS_date.+1).
- 2: exact H.
- rewrite -addnBA.
- 2: exact WAIT_CAS.
- rewrite leq_add2l leq_subRL.
- 2: exact WAIT_CAS.
- rewrite addnC addnS addnC !addnA.
- exact WAIT_END_WRITE.
- Qed.
-
- Theorem Cmds_T_RtoW_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) ->
- b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_CWR a b -> Before a b ->
- Apart_at_least a b T_RTW.
- Proof.
- intros Ha Hb Htype aBb.
- rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iCRa iCWb].
- apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
- apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]].
- 3: by unfold isCAS; unfold isCRD in iCRa; rewrite iCRa orTb.
- 2: by unfold isCAS; unfold isCWR in iCWb; rewrite iCWb orbT.
- unfold Apart_at_least.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OCAS_date) in Hrun_a as H.
- 2-5: done.
- apply leq_trans with (n := a.(CDate) + WAIT).
- 2: exact H.
- by rewrite leq_add2l leq_eqVlt RTW_WAIT orbT.
- Qed.
-
- Theorem Cmds_T_WtoR_SBG_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) ->
- b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CWR_to_CRD a b -> Before a b -> Same_Bankgroup a b ->
- Apart_at_least a b (T_WTR_l + T_WL + T_BURST).
- Proof.
- intros Ha Hb Htype aBb sBG.
- rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iCWa iCRb].
- apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
- apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]].
- 3: by unfold isCAS; unfold isCWR in iCWa; rewrite iCWa orbT.
- 2: by unfold isCAS; unfold isCRD in iCRb; rewrite iCRb orTb.
- unfold Apart_at_least.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OCAS_date) in Hrun_a as H.
- 2-5: done.
- apply leq_trans with (n := a.(CDate) + WAIT).
- 2: exact H.
- by rewrite leq_add2l leq_eqVlt WTR_WAIT orbT.
- Qed.
-
- Theorem Cmds_T_WtoR_DBG_ok t:
- BANKGROUPS > 1 -> forall (a b : Command_t),
- a \in (Default_arbitrate t).(Arbiter_Commands) ->
- b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CWR_to_CRD a b -> Before a b -> ~~ Same_Bankgroup a b ->
- Apart_at_least a b (T_WTR_s + T_WL + T_BURST).
- Proof.
- intros H. specialize FIFO.DDR3 as Hbug. by rewrite Hbug in H.
- Qed.
-
- Theorem Cmds_T_CCD_SBG_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) ->
- b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b -> Same_Bankgroup a b ->
- Apart_at_least a b T_CCD_l.
- Proof.
- intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
- destruct Htype as [Htype | Htype].
- 2: unfold CWR_to_CWR in Htype; move: Htype => /andP [iWa iWb].
- 1: unfold CRD_to_CRD in Htype; move: Htype => /andP [iRa iRb].
- all: apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
- all: apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]].
- all: try (by unfold isCAS; unfold isCRD in iRb; rewrite iRb orTb).
- all: try (by unfold isCAS; unfold isCRD in iRa; rewrite iRa orTb).
- all: try (by unfold isCAS; unfold isCWR in iWb; rewrite iWb orbT).
- all: try (by unfold isCAS; unfold isCWR in iWa; rewrite iWa orbT).
- all: apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OCAS_date) in Hrun_a as H.
- all: try done.
- all: apply leq_trans with (n := a.(CDate) + WAIT).
- all: try exact H.
- all: by rewrite leq_add2l leq_eqVlt CCD_WAIT orbT.
- Qed.
-
- Theorem Cmds_T_CCD_DBG_ok t:
- BANKGROUPS > 1 -> forall a b,
- a \in (Default_arbitrate t).(Arbiter_Commands) ->
- b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b -> ~~ Same_Bankgroup a b ->
- Apart_at_least a b T_CCD_s.
- Proof.
- intros H. specialize FIFO.DDR3 as Hbug. by rewrite Hbug in H.
- Qed.
-
- Theorem Cmds_T_FAW_ok t a b c d:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- c \in (Default_arbitrate t).(Arbiter_Commands) -> d \in (Default_arbitrate t).(Arbiter_Commands) ->
- isACT a -> isACT b -> isACT c -> isACT d -> Diff_Bank [::a;b;c;d] ->
- Before a b -> Before b c -> Before c d ->
- Apart_at_least a d T_FAW.
- Proof.
- intros Ha Hb Hc Hd iAa iAb iAc iAd dB aBb bBc cBd.
- apply FIFO_date_gt_0 in Ha as Ha_pos.
- apply FIFO_date_gt_0 in Hb as Hb_pos.
- apply FIFO_date_gt_0 in Hc as Hc_pos.
- apply FIFO_date_gt_0 in Hd as Hd_pos.
- unfold Apart_at_least.
- apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]].
- apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]].
- apply FIFO_ACT_date in Hc as [Hc_c [Hrun_c _]].
- apply FIFO_ACT_date in Hd as [Hc_d [Hrun_d _]].
- all: try done.
- clear iAa iAb iAc iAd.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt_ab.
- all: try done.
- apply FIFO_l_eq_bound with (ta := b.(CDate)) (tb := c.(CDate)) (c := Next_cycle OACT_date) in Hrun_b as Hlt_bc.
- all: try done.
- apply FIFO_l_eq_bound with (ta := c.(CDate)) (tb := d.(CDate)) (c := Next_cycle OACT_date) in Hrun_c as Hlt_cd.
- all: try done.
- apply leq_trans with (p := c.(CDate) - WAIT) in Hlt_ab as Hlt_ac.
- 2: rewrite leq_psubRL; (rewrite -addnC; exact Hlt_bc) || exact Hb_pos.
- rewrite leq_psubRL addnC in Hlt_ac.
- 2: rewrite addn_gt0; apply /orP; left; exact WAIT_pos.
- apply leq_trans with (p := d.(CDate) - WAIT) in Hlt_ac as Hlt_ad.
- 2: rewrite leq_psubRL; (by rewrite -addnC) || exact Hc_pos.
- rewrite leq_psubRL addnC in Hlt_ad.
- 2: rewrite addn_gt0; apply /orP; left; exact WAIT_pos.
- apply leq_trans with (n := (a.(CDate) + WAIT + WAIT + WAIT)).
- 2: exact Hlt_ad.
- by rewrite -addnA -addnA leq_add2l addnA leq_eqVlt FAW_WAIT orbT.
- Qed.
-
- Theorem Cmds_T_RRD_SBG_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b -> Same_Bankgroup a b ->
- Apart_at_least a b T_RRD_l.
- Proof.
- intros Ha Hb AtA nSb aBb sBG; rewrite /Apart_at_least.
- move : AtA => /andP [Aa Ab].
- apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]].
- 2: exact Aa; clear Aa.
- apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]].
- 2: exact Ab; clear Ab.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt.
- 2-5: done.
- apply leq_trans with (n := (a.(CDate) + WAIT)).
- 2: exact Hlt.
- rewrite leq_add2l.
- by rewrite leq_eqVlt RRD_WAIT orbT.
+ 2: {
+ clear H.
+ apply FIFO_PRE_date in Hc as H; [ | done ]; destruct H as [Hcc [Hrun_c Hreq_c]].
+ apply FIFO_add_counter with (d := Next_cycle OCAS_date) in Hcc as H. destruct H as [Hrun_c' Hcc'].
+ 3: by rewrite /OCycle0 add0n FIFO_next_cycle_cas_eq_casS FIFO_WAIT_GT_SCAS.
+ 2: done.
+ set (d := Next_cycle OCAS_date).
+ specialize FIFO_l_eq_bound_or with (ta := c.(CDate) + d) (tb := b.(CDate)) (c := d) as HH.
+ apply HH in Hrun_c' as Hlt. clear HH.
+ 4: unfold d; by rewrite Hsb.
+ 3: by rewrite Hsb.
+ 2: by rewrite /OCycle0 add0n in Hcc'; fold d in Hcc'.
+ rewrite /FIFO_counter in Hcb; rewrite Hcb.
+ destruct Hlt as [H0 | [H1 | H2]]; fold d.
+ { rewrite -H0 addnBAC; [ | by rewrite addnC leq_addr ].
+ rewrite ltn_subRL addnC -addnA ltn_add2l.
+ apply nat_ltn_add; by rewrite FIFO_nextcycle_act_eq_actS. }
+ { rewrite leq_eqVlt in H1; move: H1 => /orP [/eqP H1 | H1].
+ { rewrite -H1 -addnA -subnA.
+ 3: rewrite -addnCA; by apply leq_addr.
+ 2: { unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite /CAS_date -addnS; by apply nat_ltn_add. }
+ rewrite ltn_subRL addnC ltn_add2l ltn_subLR.
+ 2: { unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite /CAS_date -addnS; by apply nat_ltn_add. }
+ rewrite -addnCA; apply nat_ltn_add; by rewrite addn_gt0 WAIT_pos orbT.
+ }
+ rewrite -subnA.
+ 3: { rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b.
+ rewrite /FIFO_counter Hsb Hcb in Hrun_b; fold d in Hrun_b.
+ by rewrite leq_eqVlt Hrun_b orbT. }
+ 2: { unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite /CAS_date -addnS; by apply nat_ltn_add. }
+ rewrite ltn_subRL addnC.
+ apply ltn_trans with (m := c.(CDate) + (d - Next_cycle OACT_date)) in H1. exact H1.
+ rewrite -addnA ltn_add2l ltn_subLR.
+ 2: { unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite /CAS_date -addnS; by apply nat_ltn_add. }
+ rewrite -addnCA; apply nat_ltn_add; by rewrite addn_gt0 WAIT_pos orbT. }
+ { contradict H2; apply /negP; rewrite -ltnNge.
+ unfold Before in cBb.
+ rewrite addnC -ltn_subRL.
+ apply ltn_trans with (n := b.(CDate)). exact cBb.
+ rewrite ltn_subRL addnC ltn_add2l; unfold d; rewrite FIFO_next_cycle_cas_eq_casS.
+ exact FIFO_WAIT_GT_SCAS. }
+ }
+ apply FIFO_in_the_past with (t := b.(CDate)); [ by apply Cmd_in_trace | ].
+ apply FIFO_in_the_past with (t := b.(CDate) - c0 + Next_cycle OACT_date).
+ { rewrite -subnA.
+ 3: { rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b.
+ rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT. }
+ 2: { rewrite /FIFO_counter in Hcb; rewrite Hcb;
+ rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS;
+ rewrite /CAS_date -addnS; by apply nat_ltn_add. }
+ apply leq_subr. }
+ exact H'.
Qed.
- Theorem Cmds_T_RRD_DBG_ok t: BANKGROUPS > 1 -> forall a b,
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b -> ~~ Same_Bankgroup a b ->
- Apart_at_least a b T_RRD_s.
+ Theorem Cmds_initial t b:
+ b \in (# t).(Arbiter_Commands) -> isCAS b ->
+ exists a, (a \in (# t).(Arbiter_Commands)) && (isACT a) && (Same_Row a b) && (Before a b).
Proof.
- intros H. specialize FIFO.DDR3 as Hbug. by rewrite Hbug in H.
- Qed.
+ intros Hb iCb.
+ apply FIFO_CAS_date in Hb as H; [ | done ]. destruct H as [Hcb [Hrun_b Hreq_b]].
+ destruct # (b.(CDate)).(Implementation_State) eqn:Hsb; [ done | ].
+
+ apply Request_exists in Hsb as H; try assumption; [ | by rewrite <- Hsb in Hreq_b].
+ rewrite -Hsb in Hreq_b.
+
+ apply Request_ACT_bounded in H as H'; try (by rewrite -Hsb in Hrun_b);
+ rewrite /Slot_start Hsb in H'.
+
+ exists (ACT_of_req r0 (b.(CDate) - c + Next_cycle OACT_date)).
+ rewrite /isACT //= andbT /Before /After //= /Same_Row /get_row /ACT_of_req //=.
+ apply /andP; split; [ apply /andP; split | ].
+ 2: {
+ unfold FIFO_request, get_req in *.
+ destruct b.(CKind) eqn:Hkind;
+ try (by unfold isCAS,isCRD,isCWR in iCb; rewrite Hkind in iCb);
+ rewrite Hsb in H,Hreq_b; rewrite inj_eq; try (exact ssrfun.Some_inj);
+ rewrite inj_eq in Hreq_b; try (exact ssrfun.Some_inj); move: Hreq_b => /eqP Hreq_b;
+ subst r0; by rewrite eq_refl.
+ }
+ 2: {
+ rewrite /FIFO_counter in Hcb; rewrite Hcb FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite -Hsb in Hrun_b; rewrite -subnA.
+ 3: { clear H.
+ apply Date_gt_counter in Hrun_b as H; rewrite Hsb /FIFO_counter Hcb FIFO_next_cycle_cas_eq_casS in H.
+ apply ltn_trans with (m := CAS_date) in H. exact H. done.
+ }
+ 2: rewrite /CAS_date /ACT_date -addnS; by apply nat_ltn_add.
+ rewrite ltn_subrL.
+ apply FIFO_date_gt_0 in Hb; rewrite subn_gt0 Hb andbT -addn1 -[CAS_date.+1]addn1 leq_add2r.
+ rewrite /CAS_date /ACT_date; apply nat_ltn_add; by rewrite lt0n T_RCD_pos.
+ }
+ apply (FIFO_in_the_past b.(CDate)); [ by apply Cmd_in_trace | ].
+ apply (FIFO_in_the_past (b.(CDate) - c + Next_cycle OACT_date)); [ | assumption ].
+ rewrite -subnA; [ apply leq_subr | |].
+ 2: {
+ rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b.
+ rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT.
+ }
+ rewrite /FIFO_counter in Hcb; rewrite Hcb;
+ rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS;
+ rewrite /CAS_date -addnS; by apply nat_ltn_add.
+ Qed.
- (* ------------------------------------------------------------------ *)
+ (* ------------------------------------------------------------------ *)
(* -------------------- REQUEST PROOFS ------------------------------ *)
(* ------------------------------------------------------------------ *)
+ Lemma FIFO_l_counter_border_run t :
+ FIFO_pending (# t).(Implementation_State) != [::] ->
+ FIFO_counter (# t).(Implementation_State) = WAIT.-1 ->
+ FIFO_counter # (t.+1).(Implementation_State) = 0 /\ isRUNNING # (t.+1).(Implementation_State).
+ Proof.
+ intros HP Hc; simpl.
+ rewrite /Next_state //=; destruct_state t; simpl; try done;
+ destruct c; simpl in *; unfold Next_cycle; simpl; set (H := m.+1 < WAIT); dependent destruction H;
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e; try done;
+ rewrite Hc prednK in x; lia.
+ Qed.
+
Lemma Pending_on_arrival ta ra:
- ra \in Arrival_at ta
- -> ra \in (FIFO_pending ((Default_arbitrate ta).(Implementation_State))).
+ ra \in Arrival_at ta -> ra \in (FIFO_pending # (ta).(Implementation_State)).
Proof.
- intros HA.
- destruct ta.
- { by rewrite /FIFO_pending //= /Enqueue mem_cat HA orTb. }
- { rewrite /FIFO_pending //= /Next_state.
- destruct (Default_arbitrate ta).(Implementation_State) as [c P | c P rb] eqn:HSS; simpl.
- { destruct P eqn:HP.
- { simpl. exact HA. }
- { simpl. assert (r == r). apply /eqP. reflexivity. by rewrite H /Enqueue mem_cat HA orbT. }
- }
- { destruct c; simpl.
- destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl.
- all: try by rewrite /Enqueue mem_cat HA orbT.
- destruct P eqn:HP; simpl.
- { exact HA. }
- { by rewrite /Enqueue mem_cat HA orbT. }
- }
- }
- Qed.
+ intros HA; destruct ta; [ by rewrite /FIFO_pending //= /Enqueue mem_cat HA orTb | ].
+ rewrite /FIFO_pending //= /Next_state.
+ destruct_state ta; simpl; try assumption; rewrite /Enqueue;
+ try (by rewrite eq_refl mem_cat HA orbT);
+ try (by rewrite in_cons mem_cat HA !orbT).
+ Qed.
- Lemma Pending_requestor ta ra:
- ra \in FIFO_pending (Default_arbitrate ta).(Implementation_State)
- -> isRUNNING (Default_arbitrate ta).(Implementation_State)
- -> FIFO_counter (Default_arbitrate ta).(Implementation_State) != WAIT.-1
- -> ra \in FIFO_pending (Default_arbitrate ta.+1).(Implementation_State).
+ Lemma Pending_requestor ta ra:
+ ra \in FIFO_pending # ta.(Implementation_State)
+ -> isRUNNING # ta.(Implementation_State)
+ -> FIFO_counter # ta.(Implementation_State) != WAIT.-1
+ -> ra \in FIFO_pending # (ta.+1).(Implementation_State).
Proof.
intros HP Hrun HCS.
simpl; unfold Next_state, FIFO_pending, isRUNNING in *.
- destruct (Default_arbitrate ta).(Implementation_State); simpl.
- { discriminate Hrun. }
- { destruct c; simpl. destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait, r eqn:HPP; simpl.
- all: try discriminate HP.
- all: try by rewrite /Enqueue -cat_cons mem_cat HP orTb.
- move: Hwait => /eqP Hwait; simpl in HCS.
- contradict Hwait. apply /eqP. exact HCS.
- }
- Qed.
+ destruct (Default_arbitrate ta).(Implementation_State); simpl; try done.
+ destruct c; simpl. destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait, r eqn:HPP;
+ simpl; try discriminate HP;
+ try (by rewrite /Enqueue -cat_cons mem_cat HP orTb).
+ move: Hwait => /eqP Hwait; simpl in HCS.
+ contradict Hwait; by apply /eqP.
+ Qed.
- Lemma Running_on_next_cycle ra ta:
- ra \in (FIFO_pending (Default_arbitrate ta).(Implementation_State)) ->
- isIDLE (Default_arbitrate ta).(Implementation_State) ->
- (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)) && (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0).
+ Lemma Running_on_next_cycle ra ta:
+ ra \in (FIFO_pending # ta.(Implementation_State)) ->
+ isIDLE # ta.(Implementation_State) ->
+ (isRUNNING # (ta.+1).(Implementation_State)) && (FIFO_counter # (ta.+1).(Implementation_State) == OCycle0).
Proof.
intros HP Hidle.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- 2: discriminate Hidle.
- clear Hidle.
+ destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs; [ | done ]; clear Hidle.
rewrite /FIFO_pending in HP.
- simpl. rewrite /Next_state Hs.
- destruct r eqn:HP'.
- { discriminate HP. }
- simpl. done.
+ rewrite //= /Next_state Hs.
+ destruct r eqn:HP'; [ discriminate HP | by simpl ].
Qed.
- Lemma Request_index_decrements_within_period_idle ta ra:
- let S := (Default_arbitrate ta).(Implementation_State) in
- (ra \in (FIFO_pending S))
- -> isIDLE (S)
+ (* Index in the pending queue decrements by one, because a request has been select @S *)
+ Lemma Request_index_decrements_within_period_idle ta ra:
+ let S := # ta.(Implementation_State) in (ra \in (FIFO_pending S))
+ -> isIDLE S
-> (0 < index ra (FIFO_pending S))
-> forall tb, ta < tb
-> tb <= ta + WAIT
- -> let S' := (Default_arbitrate tb).(Implementation_State) in
+ -> let S' := (# tb).(Implementation_State) in
(ra \in (FIFO_pending S')) && ((index ra (FIFO_pending S)) == (index ra (FIFO_pending S')).+1).
Proof.
intros S HP Hidle HI.
unfold S in *; clear S.
- destruct ((Default_arbitrate ta).(Implementation_State)) eqn:HSS; simpl.
- 2: discriminate Hidle.
- induction tb; intros HL HU.
- { contradict HL. by rewrite ltn0. }
- { rewrite leq_eqVlt in HL; move: HL => /orP [HL | HL].
- { clear IHtb.
- rewrite eqSS in HL; move: HL => /eqP HL; subst.
- simpl; unfold FIFO_counter, FIFO_pending, Next_state in *.
- rewrite HSS.
- destruct r eqn:HPP; simpl.
- { discriminate HP. }
- { assert (r0 == r0) as H'. apply /eqP. reflexivity. rewrite H'. clear H'.
- simpl in HI. destruct (r0 == ra) eqn:Heq.
- { discriminate HI. }
- rewrite in_cons in HP. move: HP => /orP [/eqP HP | HP].
- { contradict Heq. rewrite HP. apply /eqP. by rewrite eq_refl. }
- { rewrite /Enqueue mem_cat HP orTb index_cat HP. apply /eqP. reflexivity. }
- }
- }
- rewrite ltnS in HL.
- apply ltnW in HU as HU'.
- apply IHtb in HL as IH. clear IHtb.
- 2: exact HU'.
- move: IH => /andP [HP' /eqP IH'].
- rewrite -HSS in HP. apply Running_on_next_cycle in HP as HC. move: HC => /andP [Hrun /eqP Hc].
- 2: by rewrite HSS.
- apply FIFO_add_counter with (c := OCycle0) (d := tb - (ta.+1)) in Hrun as Haux. destruct Haux as [Hrun_a' Hca'].
- 3: exact Hc.
- 2: {
- rewrite /OCycle0 //= add0n ltn_subLR.
- 2: exact HL.
- apply ltn_trans with (n := ta + WAIT).
- exact HU.
- rewrite ltn_add2r. done.
- }
- assert (ta.+1 + (tb - ta.+1) = tb).
- { rewrite subnKC. reflexivity. exact HL. }
- rewrite H in Hrun_a', Hca'. clear H.
- rewrite /OCycle0 //= add0n in Hca'.
- apply Pending_requestor with (ra := ra) in Hrun_a' as Hpen.
- 3: {
- rewrite Hca' neq_ltn. apply /orP. left.
- rewrite ltn_subLR.
- 2: exact HL.
- rewrite addnC -subn1 addnBAC.
- 2: exact WAIT_pos.
- rewrite subn1 nat_add_pred. rewrite PeanoNat.Nat.pred_succ addnC. exact HU.
- }
- 2: exact HP'.
- rewrite Hpen andTb. rewrite IH'. clear HP HI Hpen. rename Hrun_a' into Hrun_b. rename Hca' into Hcb.
- rewrite eqSS.
- simpl. unfold FIFO_pending, Next_state.
- destruct (Default_arbitrate tb).(Implementation_State) eqn:HS.
- { discriminate Hrun_b. }
- { destruct c0; simpl.
- destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl.
- all: try by rewrite /Enqueue index_cat HP'.
- simpl in Hrun_b, Hcb, IH',HP', HS.
- assert (FIFO_counter (Default_arbitrate tb).(Implementation_State) = WAIT.-1) as Heq.
- { rewrite HS //=; move: Hwait => /eqP Hwait; exact Hwait. }
- apply FIFO_l_counter_border_run in Heq as [Hcb' Hrun_b'].
- 2: rewrite HS //=; by apply Queue_non_empty in HP'.
- apply FIFO_l_eq_bound with (tb := tb.+1) (c := OCycle0) in Hrun as Hbug.
- 5,4: rewrite /OCycle0 //=.
- 3: by rewrite -[ta.+1]addn1 -[tb.+1]addn1 ltn_add2r.
- 2: exact Hrun_b'.
- contradict Hbug.
- apply /negP; rewrite leqNgt; apply /negPn.
- rewrite [ta.+1 + _]addnC -[ta.+1]addn1 addnA -[tb.+1]addn1.
- rewrite addnCAC [tb +1 ]addnC -addnA ltn_add2l.
- exact HU.
- }
- }
- Qed.
-
- Lemma Request_index_decrements_within_period ta ra:
+ destruct (# ta.(Implementation_State)) eqn:HSS; simpl; [ | discriminate Hidle ].
+ induction tb; intros HL HU; [ contradict HL; by rewrite ltn0 | ].
+ rewrite leq_eqVlt in HL; move: HL => /orP [HL | HL].
+ { clear IHtb.
+ rewrite eqSS in HL; move: HL => /eqP HL; subst.
+ simpl; unfold FIFO_counter, FIFO_pending, Next_state in *.
+ rewrite HSS; destruct r eqn:HPP; simpl; [ discriminate HP | ].
+ rewrite eq_refl.
+ simpl in HI; destruct (r0 == ra) eqn:Heq; [ discriminate HI | ].
+ rewrite in_cons in HP; move: HP => /orP [/eqP HP | HP];
+ [ contradict Heq; rewrite HP; apply /eqP; by rewrite eq_refl | ].
+ by rewrite /Enqueue mem_cat HP orTb index_cat HP; apply /eqP; reflexivity.
+ }
+ rewrite ltnS in HL; apply ltnW in HU as HU'.
+ apply IHtb in HL as IH; clear IHtb; [ | assumption ].
+ move: IH => /andP [HP' /eqP IH'].
+ rewrite -HSS in HP; apply Running_on_next_cycle in HP as HC; [ | by rewrite HSS ].
+ move: HC => /andP [Hrun /eqP Hc].
+ apply FIFO_add_counter with (c := OCycle0) (d := tb - (ta.+1)) in Hrun as Haux; try assumption.
+ 2: {
+ rewrite /OCycle0 //= add0n ltn_subLR; [ | assumption ].
+ apply ltn_trans with (n := ta + WAIT); [ assumption | ].
+ by rewrite ltn_add2r.
+ }
+ destruct Haux as [Hrun_a' Hca'].
+ assert (ta.+1 + (tb - ta.+1) = tb); [ rewrite subnKC; [ reflexivity | exact HL ] | ].
+ rewrite H in Hrun_a', Hca'; clear H.
+ rewrite /OCycle0 //= add0n in Hca'.
+ apply Pending_requestor with (ra := ra) in Hrun_a' as Hpen; try assumption.
+ 2: {
+ rewrite Hca' neq_ltn; apply /orP; left.
+ rewrite ltn_subLR; [ | assumption ].
+ rewrite addnC -subn1 addnBAC; [ lia | exact WAIT_pos ].
+ }
+ rewrite Hpen andTb IH'; clear HP HI Hpen;
+ rename Hrun_a' into Hrun_b, Hca' into Hcb.
+ rewrite eqSS //= /FIFO_pending /Next_state.
+ destruct (Default_arbitrate tb).(Implementation_State) eqn:HS; [ discriminate Hrun_b | ].
+ destruct c0; simpl.
+ destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl;
+ try (by rewrite /Enqueue index_cat HP').
+ simpl in Hrun_b, Hcb, IH',HP', HS.
+ assert (Heq : FIFO_counter # tb.(Implementation_State) = WAIT.-1);
+ [ rewrite HS //=; move: Hwait => /eqP Hwait; exact Hwait | ].
+ apply FIFO_l_counter_border_run in Heq as [Hcb' Hrun_b'];
+ [ | rewrite HS //=; by apply Queue_non_empty in HP' ].
+ apply FIFO_l_eq_bound with (tb := tb.+1) (c := OCycle0) in Hrun as Hbug; try assumption.
+ contradict Hbug; lia.
+ (* apply /negP; rewrite leqNgt; apply /negPn. lia.
+ rewrite [ta.+1 + _]addnC -[ta.+1]addn1 addnA -[tb.+1]addn1.
+ rewrite addnCAC [tb +1 ]addnC -addnA ltn_add2l.
+ *)
+ Qed.
+
+ Lemma Request_index_decrements_within_period ta ra:
let S := (Default_arbitrate ta).(Implementation_State) in
- (ra \in (FIFO_pending S))
- -> (FIFO_counter S) == WAIT.-1
- -> (0 < index ra (FIFO_pending S))
- -> forall tb, ta < tb
- -> tb <= ta + WAIT
- -> let S' := (Default_arbitrate tb).(Implementation_State) in
- (ra \in (FIFO_pending S')) && ((index ra (FIFO_pending S)) == (index ra (FIFO_pending S')).+1).
- Proof.
- intros S HP HC HI.
- unfold S in *; clear S.
- induction tb; intros HL HU.
- { contradict HL. by rewrite ltn0. }
- { rewrite leq_eqVlt in HL; move: HL => /orP [HL | HL].
- { clear IHtb.
- rewrite eqSS in HL; move: HL => /eqP HL; subst.
- simpl; unfold FIFO_counter, FIFO_pending, Next_state in *.
- destruct (Default_arbitrate tb).(Implementation_State) as [c P | c P rb] eqn:HSS; move: HC => /eqP HC; subst.
- { destruct P eqn:HPP; simpl. (* IDLE state *)
- { discriminate HP. }
- { assert (r == r) as H'. apply /eqP. reflexivity. rewrite H'. clear H'.
- simpl in HI. destruct (r == ra) eqn:He.
- { discriminate HI. }
- { rewrite in_cons in HP. move: HP => /orP [/eqP HP | HP].
- { contradict He. rewrite HP. apply /eqP. by rewrite eq_refl. }
- { rewrite /Enqueue mem_cat HP orTb index_cat HP.
- apply /eqP. reflexivity.
- }
- }
- }
- }
- { rewrite HC FIFO_wait_neq_act FIFO_wait_neq_cas. (* RUNNING state *)
- assert (WAIT.-1 == WAIT.-1 = true). { apply /eqP. reflexivity. }
- rewrite H; clear H.
- destruct P eqn:HPP; simpl.
- { discriminate HP. }
- { assert (r == r) as H'. apply /eqP. reflexivity. rewrite H'. clear H'.
- simpl in HI. destruct (r == ra) eqn:He.
- { discriminate HI. }
- { rewrite in_cons in HP. move: HP => /orP [/eqP HP | HP].
- { contradict He. rewrite HP. apply /eqP. by rewrite eq_refl. }
- { rewrite /Enqueue mem_cat HP orTb index_cat HP.
- apply /eqP. reflexivity.
- }
- }
- }
- }
- }
- { rewrite ltnS in HL.
- apply IHtb in HL as IH; clear IHtb.
- 2: by apply ltnW in HU.
- move: IH => /andP [HP' /eqP HI']; rewrite HI'; move: HC => /eqP HC.
- apply FIFO_l_counter_border_run in HC.
- 2: by apply Queue_non_empty in HP.
- destruct HC as [Hca Hrun_a].
- assert (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) = OCycle0).
- { rewrite Hca /OCycle0 //=. }
- apply FIFO_add_counter with (c := OCycle0) (d := tb - (ta.+1)) in Hrun_a as Haux. destruct Haux as [Hrun_a' Hca'].
- 3: exact H.
- 2: {
- rewrite //= /OCycle0 add0n ltn_subLR.
- 2: exact HL.
- apply ltn_trans with (n := ta + WAIT).
- 2: by rewrite ltn_add2r ltnSn.
- exact HU.
- }
- assert (ta.+1 + (tb - ta.+1) = tb).
- { rewrite subnKC. reflexivity. exact HL. }
- rewrite H0 in Hrun_a',Hca'.
- rewrite /OCycle0 //= add0n in Hca'.
- apply Pending_requestor with (ra := ra) in Hrun_a' as Hpen.
- 3: {
- rewrite Hca' neq_ltn. apply /orP. left.
- rewrite ltn_subLR.
- 2: exact HL.
- rewrite addnC -subn1 addnBAC.
- 2: exact WAIT_pos.
- rewrite subn1 nat_add_pred. rewrite PeanoNat.Nat.pred_succ addnC. exact HU.
- }
- 2: exact HP'.
- rewrite Hpen andTb; clear H H0 HP HI Hpen. rename Hrun_a' into Hrun_b.
- rewrite eqSS.
- simpl. unfold FIFO_pending, Next_state.
- destruct (Default_arbitrate tb).(Implementation_State) as [c P | c P rb] eqn:HSS.
- { discriminate Hrun_b. }
- { destruct c; simpl.
- destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl.
- all: try by rewrite /Enqueue index_cat HP'.
- simpl in Hrun_b, Hca', HI', HP', HSS.
- assert (FIFO_counter (Default_arbitrate tb).(Implementation_State) = WAIT.-1) as Heq.
- { rewrite HSS //=; move: Hwait => /eqP Hwait; exact Hwait. }
- apply FIFO_l_counter_border_run in Heq as [Hcb Hrun_b'].
- 2: rewrite HSS //=; by apply Queue_non_empty in HP'.
- apply FIFO_l_eq_bound with (tb := tb.+1) (c := OCycle0) in Hrun_a as Hbug.
- 5: rewrite /OCycle0 //=.
- 4: rewrite /OCycle0 //=.
- 3: by rewrite -[ta.+1]addn1 -[tb.+1]addn1 ltn_add2r.
- 2: exact Hrun_b'.
- contradict Hbug.
- apply /negP; rewrite leqNgt; apply /negPn.
- rewrite [ta.+1 + _]addnC -[ta.+1]addn1 addnA -[tb.+1]addn1.
- rewrite addnCAC [tb +1 ]addnC -addnA ltn_add2l.
- exact HU.
- }
+ (ra \in (FIFO_pending S))
+ -> (FIFO_counter S) == WAIT.-1
+ -> (0 < index ra (FIFO_pending S))
+ -> forall tb, ta < tb
+ -> tb <= ta + WAIT
+ -> let S' := (Default_arbitrate tb).(Implementation_State) in
+ (ra \in (FIFO_pending S')) && ((index ra (FIFO_pending S)) == (index ra (FIFO_pending S')).+1).
+ Proof.
+ cbv zeta; intros HP HC HI.
+ induction tb; intros HL HU; [ contradict HL; by rewrite ltn0 | ].
+ rewrite leq_eqVlt in HL; move: HL => /orP [HL | HL]; [ clear IHtb | ].
+ { rewrite eqSS in HL; move: HL => /eqP HL; subst.
+ simpl; unfold FIFO_counter, FIFO_pending, Next_state in *.
+ destruct (# tb).(Implementation_State) as [c P | c P rb] eqn:HSS; move: HC => /eqP HC; subst.
+ { destruct P eqn:HPP; simpl; [ discriminate HP | ].
+ rewrite eq_refl.
+ simpl in HI; destruct (r == ra) eqn:He; [ discriminate HI | ].
+ rewrite in_cons in HP; move: HP => /orP [/eqP HP | HP];
+ [ contradict He; rewrite HP; apply /eqP; by rewrite eq_refl | ].
+ by rewrite /Enqueue mem_cat HP orTb index_cat HP andTb eq_refl.
+ }
+ { rewrite HC FIFO_wait_neq_act FIFO_wait_neq_cas eq_refl. (* RUNNING state *)
+ destruct P eqn:HPP; simpl; [ discriminate HP | ].
+ rewrite eq_refl.
+ simpl in HI; destruct (r == ra) eqn:He; [ discriminate HI | ].
+ rewrite in_cons in HP; move: HP => /orP [/eqP HP | HP];
+ [ contradict He; rewrite HP; apply /eqP; by rewrite eq_refl | ].
+ by rewrite /Enqueue mem_cat HP orTb index_cat HP andTb eq_refl.
}
+ }
+ { rewrite ltnS in HL.
+ apply IHtb in HL as IH; clear IHtb; [ | by apply ltnW in HU ].
+ move: IH => /andP [HP' /eqP HI']; rewrite HI'; move: HC => /eqP HC.
+ apply FIFO_l_counter_border_run in HC; [ | by apply Queue_non_empty in HP ].
+ destruct HC as [Hca Hrun_a].
+ assert (FIFO_counter # (ta.+1).(Implementation_State) = OCycle0); [ rewrite Hca /OCycle0 //= | ].
+ apply FIFO_add_counter with (c := OCycle0) (d := tb - (ta.+1)) in Hrun_a as Haux; try assumption.
+ 2: rewrite //= /OCycle0 add0n ltn_subLR; [ lia | assumption ].
+ destruct Haux as [Hrun_a' Hca'].
+ assert (H0 : ta.+1 + (tb - ta.+1) = tb); [ lia | ].
+ rewrite H0 in Hrun_a',Hca'.
+ rewrite /OCycle0 //= add0n in Hca'.
+ apply Pending_requestor with (ra := ra) in Hrun_a' as Hpen; try assumption; [ | lia ].
+ rewrite Hpen andTb; clear H H0 HP HI Hpen; rename Hrun_a' into Hrun_b.
+ rewrite eqSS //= /FIFO_pending /Next_state.
+ destruct (# tb).(Implementation_State) as [c P | c P rb] eqn:HSS; [ discriminate Hrun_b | ];
+ destruct c; simpl.
+ destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl;
+ try by rewrite /Enqueue index_cat HP'.
+ simpl in Hrun_b, Hca', HI', HP', HSS.
+ assert (FIFO_counter (# tb).(Implementation_State) = WAIT.-1) as Heq;
+ [ rewrite HSS //=; move: Hwait => /eqP Hwait; exact Hwait | ].
+ apply FIFO_l_counter_border_run in Heq as [Hcb Hrun_b'];
+ [ | rewrite HSS //=; by apply Queue_non_empty in HP' ].
+ apply FIFO_l_eq_bound with (tb := tb.+1) (c := OCycle0) in Hrun_a as Hbug; try assumption.
+ contradict Hbug; lia.
}
Qed.
- Lemma Still_pending_on_running_border ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- let S' := (Default_arbitrate ta.+1).(Implementation_State) in
+ (* ------------------------------------------------------------------ *)
+ (* --------------------- HIGH-LEVEL PROPERTIES ---------------------- *)
+ (* ------------------------------------------------------------------ *)
+
+ Lemma Still_pending_on_running_border ra ta:
+ let S := # ta.(Implementation_State) in
+ let S' := # (ta.+1).(Implementation_State) in
ra \in (FIFO_pending S) ->
isRUNNING (S) ->
0 < index ra (FIFO_pending S) ->
@@ -1420,8 +1555,8 @@ Module FIFOPROOFS (SYS : SystemModule).
Qed.
Lemma Still_pending_on_idle_border ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- let S' := (Default_arbitrate ta.+1).(Implementation_State) in
+ let S := # ta.(Implementation_State) in
+ let S' := # (ta.+1).(Implementation_State) in
ra \in (FIFO_pending S) ->
isIDLE (S) ->
0 < index ra (FIFO_pending S) ->
@@ -1508,8 +1643,7 @@ Module FIFOPROOFS (SYS : SystemModule).
4: rewrite ltn_predL; exact WAIT_pos.
3: exact Hc.
2: exact Hrun.
- assert (ta.+1 + WAIT.-1 = ta + WAIT).
- { by rewrite -nat_add_pred addnC addnS -pred_Sn addnC. }
+ assert (ta.+1 + WAIT.-1 = ta + WAIT); [ specialize WAIT_pos; lia | ].
rewrite H in HP'' Hi'. clear H.
rewrite HP'' andTb.
move: Hi => /eqP Hi. rewrite Hi.
@@ -1522,20 +1656,18 @@ Module FIFOPROOFS (SYS : SystemModule).
apply FIFO_add_counter with (c:= c) (d := (WAIT.-1 - c)) in Hrun as Hc.
3: by rewrite /FIFO_counter Hs.
2: { rewrite subnKC.
- 2: destruct c; simpl; clear Hs HP HU; by apply nat_ltn_leq_pred in i0.
- 1: rewrite ltn_predL. exact WAIT_pos.
+ 2: destruct c; simpl; clear Hs HP HU; lia.
+ 1: rewrite ltn_predL; exact WAIT_pos.
}
destruct Hc as [Hrun' Hc].
rewrite subnKC in Hc.
- 2: destruct c; simpl; clear Hs HP HU Hrun Hrun'; by apply nat_ltn_leq_pred in i0.
- apply Still_pending_on_running_border in HP as H. move: H => /andP [ /andP [ /andP [Hrun'' Hc'] HP'] Hi].
- 4: by rewrite Hc.
- 3: by rewrite -Heq in HU.
- 2: exact Hrun'.
- apply Still_pending_during_window with (c := OCycle0) (d := WAIT.-1) in HP' as H. move: H => /andP [HP'' Hi'].
- 4: rewrite ltn_predL; exact WAIT_pos.
- 3: exact Hc'.
- 2: exact Hrun''.
+ 2: destruct c; simpl; clear Hs HP HU Hrun Hrun'; lia.
+ apply Still_pending_on_running_border in HP as H;
+ [ | assumption | by rewrite -Heq in HU | by rewrite Hc ].
+ move: H => /andP [ /andP [ /andP [Hrun'' Hc'] HP'] Hi];
+ apply Still_pending_during_window with (c := OCycle0) (d := WAIT.-1) in HP' as H; try assumption.
+ 2: rewrite ltn_predL; exact WAIT_pos.
+ move: H => /andP [HP'' Hi'].
assert ((ta + (WAIT.-1 -c)).+1 + WAIT.-1 = ta + (WAIT.-1 - c) + WAIT) as H.
{ rewrite -addnS -addn1 addnA -addnA [1 + WAIT.-1]addnC addn1 prednK. reflexivity. exact WAIT_pos. }
rewrite H in HP'',Hi'.
@@ -1565,7 +1697,7 @@ Module FIFOPROOFS (SYS : SystemModule).
}
{ rewrite -Hs in HP'.
assert (c + (WAIT.-1 -c ) = WAIT.-1) as Hcounter.
- { rewrite subnKC. reflexivity. destruct c. simpl in *. clear Hs. by apply nat_ltn_leq_pred in i0. }
+ { rewrite subnKC. reflexivity. destruct c. simpl in *. clear Hs; lia. }
assert (isRUNNING (Default_arbitrate (Requestor_slot_start ta + i * WAIT)).(Implementation_State)) as Hrun.
{ by rewrite Hs. }
apply FIFO_add_counter with (c := c) (d := (WAIT.-1 -c)) in Hrun as Hc. destruct Hc as [Hrun' Hc].
@@ -1580,21 +1712,17 @@ Module FIFOPROOFS (SYS : SystemModule).
3: { move: Hi' => /eqP Hi'. rewrite -Hi'. rewrite -Hs in Hi. rewrite Hi in HU. rewrite addnC in HU. by apply nat_ltn_add_rev in HU. }
2: exact Hrun'.
move: H => /andP [/andP [/andP [Hrun'' Hc'] HP'''] Hi''].
- apply Still_pending_during_window with (c := OCycle0) (d := c) in HP''' as H.
- 4: by destruct c.
- 3: exact Hc'.
- 2: exact Hrun''.
- move: H => /andP [HP'''' Hi'''].
+ apply Still_pending_during_window with (c := OCycle0) (d := c) in HP''' as H; try assumption.
+ 2: by destruct c.
+ move: H => /andP [HP'''' Hi'''].
rewrite mulSn -![WAIT + i * WAIT]addnC addnA.
assert ((Requestor_slot_start ta + i * WAIT + (WAIT.-1 - c)).+1 + c = Requestor_slot_start ta + i * WAIT + WAIT).
{ rewrite -addnS -addnA.
apply /eqP.
- rewrite eqn_add2l -subSn.
- 2: { destruct c; simpl in *. clear Hs. by apply nat_ltn_leq_pred in i0. }
- rewrite prednK.
- 2: exact WAIT_pos.
- rewrite subnK.
- 2: { destruct c; simpl in *. clear Hs. by apply ltnW in i0. }
+ rewrite eqn_add2l -subSn; [ | destruct c; simpl in *; clear Hs; lia ];
+ rewrite prednK; [ | exact WAIT_pos].
+ rewrite subnK;
+ [ | destruct c; simpl in *; clear Hs; by apply ltnW in i0 ].
apply /eqP. reflexivity.
}
rewrite H in HP''''; rewrite HP'''' andTb.
@@ -1714,7 +1842,7 @@ Module FIFOPROOFS (SYS : SystemModule).
destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
{ rewrite Hs in H. discriminate H. }
{ assert (c + (WAIT.-1 - c) = WAIT.-1).
- { rewrite subnKC. reflexivity. destruct c. simpl in *. clear Hs. by apply nat_ltn_leq_pred in i. }
+ { rewrite subnKC. reflexivity. destruct c. simpl in *. clear Hs. lia. }
assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun.
{ by rewrite Hs. }
apply FIFO_add_counter with (c := c) (d := (WAIT.-1 -c)) in Hrun as [_ Hc].
@@ -1758,7 +1886,7 @@ Module FIFOPROOFS (SYS : SystemModule).
}
{ rewrite -Hs in HP.
assert (c + (WAIT.-1 -c) = WAIT.-1) as Hcounter.
- { rewrite subnKC. reflexivity. destruct c; simpl in *. clear Hs. by apply nat_ltn_leq_pred in i0. }
+ { rewrite subnKC. reflexivity. destruct c; simpl in *. clear Hs. lia. }
assert (isRUNNING (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) as Hrun.
{ by rewrite Hs. }
apply Running_at_slot_start in Hrun as Hc.
@@ -1787,7 +1915,6 @@ Module FIFOPROOFS (SYS : SystemModule).
3: exact HU'.
2: exact Hi_pos.
move: HP => /andP [HP' Hi].
-
apply Still_pending_on_running_border in HP' as H.
4: by apply /eqP.
3: { move: Hi => /eqP Hi. rewrite Hi addnC in HU. by apply nat_ltn_add_rev in HU. }
@@ -1806,58 +1933,6 @@ Module FIFOPROOFS (SYS : SystemModule).
}
Qed.
- Lemma Request_starts_running ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- isRUNNING (S) ->
- FIFO_counter (S) == WAIT.-1 ->
- ra \in FIFO_pending (S) ->
- index ra (FIFO_pending S) = 0 ->
- (FIFO_request (Default_arbitrate ta.+1).(Implementation_State) == Some ra) &&
- (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0) &&
- (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)).
- Proof.
- intros S Hrun Hc HP Hi.
- unfold S in *; clear S.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- 1: discriminate Hrun.
- simpl; rewrite /Next_state Hs.
- destruct (nat_of_ord c == OACT_date) eqn:Hact, (nat_of_ord c == OCAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl.
- all: rewrite /FIFO_counter in Hc.
- all: try by rewrite Hc in Hwait.
- 4: destruct r eqn:HPP; simpl.
- 4: { discriminate HP. }
- 4: {
- destruct (r1 == ra) eqn:Heq.
- { move: Heq => /eqP Heq. by rewrite Heq eq_refl. }
- { simpl in Hi. rewrite Heq in Hi. discriminate Hi. }
- }
- 1,2: move: Hc => /eqP Hc; rewrite Hc in Hact; by rewrite FIFO_wait_neq_act in Hact.
- move: Hc => /eqP Hc; rewrite Hc in Hcas; by rewrite FIFO_wait_neq_cas in Hcas.
- Qed.
-
- Lemma Request_starts_idle ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- isIDLE (S) ->
- ra \in FIFO_pending (S) ->
- index ra (FIFO_pending S) = 0 ->
- (FIFO_request (Default_arbitrate ta.+1).(Implementation_State) == Some ra) &&
- (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0) &&
- (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)).
- Proof.
- intros S Hidle HP Hi.
- unfold S in *; clear S.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- 2: discriminate Hidle.
- simpl; rewrite /Next_state Hs.
- destruct r eqn:HPP.
- { discriminate HP. }
- simpl; rewrite eq_refl !andbT.
- rewrite /FIFO_pending in Hi.
- destruct (r0 == ra) eqn:Heq.
- { move: Heq => /eqP Heq. by rewrite Heq. }
- simpl in Hi. rewrite Heq in Hi. discriminate Hi.
- Qed.
-
Lemma Request_starts_idle_ ra ta:
let S := (Default_arbitrate ta).(Implementation_State) in
isIDLE (S) ->
@@ -1882,39 +1957,6 @@ Module FIFOPROOFS (SYS : SystemModule).
simpl in Hi. rewrite Heq in Hi. discriminate Hi.
Qed.
- Lemma Request_running_in_slot ra ta d:
- FIFO_request (Default_arbitrate ta).(Implementation_State) == Some ra ->
- FIFO_counter (Default_arbitrate ta).(Implementation_State) == OCycle0 ->
- d < WAIT ->
- (FIFO_request (Default_arbitrate (ta + d)).(Implementation_State) == Some ra).
- Proof.
- intros Hreq Hc Hd.
- induction d.
- { by rewrite addn0 Hreq. }
- apply ltn_trans with (m := d) in Hd as Hd'.
- 2: done.
- apply IHd in Hd' as IH. clear IHd.
- assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun.
- { destruct (Default_arbitrate ta).(Implementation_State).
- { rewrite /FIFO_request in Hreq. discriminate Hreq. }
- { done. }
- }
- destruct (Default_arbitrate (ta + d)).(Implementation_State) eqn:Hs.
- { rewrite /FIFO_request in IH. discriminate IH. }
- { apply FIFO_add_counter with (c := OCycle0) (d := d) in Hrun as H. destruct H as [Hrun' Hc'].
- 3: apply /eqP; exact Hc.
- 2: rewrite /OCycle0 //= add0n.
- rewrite /OCycle0 //= add0n in Hc'.
- rewrite addnS; simpl; rewrite /Next_state Hs //=.
- destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl.
- all: try by rewrite /FIFO_request in IH.
- destruct r eqn:HPP; simpl.
- all: rewrite Hs /FIFO_counter in Hc'; move: Hwait => /eqP Hwait; rewrite Hc' in Hwait; rewrite Hwait prednK in Hd.
- all: try exact WAIT_pos.
- all: try by rewrite ltnn in Hd.
- }
- Qed.
-
Lemma Request_processing ta ra d:
ra \in (Arrival_at ta)
-> let t := Requestor_slot_start ta in
@@ -1940,595 +1982,174 @@ Module FIFOPROOFS (SYS : SystemModule).
2: by rewrite Hs.
apply Request_running_in_slot with (d := d) in Hreq as Hreq'.
3: exact Hd.
- 2: exact Hc.
- rewrite Hreq' andbT.
- apply FIFO_add_counter with (c:=OCycle0) (d:=d) in Hrun. destruct Hrun as [_ H].
- 3: by apply /eqP.
- 2: rewrite /OCycle0 //= add0n.
- rewrite /OCycle0 add0n in H; by apply /eqP.
- }
- { assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun.
- { by rewrite Hs. }
- assert (c + (WAIT.-1 - c ) = WAIT.-1).
- { rewrite subnKC. reflexivity. destruct c; simpl in *. clear Hs. by apply nat_ltn_leq_pred in i. }
- apply FIFO_add_counter with (c := c) (d := (WAIT.-1 -c)) in Hrun as H'. destruct H' as [Hrun' Hc'].
- 3: by rewrite Hs.
- 2: rewrite H ltn_predL; exact WAIT_pos.
- rewrite H in Hc'.
- apply Request_starts_running with (ra := ra) in Hrun' as H'. move: H' => /andP [/andP [Hreq Hc''] Hrun''].
- 4: exact Hz.
- 3: exact HP'.
- 2: by rewrite Hc' eq_refl.
- apply FIFO_add_counter with (c := OCycle0) (d:= d) in Hrun'' as H'. destruct H' as [Hrun''' Hc'''].
- 3: by apply /eqP.
- 2: by rewrite /OCycle0 add0n.
- apply Request_running_in_slot with (d := d) in Hreq.
- 3: exact Hd.
- 2: exact Hc''.
- rewrite Hreq andbT.
- rewrite /OCycle0 add0n in Hc'''; by rewrite Hc''' eq_refl.
- }
- }
- apply Counter_reaches with (i := index ra (FIFO_pending (Default_arbitrate t).(Implementation_State))) in HP'.
- 3: by subst t.
- 2: by rewrite Hz.
- move: HP' => /andP [Hrun HC].
- apply Request_processing_starts in HA as H. move: H => /andP [HP' Hiz].
- fold t in Hrun,HC; rewrite Hz in Hrun,HC.
- fold i in Hrun,HC; fold t in HP',Hiz.
- rewrite Hz in HP',Hiz; fold i in HP',Hiz.
- apply Request_starts_running with (ra := ra) in HC as H. move: H => /andP [/andP [Hreq HC'] H].
- 4: by apply /eqP.
- 3: exact HP'.
- 2: exact Hrun.
- apply FIFO_add_counter with (c := OCycle0) (d := d) in H. destruct H as [Hrun' HC''].
- 3: by apply /eqP.
- 2: rewrite /OCycle0 add0n; exact Hd.
- rewrite /OCycle0 add0n in HC''.
- apply Request_running_in_slot with (d := d) in Hreq as H.
- 3: exact Hd.
- 2: exact HC'.
- set S' := (Default_arbitrate ((t + i).+1 + d)).(Implementation_State); simpl.
- by fold S' in HC'',H; rewrite H; rewrite HC'' eq_refl.
- Qed.
-
- Lemma Request_CAS ta ra:
- ra \in (Arrival_at ta)
- -> let tc := (Requestor_slot_start ta + (index ra (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) * WAIT) + CAS_date).+1 in
- (CAS_of_req ra tc.+1) \in (Default_arbitrate tc.+1).(Arbiter_Commands).
- Proof.
- intros HA.
- apply Request_processing with (d := CAS_date) in HA as H.
- 2: exact WAIT_CAS.
- move: H => /andP [HC HR]; clear HA.
- rewrite addSn in HC, HR; set (tc := _ + CAS_date); fold tc in HC, HR.
- destruct (Default_arbitrate tc.+1).(Implementation_State) eqn:Hs; simpl.
- { by rewrite /FIFO_request in HR. }
- simpl in Hs; rewrite Hs.
- rewrite /Next_state.
- rewrite /FIFO_counter in HC.
- assert ((nat_of_ord c == ACT_date) = false) as Hact.
- { move: HC => /eqP HC. by rewrite HC CAS_neq_ACT. }
- rewrite //= Hact HC //= /CAS_of_req in_cons; apply /orP; left.
- rewrite /FIFO_request inj_eq in HR. move: HR => /eqP HR.
- 2: exact ssrfun.Some_inj.
- by rewrite HR.
- Qed.
-
- Lemma Counter_at_running_slot_start ta c:
- FIFO_counter (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) == c ->
- isRUNNING (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) ->
- c == WAIT.-1.
- Proof.
- intros Hc Hrun.
- unfold Requestor_slot_start in *.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- { by rewrite Hs in Hrun. }
- { clear Hrun.
- assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as H.
- { by rewrite Hs. }
- assert (c0 + (WAIT.-1 - c0) = WAIT.-1).
- { rewrite subnKC. reflexivity. destruct c0; simpl in *; clear Hs; by apply nat_ltn_leq_pred in i. }
- apply FIFO_add_counter with (c := c0) (d := (WAIT.-1 - c0)) in H as [Hrun Hc'].
- 3: by rewrite Hs.
- 2: rewrite H0; rewrite ltn_predL; exact WAIT_pos.
- rewrite H0 in Hc'; by rewrite Hc' eq_sym in Hc.
- }
- Qed.
-
- Lemma Request_PRE ta ra:
- ra \in (Arrival_at ta)
- -> let i := index ra (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) * WAIT in
- let tc := ((Requestor_slot_start ta) + i).+1 in
- (PRE_of_req ra tc) \in (Default_arbitrate tc).(Arbiter_Commands).
- Proof.
- intros HA.
-
- apply Request_processing_starts in HA as HP; move: HP => /andP [HP HI].
- set i := index _ _; fold i in HP,HI.
- set t := Requestor_slot_start ta + i * WAIT; fold t in HP,HI.
-
- destruct i eqn:Hz. (* Case i = 0 *)
- { rewrite mul0n //= addn0; subst t.
- rewrite mul0n addn0 in HP,HI.
- rewrite /Next_state.
- destruct (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) eqn:Hs.
- { rewrite /FIFO_pending in HP,HI.
- destruct r eqn:HPP.
- { discriminate HP. }
- { destruct (ra == r0) eqn:Heq.
- { simpl; move: Heq => /eqP Heq; rewrite /PRE_of_req in_cons Heq; apply /orP; left; by rewrite eq_refl. }
- { rewrite eq_sym in Heq; by rewrite //= Heq in HI. }}}
- { rewrite /FIFO_pending in HP,HI.
- assert (FIFO_counter (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) == c).
- { by rewrite Hs. }
- apply Counter_at_running_slot_start in H.
- 2: by rewrite Hs.
- move: H => /eqP H; rewrite H FIFO_wait_neq_act FIFO_wait_neq_cas eq_refl.
- destruct r eqn:HPP.
- { discriminate HP. }
- { destruct (r1 == ra) eqn:Heq.
- { simpl; move: Heq => /eqP Heq; rewrite /PRE_of_req in_cons Heq; apply /orP; left; by rewrite eq_refl. }
- { by rewrite //= Heq in HI. }}}}
-
- apply Pending_on_arrival in HA as H.
- apply Pending_requestor_slot_start with (tb := Requestor_slot_start ta) in H.
- 3: by rewrite leqnn.
- 2: { rewrite /Requestor_slot_start; destruct (Default_arbitrate ta).(Implementation_State).
- by rewrite leqnn. by rewrite leq_addr. }
- apply Counter_reaches with (i := i) in H. move: H => /andP [Hrun HC]; fold t in Hrun,HC.
- 3: subst i; by rewrite leqnn.
- 2: by rewrite Hz.
-
- simpl; fold t; rewrite /Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- { destruct r eqn:HPP.
- { simpl in HP; discriminate HP. }
- { destruct (r0 == ra) eqn:Heq.
- { by simpl; move: Heq => /eqP Heq; rewrite in_cons /PRE_of_req //= Heq eq_refl orTb. }
- { by rewrite /FIFO_pending //= Heq in HI. }
- }}
- { unfold FIFO_pending in HP,HI. subst t; rewrite -Hz in Hs; rewrite Hs /FIFO_counter in HC; move: HC => /eqP HC.
- rewrite HC FIFO_wait_neq_act FIFO_wait_neq_cas eq_refl.
- destruct r eqn:HPP.
- { discriminate HP. }
- { destruct (r1 == ra) eqn:Heq.
- { simpl; move: Heq => /eqP Heq; by rewrite in_cons /PRE_of_req //= Heq eq_refl orTb. }
- { by rewrite /FIFO_pending //= Heq in HI. }
- }
- }
- Qed.
-
- Theorem Requests_handled ta ra:
- ra \in (Arrival_at ta)
- -> exists tc, (CAS_of_req ra tc) \in ((Default_arbitrate tc).(Arbiter_Commands)).
- Proof.
- intros HA.
- apply Request_CAS in HA as H.
- set tc := _.+1 in H.
- exists (tc.+1).
- exact H.
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* -------------------- PROTOCOL PROOFS ----------------------------- *)
- (* ------------------------------------------------------------------ *)
-
- Lemma Request_PRE_bounded t ra:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- FIFO_request (Default_arbitrate t).(Implementation_State) == Some ra ->
- (PRE_of_req ra (Slot_start t)) \in (Default_arbitrate (Slot_start t)).(Arbiter_Commands).
- Proof.
- intros Hrun Hreq.
- induction t.
- { by simpl in Hrun. }
- rewrite /Slot_start. simpl in *. unfold Next_state in *. simpl in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- { destruct r eqn:HPP; simpl in *.
- { by simpl in Hrun. }
- { clear Hrun IHt.
- rewrite /Next_state Hs //= subn0 in_cons /PRE_of_req.
- rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
- 2: exact ssrfun.Some_inj.
- by rewrite Hreq eq_refl orTb. } }
- { destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl in *.
- 7: destruct r eqn:HPP.
- 7: by simpl in Hrun.
- 7: {
- simpl; rewrite /Next_state Hs Hact Hcas Hwait //=.
- rewrite in_cons subn0; apply /orP; left.
- simpl in Hreq; rewrite /PRE_of_req.
- rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
- 2: exact ssrfun.Some_inj.
- by rewrite Hreq.
- }
- all: apply IHt in Hreq as IH.
- all: try trivial; clear IHt.
- all: rewrite /Slot_start Hs in IH.
- all: try (rewrite {1}/Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc).
- all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
- all: try (rewrite {1}/Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc).
- all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
- all: try (rewrite subSS; by exact IH).
- all: try (contradict x; by apply Bool.not_true_iff_false).
- all: try (contradict x0; by apply Bool.not_true_iff_false).
- all: try (move: Hact => /eqP Hact; by rewrite Hact FIFO_WAIT_GT_ACTp1 in x).
- all: try (move: Hcas => /eqP Hcas; by rewrite Hcas FIFO_WAIT_GT_CASp1 in x).
- clear Hc0 Hc1 x0.
- rewrite ltnNge in x; apply negbFE in x.
- rewrite leq_eqVlt in x; move: x => /orP [x | x].
- { move: Hwait => /eqP Hwait; contradict Hwait. apply eq_add_S; rewrite prednK.
- 2: exact WAIT_pos.
- move: x => /eqP x.
- by apply Logic.eq_sym. }
- { destruct c; simpl in *; contradict x.
- apply /negP.
- by rewrite -leqNgt. } }
- Qed.
-
- Lemma Request_ACT_bounded t ra:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- FIFO_request (Default_arbitrate t).(Implementation_State) == Some ra ->
- let tact := (Slot_start t + Next_cycle OACT_date) in
- (ACT_of_req ra tact) \in (Default_arbitrate tact).(Arbiter_Commands).
- Proof.
- intros Hrun Hreq; simpl.
- induction t.
- { by simpl in Hrun. }
- rewrite /Slot_start; simpl in *; unfold Next_state in *; simpl in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- { destruct r eqn:HPP; simpl in *.
- { done. }
- { clear Hrun IHt.
- rewrite /Next_state //=.
- assert (isIDLE (Default_arbitrate t).(Implementation_State)) as Hidle.
- { by rewrite Hs. }
- apply Request_starts_idle with (ra := r0) in Hidle.
- 3,2: rewrite Hs /FIFO_pending; (by apply index_head || by apply mem_head).
- rename Hidle into H; move: H => /andP [/andP [Hreq' Hc'] Hrun']; move: Hc' => /eqP Hc'.
- apply FIFO_add_counter with (d := ACT_date) in Hc' as H. destruct H as [Hrun'' Hc''].
- 3: rewrite /OCycle0 add0n //=; specialize FIFO_WAIT_GT_ACTp1; by apply ltnW.
- 2: done.
- apply Request_running_in_slot with (d := ACT_date) in Hreq' as Hreq''.
- 3: specialize FIFO_WAIT_GT_ACTp1; by apply ltnW.
- 2: by apply /eqP.
- rewrite -addn1 -addnA [1 + _]addnC addn1 in Hc'',Hrun'', Hreq''.
- rewrite FIFO_nextcycle_act_eq_actS.
- destruct (Default_arbitrate (t + ACT_date.+1)).(Implementation_State) eqn:Hs_act.
- { by simpl in Hrun''. }
- clear Hrun''; rewrite /FIFO_counter /OCycle0 add0n in Hc''.
- assert ((ACT_date == ACT_date) = true).
- { by rewrite eq_refl. }
- rewrite Hc'' H //= in_cons /ACT_of_req subn0.
- rewrite -addn1 -addnA [1 + _]addnC addn1 addnS.
- rewrite /FIFO_request inj_eq in Hreq''.
- 2: exact ssrfun.Some_inj.
- move: Hreq'' => /eqP Hreq''; rewrite -Hreq'' in Hreq.
- rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
- 2: exact ssrfun.Some_inj.
- by rewrite Hreq eq_refl orTb. }}
- { destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl in *.
- all: rewrite FIFO_nextcycle_act_eq_actS.
- 7: destruct r eqn:HPP; simpl.
- 7: discriminate Hrun.
- 7: {
- simpl in *; clear IHt Hrun; rewrite /Next_state.
- assert (isRUNNING (Default_arbitrate t).(Implementation_State)).
- { by rewrite Hs. }
- rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
- 2: exact ssrfun.Some_inj.
- apply Request_starts_running with (ra := ra) in H. move: H => /andP [/andP [Hreq' Hc']Hrun'].
- 4: rewrite Hs /FIFO_pending Hreq; apply index_head.
- 3: rewrite /FIFO_pending Hs Hreq; apply mem_head.
- 2: move: Hwait => /eqP Hwait; by rewrite /FIFO_counter Hs Hwait eq_refl.
- move: Hc' => /eqP Hc'.
- apply FIFO_add_counter with (d := ACT_date) in Hc' as H.
- 3: rewrite /OCycle0 add0n //=; specialize FIFO_WAIT_GT_ACTp1; by apply ltnW.
- 2: done.
- apply Request_running_in_slot with (d := ACT_date) in Hreq' as Hreq''.
- 3: specialize FIFO_WAIT_GT_ACTp1; by apply ltnW.
- 2: by apply /eqP.
- destruct H as [Hrun'' Hc''].
- rewrite -addn1 -addnA [1 + _]addnC addn1 in Hc'',Hrun'', Hreq''.
- destruct (Default_arbitrate (t + ACT_date.+1)).(Implementation_State) eqn:Hs_act.
- { by simpl in Hrun''. }
- clear Hrun''; rewrite /FIFO_counter /OCycle0 add0n in Hc''.
- assert ((ACT_date == ACT_date) = true).
- { by rewrite eq_refl. }
- rewrite Hc'' H //= in_cons /ACT_of_req subn0.
- rewrite -addn1 -addnA [1 + _]addnC addn1 addnS.
- rewrite /FIFO_request inj_eq in Hreq''.
- 2: exact ssrfun.Some_inj.
- move: Hreq'' => /eqP Hreq''; by rewrite -Hreq'' eq_refl orTb.
- }
- all: rewrite /Slot_start Hs in IHt.
- all: try (rewrite {1}/Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc).
- all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
- all: try (apply IHt in Hreq); try done.
- all: try (rewrite {1}/Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc).
- all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
- all: try (contradict x; by apply Bool.not_true_iff_false).
- all: try (contradict x0; by apply Bool.not_true_iff_false); try (clear x0 Hc0 Hc1).
- all: assert (t.+1 - c.+1 + ACT_date.+1 = t - c + Next_cycle OACT_date) as H.
- all: try (rewrite -FIFO_nextcycle_act_eq_actS -addn1 -[c.+1]addn1 subnDA -subnAC subn1 addn1 -pred_Sn; reflexivity).
- all: try (by rewrite H); clear H.
- all: try (move: Hact => /eqP Hact; rewrite Hact in x; contradict x;
- apply Bool.not_false_iff_true; by rewrite FIFO_WAIT_GT_ACTp1).
- all: try (move: Hcas => /eqP Hcas; rewrite Hcas in x; contradict x;
- apply Bool.not_false_iff_true; by rewrite FIFO_WAIT_GT_CASp1).
- clear Hrun IHt.
- rewrite ltnNge in x; apply negbFE in x.
- rewrite leq_eqVlt in x; move: x => /orP [x | x].
- { move: Hwait => /eqP Hwait; contradict Hwait. apply eq_add_S; rewrite prednK.
- 2: exact WAIT_pos.
- move: x => /eqP x.
- by apply Logic.eq_sym. }
- { destruct c; simpl in *; contradict x.
- apply /negP.
- by rewrite -leqNgt. } }
- Qed.
-
- Theorem Cmds_ACT_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- isACT a \/ isCAS a -> isACT b -> Same_Bank a b -> Before a b ->
- exists c, (c \in (Default_arbitrate t).(Arbiter_Commands)) && isPRE c && Same_Bank b c && Same_Bank a c && After c a && Before c b.
- Proof.
- intros Ha Hb iA iAb SB aBb.
- apply FIFO_ACT_date in Hb as H. destruct H as [Hcb [Hrun_b Hreq_b]].
- all: try done.
- destruct (Default_arbitrate b.(CDate)).(Implementation_State) eqn:Hsb.
- 1: by simpl in Hrun_b.
- rewrite -Hsb in Hreq_b.
- apply Request_PRE_bounded in Hreq_b.
- 2: by rewrite -Hsb in Hrun_b.
- rewrite /Slot_start Hsb in Hreq_b.
- exists (PRE_of_req b.(Request) (b.(CDate) - c)).
- rewrite /Same_Bank in SB; move: SB => /eqP SB.
- rewrite /isPRE /Same_Bank //= eq_refl andbT SB eq_refl andbT andbT /Before /After //=.
-
- (* Solving Before c b*)
- apply /andP; split.
- 2: {
- rewrite /FIFO_counter in Hcb; rewrite Hcb.
- rewrite ltn_subLR.
- 2: { rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b; rewrite -Hcb.
- rewrite /FIFO_counter Hsb in Hrun_b. by rewrite leq_eqVlt Hrun_b orbT.
- }
- rewrite addnC.
- apply nat_ltn_add; by rewrite FIFO_nextcycle_act_eq_actS.
- }
-
- (* Solving ~~ Before_at a c*)
- apply /andP; split.
- 2:{ destruct iA as [iAa | iCa].
- { apply FIFO_ACT_date in Ha as H. destruct H as [Hca [Hrun_a Hreq_a]].
- 2: done.
- rewrite -Hsb in Hcb.
- specialize FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) as HH; apply HH in Hrun_a as Hlt.
- all: try (done || by rewrite -Hsb in Hrun_b).
- clear HH. rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP H0 | H1].
- { rewrite -H0 -addnBA.
- 2: by destruct c; simpl; rewrite leq_eqVlt i orbT.
- apply nat_ltn_add; rewrite subn_gt0; destruct c; simpl; exact i. }
- { apply ltn_trans with (n := b.(CDate) - WAIT).
- 2: {
- apply ltn_sub2l.
- 2: destruct c; simpl; exact i.
- by rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b; rewrite /FIFO_counter Hsb in Hrun_b.
- }
- rewrite ltn_subRL addnC; exact H1.
- }
- }
- { apply FIFO_CAS_date in Ha as H. destruct H as [Hca [Hrun_a Hreq_a]].
- 2: done.
- rewrite -Hsb in Hcb.
- apply FIFO_add_counter with (d := Next_cycle OCAS_date - Next_cycle OACT_date) in Hcb as H.
- 3: { rewrite subnKC. by rewrite FIFO_next_cycle_cas_eq_casS FIFO_WAIT_GT_CASp1.
- rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite /CAS_date /ACT_date -addnS. by apply nat_ltn_add. }
- 2: by rewrite -Hsb in Hrun_b.
- destruct H as [Hrun_b' Hcb'].
- set (d := Next_cycle OCAS_date - Next_cycle OACT_date); fold d in Hrun_b',Hcb'.
- assert (Next_cycle OACT_date + d = Next_cycle OCAS_date).
- { unfold d; rewrite subnKC. reflexivity.
- rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS /CAS_date /ACT_date -addnS.
- by apply nat_ltn_add. }
- rewrite H in Hcb'.
- specialize FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate) + d) (c := Next_cycle OCAS_date) as HH.
- apply HH in Hrun_a as Hlt. clear HH.
- all: try done.
- 2 : { unfold Before in aBb; apply ltn_trans with (n := b.(CDate)).
- exact aBb. apply nat_ltn_add. unfold d.
- rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS /CAS_date /ACT_date prednK.
- 2: by rewrite lt0n T_RP_pos.
- rewrite subSn.
- 2: {
- rewrite -subn1 addnBAC.
- 2: by rewrite lt0n T_RP_pos.
- rewrite subn1. apply nat_ltn_leq_pred. apply nat_ltn_add.
- by rewrite lt0n T_RCD_pos.
- }
- trivial.
- }
- assert ((a.(CDate) < b.(CDate) - c) == (a.(CDate) + WAIT < b.(CDate) - c + WAIT)).
- { apply /eqP; by rewrite ltn_add2r. }
- move: H0 => /eqP H0; rewrite H0; clear H0.
- rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP Hlt | Hlt].
- { rewrite Hlt addnBAC.
- 2: { rewrite -Hsb in Hrun_b. apply Date_gt_counter in Hrun_b.
- rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT.
- }
- rewrite -addnBA.
- 2: by destruct c; simpl; rewrite leq_eqVlt i orbT.
- rewrite ltn_add2l ltn_subRL.
- rewrite /FIFO_counter Hsb in Hcb; rewrite Hcb; unfold d.
- rewrite subnKC.
- 2: { rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite /CAS_date /ACT_date -addnS. apply nat_ltnn_add. by specialize T_RCD_GT_ONE.
- }
- by rewrite FIFO_next_cycle_cas_eq_casS FIFO_WAIT_GT_CASp1. }
- { apply ltn_trans with (n := b.(CDate) + d). exact Hlt.
- rewrite addnBAC.
- 2: { rewrite -Hsb in Hrun_b. apply Date_gt_counter in Hrun_b.
- rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT.
- }
- rewrite -addnBA.
- 2: by destruct c; simpl; rewrite leq_eqVlt i orbT.
- rewrite ltn_add2l ltn_subRL.
- rewrite /FIFO_counter Hsb in Hcb; rewrite Hcb; unfold d.
- rewrite subnKC.
- 2: { rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite /CAS_date /ACT_date -addnS. apply nat_ltnn_add. by specialize T_RCD_GT_ONE.
- }
- by rewrite FIFO_next_cycle_cas_eq_casS FIFO_WAIT_GT_CASp1. }
+ 2: exact Hc.
+ rewrite Hreq' andbT.
+ apply FIFO_add_counter with (c:=OCycle0) (d:=d) in Hrun. destruct Hrun as [_ H].
+ 3: by apply /eqP.
+ 2: rewrite /OCycle0 //= add0n.
+ rewrite /OCycle0 add0n in H; by apply /eqP.
}
- }
-
- apply FIFO_in_the_past with (t := b.(CDate)).
- { by apply Cmd_in_trace. }
- apply FIFO_in_the_past with (t := b.(CDate) - c).
- { by apply leq_subr. }
- exact Hreq_b.
+ { assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun.
+ { by rewrite Hs. }
+ assert (c + (WAIT.-1 - c ) = WAIT.-1).
+ { rewrite subnKC. reflexivity. destruct c; simpl in *. clear Hs. lia. }
+ apply FIFO_add_counter with (c := c) (d := (WAIT.-1 -c)) in Hrun as H'. destruct H' as [Hrun' Hc'].
+ 3: by rewrite Hs.
+ 2: rewrite H ltn_predL; exact WAIT_pos.
+ rewrite H in Hc'.
+ apply Request_starts_running with (ra := ra) in Hrun' as H'. move: H' => /andP [/andP [Hreq Hc''] Hrun''].
+ 4: exact Hz.
+ 3: exact HP'.
+ 2: by rewrite Hc' eq_refl.
+ apply FIFO_add_counter with (c := OCycle0) (d:= d) in Hrun'' as H'. destruct H' as [Hrun''' Hc'''].
+ 3: by apply /eqP.
+ 2: by rewrite /OCycle0 add0n.
+ apply Request_running_in_slot with (d := d) in Hreq.
+ 3: exact Hd.
+ 2: exact Hc''.
+ rewrite Hreq andbT.
+ rewrite /OCycle0 add0n in Hc'''; by rewrite Hc''' eq_refl.
+ }
+ }
+ apply Counter_reaches with (i := index ra (FIFO_pending (Default_arbitrate t).(Implementation_State))) in HP'.
+ 3: by subst t.
+ 2: by rewrite Hz.
+ move: HP' => /andP [Hrun HC].
+ apply Request_processing_starts in HA as H. move: H => /andP [HP' Hiz].
+ fold t in Hrun,HC; rewrite Hz in Hrun,HC.
+ fold i in Hrun,HC; fold t in HP',Hiz.
+ rewrite Hz in HP',Hiz; fold i in HP',Hiz.
+ apply Request_starts_running with (ra := ra) in HC as H. move: H => /andP [/andP [Hreq HC'] H].
+ 4: by apply /eqP.
+ 3: exact HP'.
+ 2: exact Hrun.
+ apply FIFO_add_counter with (c := OCycle0) (d := d) in H. destruct H as [Hrun' HC''].
+ 3: by apply /eqP.
+ 2: rewrite /OCycle0 add0n; exact Hd.
+ rewrite /OCycle0 add0n in HC''.
+ apply Request_running_in_slot with (d := d) in Hreq as H.
+ 3: exact Hd.
+ 2: exact HC'.
+ set S' := (Default_arbitrate ((t + i).+1 + d)).(Implementation_State); simpl.
+ by fold S' in HC'',H; rewrite H; rewrite HC'' eq_refl.
Qed.
- Theorem Cmds_row_ok t b c:
- b \in (Default_arbitrate t).(Arbiter_Commands) -> c \in (Default_arbitrate t).(Arbiter_Commands) ->
- isCAS b -> isPRE c -> Same_Bank b c -> Before c b ->
- exists a, (a \in (Default_arbitrate t).(Arbiter_Commands))
- && isACT a && Same_Row a b && After a c && Before a b.
+ Lemma Request_CAS ta ra:
+ ra \in (Arrival_at ta)
+ -> let tc := (Requestor_slot_start ta + (index ra (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) * WAIT) + CAS_date).+1 in
+ (CAS_of_req ra tc.+1) \in (Default_arbitrate tc.+1).(Arbiter_Commands).
Proof.
- intros Hb Hc iCb iPc SB cBb.
- apply FIFO_CAS_date in Hb as H. destruct H as [Hcb [Hrun_b Hreq_b]].
- 2: done.
- destruct (Default_arbitrate b.(CDate)).(Implementation_State) eqn:Hsb.
- 1: by simpl in Hrun_b.
- rewrite -Hsb in Hreq_b. apply Request_ACT_bounded in Hreq_b.
- 2: by rewrite -Hsb in Hrun_b.
- rewrite /Slot_start Hsb in Hreq_b.
- exists (ACT_of_req b.(Request) (b.(CDate) - c0 + Next_cycle OACT_date)).
- rewrite /Same_Bank in SB; move: SB => /eqP SB.
- rewrite /isACT //= eq_refl andbT /Before /After //= /Same_Row eq_refl //= andbT.
+ intros HA.
+ apply Request_processing with (d := CAS_date) in HA as H; [ | exact WAIT_CAS].
+ move: H => /andP [HC HR]; clear HA.
+ rewrite addSn in HC, HR; set (tc := _ + CAS_date); fold tc in HC, HR.
+ destruct (Default_arbitrate tc.+1).(Implementation_State) eqn:Hs; simpl.
+ { by rewrite /FIFO_request in HR. }
+ simpl in Hs; rewrite Hs.
+ rewrite /Next_state.
+ rewrite /FIFO_counter in HC.
+ assert ((nat_of_ord c == ACT_date) = false) as Hact.
+ { move: HC => /eqP HC. by rewrite HC CAS_neq_ACT. }
+ rewrite //= Hact HC //= /CAS_of_req in_cons; apply /orP; left.
+ rewrite /FIFO_request inj_eq in HR. move: HR => /eqP HR.
+ 2: exact ssrfun.Some_inj.
+ by rewrite HR.
+ Qed.
- apply /andP; split.
- 2: {
- rewrite /FIFO_counter in Hcb; rewrite Hcb FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite -Hsb in Hrun_b.
- rewrite -subnA.
- 3: {
- apply Date_gt_counter in Hrun_b as H; rewrite Hsb /FIFO_counter Hcb FIFO_next_cycle_cas_eq_casS in H.
- apply ltn_trans with (m := CAS_date) in H. exact H. done. }
- 2: rewrite /CAS_date /ACT_date -addnS; by apply nat_ltn_add.
- rewrite ltn_subrL.
- apply FIFO_date_gt_0 in Hb; rewrite subn_gt0 Hb andbT -addn1 -[CAS_date.+1]addn1 leq_add2r.
- rewrite /CAS_date /ACT_date; apply nat_ltn_add; by rewrite lt0n T_RCD_pos.
+ Lemma Counter_at_running_slot_start ta c:
+ FIFO_counter (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) == c ->
+ isRUNNING (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) ->
+ c == WAIT.-1.
+ Proof.
+ intros Hc Hrun.
+ unfold Requestor_slot_start in *.
+ destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
+ { by rewrite Hs in Hrun. }
+ { clear Hrun.
+ assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as H.
+ { by rewrite Hs. }
+ assert (c0 + (WAIT.-1 - c0) = WAIT.-1).
+ { rewrite subnKC. reflexivity. destruct c0; simpl in *; clear Hs; lia. }
+ apply FIFO_add_counter with (c := c0) (d := (WAIT.-1 - c0)) in H as [Hrun Hc'].
+ 3: by rewrite Hs.
+ 2: rewrite H0; rewrite ltn_predL; exact WAIT_pos.
+ rewrite H0 in Hc'; by rewrite Hc' eq_sym in Hc.
}
-
- clear SB.
- apply /andP; split.
- 2: {
- apply FIFO_PRE_date in Hc as H. destruct H as [Hcc [Hrun_c Hreq_c]].
- 2: done.
- apply FIFO_add_counter with (d := Next_cycle OCAS_date) in Hcc as H. destruct H as [Hrun_c' Hcc'].
- 3: by rewrite /OCycle0 add0n FIFO_next_cycle_cas_eq_casS FIFO_WAIT_GT_CASp1.
- 2: done.
- set (d := Next_cycle OCAS_date).
- specialize FIFO_l_eq_bound_or with (ta := c.(CDate) + d) (tb := b.(CDate)) (c := d) as HH.
- apply HH in Hrun_c' as Hlt. clear HH.
- 4: unfold d; by rewrite Hsb.
- 3: by rewrite Hsb.
- 2: by rewrite /OCycle0 add0n in Hcc'; fold d in Hcc'.
- rewrite /FIFO_counter in Hcb; rewrite Hcb.
- destruct Hlt as [H0 | [H1 | H2]]; fold d.
- { rewrite -H0.
- rewrite addnBAC.
- 2: by rewrite addnC leq_addr.
- rewrite ltn_subRL addnC -addnA ltn_add2l.
- apply nat_ltn_add; by rewrite FIFO_nextcycle_act_eq_actS. }
- { rewrite leq_eqVlt in H1; move: H1 => /orP [/eqP H1 | H1].
- { rewrite -H1 -addnA -subnA.
- 3: rewrite -addnCA; by apply leq_addr.
- 2: { unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite /CAS_date -addnS; by apply nat_ltn_add. }
- rewrite ltn_subRL addnC ltn_add2l ltn_subLR.
- 2: { unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite /CAS_date -addnS; by apply nat_ltn_add. }
- rewrite -addnCA; apply nat_ltn_add; by rewrite addn_gt0 WAIT_pos orbT.
- }
- rewrite -subnA.
- 3: { rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b.
- rewrite /FIFO_counter Hsb Hcb in Hrun_b; fold d in Hrun_b.
- by rewrite leq_eqVlt Hrun_b orbT. }
- 2: { unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite /CAS_date -addnS; by apply nat_ltn_add. }
- rewrite ltn_subRL addnC.
- apply ltn_trans with (m := c.(CDate) + (d - Next_cycle OACT_date)) in H1. exact H1.
- rewrite -addnA ltn_add2l ltn_subLR.
- 2: { unfold d; rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite /CAS_date -addnS; by apply nat_ltn_add. }
- rewrite -addnCA; apply nat_ltn_add; by rewrite addn_gt0 WAIT_pos orbT. }
- { contradict H2; apply /negP; rewrite -ltnNge.
- unfold Before in cBb.
- rewrite addnC -ltn_subRL.
- apply ltn_trans with (n := b.(CDate)). exact cBb.
- rewrite ltn_subRL addnC ltn_add2l; unfold d; rewrite FIFO_next_cycle_cas_eq_casS.
- exact FIFO_WAIT_GT_CASp1. } }
-
- apply FIFO_in_the_past with (t := b.(CDate)).
- { by apply Cmd_in_trace. }
- apply FIFO_in_the_past with (t := b.(CDate) - c0 + Next_cycle OACT_date).
- { rewrite -subnA.
- 3: { rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b.
- rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT. }
- 2: { rewrite /FIFO_counter in Hcb; rewrite Hcb;
- rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS;
- rewrite /CAS_date -addnS; by apply nat_ltn_add. }
- apply leq_subr. }
- exact Hreq_b.
Qed.
- Theorem Cmds_initial t b:
- b \in (Default_arbitrate t).(Arbiter_Commands) -> isCAS b ->
- exists a, (a \in (Default_arbitrate t).(Arbiter_Commands)) && (isACT a) && (Same_Row a b) && (Before a b).
+ Lemma Request_PRE ta ra:
+ ra \in (Arrival_at ta)
+ -> let i := index ra (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) * WAIT in
+ let tc := ((Requestor_slot_start ta) + i).+1 in
+ (PRE_of_req ra tc) \in (Default_arbitrate tc).(Arbiter_Commands).
Proof.
- intros Hb iCb.
- apply FIFO_CAS_date in Hb as H. destruct H as [Hcb [Hrun_b Hreq_b]].
- 2: done.
- destruct (Default_arbitrate b.(CDate)).(Implementation_State) eqn:Hsb.
- 1: by simpl in Hrun_b.
- rewrite -Hsb in Hreq_b.
- apply Request_ACT_bounded in Hreq_b.
- 2: by rewrite -Hsb in Hrun_b.
- rewrite /Slot_start Hsb in Hreq_b.
- exists (ACT_of_req b.(Request) (b.(CDate) - c + Next_cycle OACT_date)).
- rewrite /isACT //= eq_refl andbT /Before /After //= /Same_Row eq_refl //= andbT.
+ intros HA.
- apply /andP; split.
- 2: {
- rewrite /FIFO_counter in Hcb; rewrite Hcb FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
- rewrite -Hsb in Hrun_b.
- rewrite -subnA.
- 3: {
- apply Date_gt_counter in Hrun_b as H; rewrite Hsb /FIFO_counter Hcb FIFO_next_cycle_cas_eq_casS in H.
- apply ltn_trans with (m := CAS_date) in H. exact H. done. }
- 2: rewrite /CAS_date /ACT_date -addnS; by apply nat_ltn_add.
- rewrite ltn_subrL.
- apply FIFO_date_gt_0 in Hb; rewrite subn_gt0 Hb andbT -addn1 -[CAS_date.+1]addn1 leq_add2r.
- rewrite /CAS_date /ACT_date; apply nat_ltn_add; by rewrite lt0n T_RCD_pos.
- }
+ apply Request_processing_starts in HA as HP; move: HP => /andP [HP HI].
+ set i := index _ _; fold i in HP,HI.
+ set t := Requestor_slot_start ta + i * WAIT; fold t in HP,HI.
- apply FIFO_in_the_past with (t := b.(CDate)).
- { by apply Cmd_in_trace. }
- apply FIFO_in_the_past with (t := b.(CDate) - c + Next_cycle OACT_date).
- { rewrite -subnA.
- 3: { rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b.
- rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT. }
- 2: { rewrite /FIFO_counter in Hcb; rewrite Hcb;
- rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS;
- rewrite /CAS_date -addnS; by apply nat_ltn_add. }
- apply leq_subr. }
- exact Hreq_b.
+ destruct i eqn:Hz. (* Case i = 0 *)
+ { rewrite mul0n //= addn0; subst t.
+ rewrite mul0n addn0 in HP,HI.
+ rewrite /Next_state.
+ destruct (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) eqn:Hs.
+ { rewrite /FIFO_pending in HP,HI.
+ destruct r eqn:HPP.
+ { discriminate HP. }
+ { destruct (ra == r0) eqn:Heq.
+ { simpl; move: Heq => /eqP Heq; rewrite /PRE_of_req in_cons Heq; apply /orP; left; by rewrite eq_refl. }
+ { rewrite eq_sym in Heq; by rewrite //= Heq in HI. }}}
+ { rewrite /FIFO_pending in HP,HI.
+ assert (FIFO_counter (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) == c).
+ { by rewrite Hs. }
+ apply Counter_at_running_slot_start in H.
+ 2: by rewrite Hs.
+ move: H => /eqP H; rewrite H FIFO_wait_neq_act FIFO_wait_neq_cas eq_refl.
+ destruct r eqn:HPP.
+ { discriminate HP. }
+ { destruct (r1 == ra) eqn:Heq.
+ { simpl; move: Heq => /eqP Heq; rewrite /PRE_of_req in_cons Heq; apply /orP; left; by rewrite eq_refl. }
+ { by rewrite //= Heq in HI. }}}}
+
+ apply Pending_on_arrival in HA as H.
+ apply Pending_requestor_slot_start with (tb := Requestor_slot_start ta) in H.
+ 3: by rewrite leqnn.
+ 2: { rewrite /Requestor_slot_start; destruct (Default_arbitrate ta).(Implementation_State).
+ by rewrite leqnn. by rewrite leq_addr. }
+ apply Counter_reaches with (i := i) in H. move: H => /andP [Hrun HC]; fold t in Hrun,HC.
+ 3: subst i; by rewrite leqnn.
+ 2: by rewrite Hz.
+
+ simpl; fold t; rewrite /Next_state.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
+ { destruct r eqn:HPP.
+ { simpl in HP; discriminate HP. }
+ { destruct (r0 == ra) eqn:Heq.
+ { by simpl; move: Heq => /eqP Heq; rewrite in_cons /PRE_of_req //= Heq eq_refl orTb. }
+ { by rewrite /FIFO_pending //= Heq in HI. }
+ }}
+ { unfold FIFO_pending in HP,HI. subst t; rewrite -Hz in Hs; rewrite Hs /FIFO_counter in HC; move: HC => /eqP HC.
+ rewrite HC FIFO_wait_neq_act FIFO_wait_neq_cas eq_refl.
+ destruct r eqn:HPP.
+ { discriminate HP. }
+ { destruct (r1 == ra) eqn:Heq.
+ { simpl; move: Heq => /eqP Heq; by rewrite in_cons /PRE_of_req //= Heq eq_refl orTb. }
+ { by rewrite /FIFO_pending //= Heq in HI. }
+ }
+ }
Qed.
+ Theorem Requests_handled ta ra:
+ ra \in (Arrival_at ta)
+ -> exists tc, (CAS_of_req ra tc) \in ((Default_arbitrate tc).(Arbiter_Commands)).
+ Proof.
+ intros HA.
+ apply Request_CAS in HA as H.
+ set tc := _.+1 in H.
+ exists (tc.+1).
+ exact H.
+ Qed.
(* ------------------------------------------------------------------ *)
(* --------------------- INSTANCES ---------------------------------- *)
@@ -2538,42 +2159,28 @@ Module FIFOPROOFS (SYS : SystemModule).
c.(CDate) > t -> c \notin (Default_arbitrate t).(Arbiter_Commands).
Proof.
intros.
- destruct (c \notin (Default_arbitrate t).(Arbiter_Commands)) eqn:Hni.
- { done. }
- { move : Hni => /negPn Hni. apply Cmd_in_trace in Hni.
- contradict Hni; apply /negP; by rewrite -ltnNge. }
+ destruct (c \notin (# t).(Arbiter_Commands)) eqn:Hni; [ done | ].
+ move : Hni => /negPn Hni; apply Cmd_in_trace in Hni.
+ contradict Hni; apply /negP; by rewrite -ltnNge.
Qed.
Lemma Default_arbitrate_cmds_uniq t:
- uniq ((Default_arbitrate t).(Arbiter_Commands)).
+ uniq ((# t).(Arbiter_Commands)).
Proof.
- induction t; simpl.
- { done. }
+ induction t; simpl; [ done | ].
rewrite /Next_state //=.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- 1: destruct r; simpl.
- 3: destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl.
- 9: destruct r; simpl.
- all: rewrite IHt andbT.
- all: assert (t < t.+1) as H0; try trivial.
- all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 NOP nullreq) (t := t) as H; simpl in H;
- apply H in H0; by rewrite H0).
- all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 PRE r) (t := t) as H; simpl in H;
- apply H in H0; by rewrite H0).
- all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 ACT r0) (t := t) as H; simpl in H;
- apply H in H0; by rewrite H0).
- all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 (Kind_of_req r0) r0) (t := t) as H; simpl in H;
- apply H in H0; by rewrite H0).
- Qed.
-
+ destruct_state t; simpl; rewrite IHt andbT;
+ assert (t < t.+1) as H0; try trivial;
+ apply Default_arbitrate_notin_cmd; simpl; lia.
+ Qed.
+
Lemma Default_arbitrate_cmds_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) ->
- cmd.(CDate) <= (Default_arbitrate t).(Arbiter_Time).
+ cmd \in (# t).(Arbiter_Commands) ->
+ cmd.(CDate) <= (# t).(Arbiter_Time).
Proof.
rewrite Default_arbitrate_time; apply Cmd_in_trace.
Qed.
- (* nat -> Trace *)
Program Definition FIFO_arbitrate t :=
mkTrace
(Default_arbitrate t).(Arbiter_Commands)
@@ -2601,8 +2208,9 @@ Module FIFOPROOFS (SYS : SystemModule).
(Cmds_initial t)
_.
Admit Obligations.
-
+
+
Global Instance FIFO_arbiter : Arbiter_t :=
mkArbiter AF FIFO_arbitrate Requests_handled Default_arbitrate_time_match.
-End FIFOPROOFS.
\ No newline at end of file
+End Proofs.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/FIFO/FIFO_sim.v b/framework/DRAM/Implementations/TS/FIFO/FIFO_sim.v
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/FIFO_sim.v
rename to framework/DRAM/Implementations/TS/FIFO/FIFO_sim.v
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/App.hs b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/App.hs
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/App.hs
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/App.hs
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/ForeignCommand.hsc b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/ForeignCommand.hsc
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/ForeignCommand.hsc
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/ForeignCommand.hsc
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/ForeignCommand_t.h b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/ForeignCommand_t.h
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/ForeignCommand_t.h
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/ForeignCommand_t.h
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/ForeignRequest.hsc b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/ForeignRequest.hsc
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/ForeignRequest.hsc
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/ForeignRequest.hsc
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/ForeignRequest_t.h b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/ForeignRequest_t.h
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/ForeignRequest_t.h
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/ForeignRequest_t.h
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/MCsimRequest.h b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/MCsimRequest.h
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/MCsimRequest.h
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/MCsimRequest.h
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/README.md b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/README.md
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/README.md
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/README.md
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/main.cpp b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/main.cpp
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/main.cpp
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/main.cpp
diff --git a/framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/makefile b/framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/makefile
similarity index 100%
rename from framework/DRAM/Implementations/FIFO/haskell_gencode_fifo/makefile
rename to framework/DRAM/Implementations/TS/FIFO/haskell_gencode_fifo/makefile
diff --git a/framework/DRAM/Implementations/FIFOImp2/FIFOImp2.v b/framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2.v
similarity index 100%
rename from framework/DRAM/Implementations/FIFOImp2/FIFOImp2.v
rename to framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2.v
diff --git a/framework/DRAM/Implementations/FIFOImp2/FIFOImp2Properties.v b/framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2Properties.v
similarity index 100%
rename from framework/DRAM/Implementations/FIFOImp2/FIFOImp2Properties.v
rename to framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2Properties.v
diff --git a/framework/DRAM/Implementations/FIFOImp2/FIFOImp2Test.v b/framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2Test.v
similarity index 100%
rename from framework/DRAM/Implementations/FIFOImp2/FIFOImp2Test.v
rename to framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2Test.v
diff --git a/framework/DRAM/Implementations/TDM/TDM.v b/framework/DRAM/Implementations/TS/TDM/TDM.v
similarity index 84%
rename from framework/DRAM/Implementations/TDM/TDM.v
rename to framework/DRAM/Implementations/TS/TDM/TDM.v
index 846ddad..b262d3e 100644
--- a/framework/DRAM/Implementations/TDM/TDM.v
+++ b/framework/DRAM/Implementations/TS/TDM/TDM.v
@@ -8,7 +8,7 @@ Section TDM.
Context {SYS_CFG : System_configuration}.
- #[local] Axiom DDR3: BANKGROUPS = 1.
+ (* #[local] Axiom DDR3: BANKGROUPS = 1. *)
Definition ACT_date := T_RP.+1.
Definition CAS_date := ACT_date + T_RCD.+1.
@@ -38,6 +38,8 @@ Section TDM.
Context {TDM_CFG : TDM_configuration}.
+ (* -------------------------------------------------------- *)
+ (* Helper lemmas *)
Lemma Last_cycle:
SL.-1 < SL.
Proof.
@@ -91,6 +93,7 @@ Section TDM.
Proof.
by rewrite /ACT_date -[T_RP.+1]addn1 addn_gt0 ltn0Sn orbT.
Qed.
+ (* -------------------------------------------------------- *)
Definition OZCycle := Ordinal SL_pos.
Definition OACT_date := Ordinal SL_ACT.
@@ -99,16 +102,15 @@ Section TDM.
Definition OZSlot := Ordinal SN_pos.
- Definition Slot_t :=
- ordinal_eqType SN.
+ Definition Slot_t := ordinal_eqType SN.
Instance REQESTOR_CFG : Requestor_configuration :=
{
Requestor_t := Slot_t
}.
- Definition Same_Slot (a b : Command_t) :=
- a.(Request).(Requestor) == b.(Request).(Requestor).
+ (* Definition Same_Slot (a b : Command_t) :=
+ a.(Request).(Requestor) == b.(Request).(Requestor). *)
Context {AF : Arrival_function_t}.
@@ -119,7 +121,7 @@ Section TDM.
pending requests. *)
Variant TDM_state_t :=
| IDLE : Slot_t -> Counter_t -> Requests_t -> TDM_state_t
- | RUNNING : Slot_t -> Counter_t -> Requests_t -> Request_t-> TDM_state_t.
+ | RUNNING : Slot_t -> Counter_t -> Requests_t -> Request_t -> TDM_state_t.
Definition TDM_state_eqdef (a b : TDM_state_t) :=
match a, b with
@@ -141,7 +143,6 @@ Section TDM.
}
destruct x, y; apply negbT in H; apply ReflectF;
try discriminate.
-
all: unfold not; intro BUG.
1: rewrite 2! negb_and in H.
2: rewrite 3! negb_and in H.
@@ -185,33 +186,18 @@ Section TDM.
else
fun _ => OZSlot) Logic.eq_refl.
- (* Enqueue newly arriving requests in the pending queue. *)
- Definition Enqueue (R P : Requests_t) :=
- P ++ R.
-
- (* Remove a request from the pending queue that is about to be processed. *)
- Definition Dequeue r (P : Requests_t) :=
- rem r P.
-
(* The set of pending requests of a slot *)
- Definition Pending_of s (P : Requests_t) :=
- [seq r <- P | r.(Requestor) == s].
+ Definition Pending_of s (P : Requests_t) := [seq r <- P | r.(Requestor) == s].
- Definition Init_state R :=
- IDLE OZSlot OZCycle (Enqueue R [::]).
+ Definition Init_state R := IDLE OZSlot OZCycle (Enqueue R [::]).
Hint Unfold PRE_of_req : core.
Hint Unfold ACT_of_req : core.
Hint Unfold CAS_of_req : core.
- (* Axiom ACommand_t : Command_t. *)
-
- Definition nullreq :=
- mkReq OZSlot 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
-
(* The next-state function of the arbiter *)
- Definition Next_state R (AS : TDM_state_t) : (TDM_state_t * (Command_kind_t * Request_t)) :=
- match AS return (TDM_state_t * (Command_kind_t * Request_t)) with
+ Definition Next_state R (AS : TDM_state_t) : (TDM_state_t * Command_kind_t) :=
+ match AS with
| IDLE s c P => (* Currently no request is processed *)
let P' := Enqueue R P in (* enqueue newly arriving requests *)
let s' := Next_slot s c in (* advance slot counter (if needed) *)
@@ -219,28 +205,30 @@ Section TDM.
if (c == OZCycle) then
match Pending_of s P with (* Check if a request is pending *)
| [::] => (* No? Continue with IDLE *)
- (IDLE s' c' P', (NOP, nullreq))
+ (IDLE s' c' P', NOP)
| r::_ => (* Yes? Emit PRE, dequeue request, and continue with RUNNING *)
- (RUNNING s' c' (Enqueue R (Dequeue r P)) r, (PRE,r))
+ (RUNNING s' c' (Enqueue R (Dequeue r P)) r, PRE r)
end
- else (IDLE s' c' P', (NOP, nullreq))
+ else (IDLE s' c' P', NOP)
| RUNNING s c P r => (* Currently a request is processed *)
let P' := Enqueue R P in (* enqueue newly arriving requests *)
let s' := Next_slot s c in (* advance slot counter (if needed) *)
let c' := Next_cycle c in (* advance slot counter (if needed) *)
if c == OACT_date then (* need to emit the ACT command *)
- (RUNNING s' c' P' r, (ACT, r))
+ (RUNNING s' c' P' r, ACT r)
else if c == OCAS_date then (* need to emit the CAS command *)
- (RUNNING s' c' P' r, (Kind_of_req r, r))
+ (RUNNING s' c' P' r, (Kind_of_req r) r)
else if c == OLastCycle then (* return to IDLE state *)
- (IDLE s' c' P', (NOP, nullreq))
+ (IDLE s' c' P', NOP)
else
- (RUNNING s' c' P' r, (NOP, nullreq))
+ (RUNNING s' c' P' r, NOP)
end.
Global Instance TDM_implementation : Implementation_t :=
mkImplementation Init_state Next_state.
+ (* -------------------------------------------------------------- *)
+ (* Helper functions *)
Definition TDM_counter (AS : State_t) :=
match AS with
| IDLE _ c _ => c
@@ -272,7 +260,7 @@ Section TDM.
end.
#[local] Axiom Private_Mapping :
- forall a b, Same_Bank a b ->
+ forall a b, get_bank a == get_bank b ->
nat_of_ord (TDM_slot (Default_arbitrate b.(CDate)).(Implementation_State)) =
nat_of_ord (TDM_slot (Default_arbitrate a.(CDate)).(Implementation_State)).
diff --git a/framework/DRAM/Implementations/TDM/TDMREF.v b/framework/DRAM/Implementations/TS/TDM/TDMREF.v
similarity index 100%
rename from framework/DRAM/Implementations/TDM/TDMREF.v
rename to framework/DRAM/Implementations/TS/TDM/TDMREF.v
diff --git a/framework/DRAM/Implementations/TDM/TDM_extraction.v b/framework/DRAM/Implementations/TS/TDM/TDM_extraction.v
similarity index 100%
rename from framework/DRAM/Implementations/TDM/TDM_extraction.v
rename to framework/DRAM/Implementations/TS/TDM/TDM_extraction.v
diff --git a/framework/DRAM/Implementations/TDM/TDM_proofs.v b/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v
similarity index 100%
rename from framework/DRAM/Implementations/TDM/TDM_proofs.v
rename to framework/DRAM/Implementations/TS/TDM/TDM_proofs.v
diff --git a/framework/DRAM/Implementations/TDM/TDM_sim.v b/framework/DRAM/Implementations/TS/TDM/TDM_sim.v
similarity index 100%
rename from framework/DRAM/Implementations/TDM/TDM_sim.v
rename to framework/DRAM/Implementations/TS/TDM/TDM_sim.v
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/App.hs b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/App.hs
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/App.hs
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/App.hs
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/ForeignCommand.hsc b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/ForeignCommand.hsc
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/ForeignCommand.hsc
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/ForeignCommand.hsc
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/ForeignCommand_t.h b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/ForeignCommand_t.h
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/ForeignCommand_t.h
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/ForeignCommand_t.h
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/ForeignRequest.hsc b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/ForeignRequest.hsc
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/ForeignRequest.hsc
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/ForeignRequest.hsc
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/ForeignRequest_t.h b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/ForeignRequest_t.h
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/ForeignRequest_t.h
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/ForeignRequest_t.h
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/MCsimRequest.h b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/MCsimRequest.h
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/MCsimRequest.h
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/MCsimRequest.h
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/README.md b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/README.md
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/README.md
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/README.md
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/main.cpp b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/main.cpp
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/main.cpp
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/main.cpp
diff --git a/framework/DRAM/Implementations/TDM/haskell_gencode_tdm/makefile b/framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/makefile
similarity index 100%
rename from framework/DRAM/Implementations/TDM/haskell_gencode_tdm/makefile
rename to framework/DRAM/Implementations/TS/TDM/haskell_gencode_tdm/makefile
diff --git a/framework/DRAM/_CoqProject b/framework/DRAM/_CoqProject
index b65f6c8..77ada9d 100644
--- a/framework/DRAM/_CoqProject
+++ b/framework/DRAM/_CoqProject
@@ -1,11 +1,19 @@
INSTALLDEFAULTROOT = DRAM
-Q . DRAM
+Core/Util.v
Core/System.v
Core/Address.v
Core/Requests.v
Core/Commands.v
-Core/BankMachine.v
Core/Trace.v
Core/Arbiter.v
-Core/ImplementationInterface.v
\ No newline at end of file
+Core/ImplementationInterface.v
+Core/BankMachine.v
+Core/InterfaceSubLayer.v
+
+Implementations/TS/FIFO/FIFO.v
+
+Implementations/BM/FIFOimpSL/FIFOimpSL.v
+Implementations/BM/RRimpSL/RRimpSL.v
+Implementations/BM/TDMimpSL/TDMimpSL.v
\ No newline at end of file
--
GitLab