From 646a29db17426a54e9204db923ce89524ad55e44 Mon Sep 17 00:00:00 2001
From: Felipe Lisboa <lisboafelipe5@gmail.com>
Date: Mon, 8 Apr 2024 13:12:24 +0200
Subject: [PATCH] Changed axiom about private bank mapping in TDM; Renamed
things to TDMShelve
---
.../dsTDMimpSL.v => TDMShelve/TDMShelve.v} | 82 +++++++++----------
.../TDMShelve_sim.v} | 12 +--
framework/DRAM/Implementations/TS/TDM/TDM.v | 23 +++++-
.../DRAM/Implementations/TS/TDM/TDM_proofs.v | 3 +-
framework/DRAM/_CoqProject | 2 +-
5 files changed, 72 insertions(+), 50 deletions(-)
rename framework/DRAM/Implementations/BM/{dsTDMimpSL/dsTDMimpSL.v => TDMShelve/TDMShelve.v} (88%)
rename framework/DRAM/Implementations/BM/{dsTDMimpSL/dsTDMimpSL_sim.v => TDMShelve/TDMShelve_sim.v} (96%)
diff --git a/framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL.v b/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve.v
similarity index 88%
rename from framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL.v
rename to framework/DRAM/Implementations/BM/TDMShelve/TDMShelve.v
index f4226ce..eeafdf5 100644
--- a/framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL.v
+++ b/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve.v
@@ -6,7 +6,7 @@ From Coq Require Import BinIntDef List Program Equality.
From DRAM Require Export InterfaceSubLayer.
From Hammer Require Import Hammer.
-Section dsTDMimpSL.
+Section TDMShelve.
Context {SYS_CFG : System_configuration}.
@@ -15,7 +15,7 @@ Section dsTDMimpSL.
2) See if the thing based on u_map is really necessary to track pending requests
*)
- Class dsTDM_configuration := mkTDMCFG {
+ Class TDMShelve_configuration := mkTDMCFG {
SN : nat;
SN_gt_1 : SN > 1;
@@ -44,7 +44,7 @@ Section dsTDMimpSL.
SL_WR_to_PRE : T_WL + T_BURST + T_WR - 1 <= SL;
}.
- Context {dsTDM_CFG : dsTDM_configuration}.
+ Context {TDMShelve_CFG : TDMShelve_configuration}.
(* ------------------------------------------------------------------ *)
(* ------------------ Slot and Cycle Counters ----------------------- *)
@@ -57,18 +57,18 @@ Section dsTDMimpSL.
Definition OZSlot := Ordinal SN_pos.
Definition O1Slot := Ordinal SN_gt_1.
- Definition dsTDM_counter_t := ordinal_eqType SL.
+ Definition TDMShelve_counter_t := ordinal_eqType SL.
Definition OZCycle := Ordinal SL_pos.
(* Increment counter for cycle offset (with wrap-arround). *)
- Definition Next_cycle (c : dsTDM_counter_t) : dsTDM_counter_t :=
+ Definition Next_cycle (c : TDMShelve_counter_t) : TDMShelve_counter_t :=
let nextc := c.+1 < SL in
- (if nextc as X return (nextc = X -> dsTDM_counter_t) then
+ (if nextc as X return (nextc = X -> TDMShelve_counter_t) then
fun (P : nextc = true) => Ordinal (P : nextc)
else
fun _ => OZCycle) Logic.eq_refl.
- Definition Next_slot (s : Slot_t) (c : dsTDM_counter_t) : Slot_t :=
+ Definition Next_slot (s : Slot_t) (c : TDMShelve_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
@@ -87,7 +87,7 @@ Section dsTDMimpSL.
(* ------------------------------------------------------------------ *)
Definition RequestorID_t := {id : nat | id < Treq}.
- Record dsTDM_requestor := mkRequestor {
+ Record TDMShelve_requestor := mkRequestor {
(* Critical requestors have an associated slot, NC requestors do not *)
ReqSlot : option Slot_t;
@@ -98,17 +98,17 @@ Section dsTDMimpSL.
Slot_matches_ID : forall slt, ReqSlot = Some slt -> ` ID = nat_of_ord slt
}.
- Local Definition dsTDM_requestor_eqdef (a b : dsTDM_requestor) :=
+ Local Definition TDMShelve_requestor_eqdef (a b : TDMShelve_requestor) :=
(a.(ReqSlot) == b.(ReqSlot)) && (a.(ID) == b.(ID)).
- Lemma dsTDM_requestor_eqn : Equality.axiom dsTDM_requestor_eqdef.
+ Lemma TDMShelve_requestor_eqn : Equality.axiom TDMShelve_requestor_eqdef.
Admitted.
- Canonical dsTDM_requestor_eqMixin := EqMixin dsTDM_requestor_eqn.
- Canonical dsTDM_requestor_eqType := Eval hnf in EqType dsTDM_requestor dsTDM_requestor_eqMixin.
+ Canonical TDMShelve_requestor_eqMixin := EqMixin TDMShelve_requestor_eqn.
+ Canonical TDMShelve_requestor_eqType := Eval hnf in EqType TDMShelve_requestor TDMShelve_requestor_eqMixin.
#[global] Instance REQUESTOR_CFG : Requestor_configuration := {
- Requestor_t := dsTDM_requestor_eqType
+ Requestor_t := TDMShelve_requestor_eqType
}.
Definition isCriticalRequestor (r : RequestorID_t) := ` r < SN.
@@ -136,10 +136,10 @@ Section dsTDMimpSL.
(* The total number of non-critical requestors *)
Definition NCreq := Treq - SN.
- Record dsTDM_internal_state := mkdsTDM_internal_state {
+ Record TDMShelve_internal_state := mkTDMShelve_internal_state {
(* Typical TDM slot and cycle counters *)
Slot : Slot_t;
- Counter : dsTDM_counter_t;
+ Counter : TDMShelve_counter_t;
(* Who has the grant to issue commands *)
Grant : option RequestorID_t;
(* Both critical and non-critical have associated deadlines *)
@@ -150,7 +150,7 @@ Section dsTDMimpSL.
Slack : { slack_cnts : seq.seq nat | seq.size slack_cnts == SN };
}.
- #[global] Instance SCH_ST : SchedulerInternalState := mkSIS dsTDM_internal_state.
+ #[global] Instance SCH_ST : SchedulerInternalState := mkSIS TDMShelve_internal_state.
(* Pick the first command from a given request *)
Definition Pick_cmd_from_requestorID
@@ -163,10 +163,10 @@ Section dsTDMimpSL.
| _ => false
end) map in seq.head NOP f.
- Definition dsTDM_schedule
+ Definition TDMShelve_schedule
(map : ReqCmdMap_t)
(SS : SystemState_t)
- (TDM_st : dsTDM_internal_state) : Command_kind_t :=
+ (TDM_st : TDMShelve_internal_state) : Command_kind_t :=
match TDM_st.(Grant) with
| None => NOP
| Some requestor_id => Pick_cmd_from_requestorID map requestor_id
@@ -227,7 +227,7 @@ Section dsTDMimpSL.
Definition checkIfPendingFromSlot (u_map : seq Command_kind_t) (s : Slot_t) :=
checkIfPendingFromID u_map (` (Slot_to_RequestorID s)).
-
+
(* let f := seq.find (fun cmd =>
match cmd with
| CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r =>
@@ -304,14 +304,14 @@ Section dsTDMimpSL.
Definition InitialArrivals :=
exist (fun (s : seq bool) => seq.size s == Treq) (repeat false _) (repeat_size false Treq).
- Definition InitSchState (cmd_map : ReqCmdMap_t) := mkdsTDM_internal_state
+ Definition InitSchState (cmd_map : ReqCmdMap_t) := mkTDMShelve_internal_state
OZSlot OZCycle None InitialDeadlines InitialArrivals InitialSlack.
(* ------------------------------------------------------------------ *)
(* ----------- Defining update functions ---------------------------- *)
(* ------------------------------------------------------------------ *)
Program Definition EDF
- (TDM_st : dsTDM_internal_state)
+ (TDM_st : TDMShelve_internal_state)
(requestors : seq (option RequestorID_t)) : option RequestorID_t :=
foldr (fun i s =>
match s, i with
@@ -330,16 +330,16 @@ Section dsTDMimpSL.
(isCriticalRequestor s) && (min_deadline <= SL)) then Some s
(* (min_deadline <= SL + (SL - TDM_st.(Counter)))) then s *)
else (
- if (cur_deadline == 0) then Some i else(
- if (cur_deadline < min_deadline) then Some i else Some s)
+ (* if (cur_deadline == 0) then Some i else( *)
+ if (cur_deadline < min_deadline) then Some i else Some s
)
)
end
) None requestors.
- Definition EDF_choice
+ Definition BankFiltering
(u_map : ReqCmdMap_t)
- (TDM_st : dsTDM_internal_state) : option RequestorID_t :=
+ (TDM_st : TDMShelve_internal_state) : option RequestorID_t :=
let cnt := TDM_st.(Counter) in
let slack := TDM_st.(Slack) in
let deadl := TDM_st.(Deadlines) in
@@ -367,31 +367,31 @@ Section dsTDMimpSL.
Definition UpdateGrant
(u_map : ReqCmdMap_t)
(sch_cmd : Command_kind_t)
- (TDM_st : dsTDM_internal_state) : option RequestorID_t :=
+ (TDM_st : TDMShelve_internal_state) : option RequestorID_t :=
let slt := TDM_st.(Slot) in
let grant := TDM_st.(Grant) in
let cur_slack := getSlackFromSlot TDM_st slt in
let cnt := TDM_st.(Counter) in
if (cnt == OZCycle) then ( (* Beginning of slot -> might abort requests *)
match grant with
- | None => if (u_map == [::]) then None else (EDF_choice u_map TDM_st) (* EDF (implement choice based on slack inside of EDF function) *)
+ | None => if (u_map == [::]) then None else (BankFiltering u_map TDM_st) (* EDF (implement choice based on slack inside of EDF function) *)
| Some requestor_id => (* May be preempted or not *)
match checkIfPendingFromSlot u_map slt with
- | false => if (isCAS_cmdkind sch_cmd) then None else (EDF_choice u_map TDM_st)
+ | false => if (isCAS_cmdkind sch_cmd) then None else (BankFiltering u_map TDM_st)
| true =>
let preq := Slot_to_RequestorID slt in
let preq_deadl := getDeadlineFromID TDM_st (` preq) in
if (preq_deadl <= SL)
- then (Some preq) (* have to abort ! *)
+ then (Some preq) (* have to abort ! *) (* Rule 1 *)
else (
- if (isCAS_cmdkind sch_cmd) then None else (EDF_choice u_map TDM_st)
+ if (isCAS_cmdkind sch_cmd) then None else (BankFiltering u_map TDM_st)
)
- (* EDF_choice u_map TDM_st) (Some requestor_id) *)
+ (* BankFiltering u_map TDM_st) (Some requestor_id) *)
end
end
) else ( (* Middle of the slot - EDF rules when a scheduling decision comes *)
- match grant with
- | None => if (u_map == [::]) then None else (EDF_choice u_map TDM_st)
+ match grant with (* Rule 4 *)
+ | None => if (u_map == [::]) then None else (BankFiltering u_map TDM_st)
| Some requestor_id =>
if (isCAS_cmdkind sch_cmd) then None else (Some requestor_id)
end
@@ -458,7 +458,7 @@ Section dsTDMimpSL.
) All_C_requestors) (size_map_iota _ _ _).
Definition UpdatSchState sch_cmd cmd_map (SS : SystemState_t) TDM_st :=
- mkdsTDM_internal_state
+ mkTDMShelve_internal_state
(Next_slot TDM_st.(Slot) TDM_st.(Counter))
(Next_cycle TDM_st.(Counter))
(UpdateGrant cmd_map sch_cmd TDM_st)
@@ -476,22 +476,22 @@ Section dsTDMimpSL.
rewrite H; done.
Qed.
- #[global] Program Instance dsTDM : Scheduler_t :=
- mkScheduler dsTDM_schedule _ _ _ InitSchState UpdatSchState.
+ #[global] Program Instance TDMShelve : Scheduler_t :=
+ mkScheduler TDMShelve_schedule _ _ _ InitSchState UpdatSchState.
Next Obligation.
- unfold dsTDM_schedule.
+ unfold TDMShelve_schedule.
destruct SCH_ST0.(Grant); [ | reflexivity].
unfold Pick_cmd_from_requestorID; simpl; reflexivity.
Defined.
Next Obligation.
- unfold dsTDM_schedule; destruct SCH_ST0.(Grant);
+ unfold TDMShelve_schedule; destruct SCH_ST0.(Grant);
[ | right; reflexivity ].
unfold Pick_cmd_from_requestorID; simpl.
destruct hd; simpl;
try destruct (_ == r); simpl; try (by left; reflexivity); by right; reflexivity.
Defined.
Next Obligation.
- unfold dsTDM_schedule; destruct SCH_ST0.(Grant);
+ unfold TDMShelve_schedule; destruct SCH_ST0.(Grant);
[ | left; reflexivity ].
unfold Pick_cmd_from_requestorID;
induction m; simpl; [ left; reflexivity | ];
@@ -507,9 +507,9 @@ Section dsTDMimpSL.
#[global] Existing Instance ImplementationSubLayer.
- Definition dsTDM_arbitrate t :=
+ Definition TDMShelve_arbitrate t :=
@mkTestTrace SYS_CFG REQUESTOR_CFG
((Default_arbitrate t).(Arbiter_Commands))
((Default_arbitrate t).(Arbiter_Time)).
-End dsTDMimpSL.
\ No newline at end of file
+End TDMShelve.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL_sim.v b/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve_sim.v
similarity index 96%
rename from framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL_sim.v
rename to framework/DRAM/Implementations/BM/TDMShelve/TDMShelve_sim.v
index 07641af..cbf279c 100644
--- a/framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL_sim.v
+++ b/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve_sim.v
@@ -2,9 +2,9 @@ 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 dsTDMimpSL.
+From DRAM Require Import TDMShelve.
-Section dsTDMimpSL_sim.
+Section TDMShelve_sim.
Program Instance SYS_CFG : System_configuration :=
{
@@ -63,7 +63,7 @@ Section dsTDMimpSL_sim.
T_RFC := 280; (* 280 [Page 36] *)
}.
- (* The one defined in dsTDMimpSL *)
+ (* The one defined in TDMShelve *)
Existing Instance REQUESTOR_CFG.
(* The one defined in TDMimpSL *)
@@ -78,7 +78,7 @@ Section dsTDMimpSL_sim.
Instance SCH_OPT : SchedulingOptions_t := mkSCH_OPT opage.
(* There has to be at least two requestors *)
- Program Instance TDM_CFG : dsTDM_configuration := mkTDMCFG
+ Program Instance TDM_CFG : TDMShelve_configuration := mkTDMCFG
2 (* SN *)
_(* SN_gt 1*)
27 (* SL *)
@@ -232,7 +232,7 @@ Section dsTDMimpSL_sim.
}.
(* Ignore proofs for computing *)
- Definition compstate (sch : dsTDM_internal_state) : compState :=
+ Definition compstate (sch : TDMShelve_internal_state) : compState :=
mkcompState
(nat_of_ord sch.(Slot))
(nat_of_ord sch.(Counter))
@@ -244,7 +244,7 @@ Section dsTDMimpSL_sim.
(* 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 dsTDM_arbiter : TestArbiter_t := mkTestArbiter AF dsTDM_arbitrate.
+ Instance TDMShelve_arbiter : TestArbiter_t := mkTestArbiter AF TDMShelve_arbitrate.
Eval vm_compute in (Default_arbitrate 270).(Arbiter_Commands).
diff --git a/framework/DRAM/Implementations/TS/TDM/TDM.v b/framework/DRAM/Implementations/TS/TDM/TDM.v
index b262d3e..70eace1 100644
--- a/framework/DRAM/Implementations/TS/TDM/TDM.v
+++ b/framework/DRAM/Implementations/TS/TDM/TDM.v
@@ -260,8 +260,29 @@ Section TDM.
end.
#[local] Axiom Private_Mapping :
- forall a b, get_bank a == get_bank b ->
+ forall t a b,
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ Same_Bank a b <->
nat_of_ord (TDM_slot (Default_arbitrate b.(CDate)).(Implementation_State)) =
nat_of_ord (TDM_slot (Default_arbitrate a.(CDate)).(Implementation_State)).
+ Locate not_iff_compat.
+
+ Lemma Private_Mapping_ :
+ forall t a b,
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ ~ Same_Bank a b ->
+ nat_of_ord (TDM_slot (Default_arbitrate b.(CDate)).(Implementation_State)) !=
+ nat_of_ord (TDM_slot (Default_arbitrate a.(CDate)).(Implementation_State)).
+ Proof.
+ specialize Private_Mapping as PM; unfold Same_Bank in *.
+ intros t a b Ha Hb; specialize (PM t a b Ha Hb).
+ apply not_iff_compat in PM.
+ intros; apply /eqP; apply PM; exact H.
+ Qed.
+
+ Locate not_iff_compat.
+
End TDM.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v b/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v
index d959f35..c2555a2 100644
--- a/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v
+++ b/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v
@@ -767,7 +767,8 @@ Section TDMPROOFS.
apply PRE_modulo_date in Hb_in as Hb.
2: exact iPb; clear iPb.
rewrite !Time_counter_modulo in Hb,Ha.
- apply TDM.Private_Mapping in sB.
+ specialize (TDM.Private_Mapping t a b Ha_in Hb_in) as [Hsb _ ].
+ apply Hsb in sB.
set (d := SL.-1 - Next_cycle OCAS_date).
set (q := (Next_cycle OCAS_date - Next_cycle OZCycle)).
diff --git a/framework/DRAM/_CoqProject b/framework/DRAM/_CoqProject
index ddea252..f3a21dd 100644
--- a/framework/DRAM/_CoqProject
+++ b/framework/DRAM/_CoqProject
@@ -20,4 +20,4 @@ Implementations/TS/FIFOREF/FIFOREF.v
Implementations/BM/FIFOimpSL/FIFOimpSL.v
Implementations/BM/RRimpSL/RRimpSL.v
Implementations/BM/TDMimpSL/TDMimpSL.v
-Implementations/BM/dsTDMimpSL/dsTDMimpSL.v
\ No newline at end of file
+Implementations/BM/TDMShelve/TDMShelve.v
\ No newline at end of file
--
GitLab