From cd46d1a2b04c96ebabe7acad2c6dbaaef5bbb7eb Mon Sep 17 00:00:00 2001
From: Felipe <flisboa@telecom-paris.fr>
Date: Sat, 20 Feb 2021 12:11:59 +0100
Subject: [PATCH] [TLA+,WIP] - Complete model
---
TLAplus/TDMv3/TDMv3.tla | 165 ++++++++++++++++++++++++++++++++++++++++
1 file changed, 165 insertions(+)
create mode 100644 TLAplus/TDMv3/TDMv3.tla
diff --git a/TLAplus/TDMv3/TDMv3.tla b/TLAplus/TDMv3/TDMv3.tla
new file mode 100644
index 0000000..540f6c9
--- /dev/null
+++ b/TLAplus/TDMv3/TDMv3.tla
@@ -0,0 +1,165 @@
+------------------------------- MODULE TDMv3 -------------------------------
+EXTENDS Naturals, FiniteSets, Sequences, SequencesExt
+
+(***************************************************************************)
+(* Utility functions *)
+(***************************************************************************)
+Max(S) == CHOOSE x \in S : \A y \in S : x >= y
+Min(S) == CHOOSE x \in S : \A y \in S : x =< y
+ModuloSum(a,b,max) == IF a + b =< max THEN a + b ELSE max - ((a+b)%max)
+
+CONSTANTS
+ CrRq, \* The set of critical requestors
+ NCrRq, \* The set of non-critical requestors
+ AllBanks, \* The set of DRAM private banks
+ Mapping, \* Bank Adress Maping
+ TDM_Slot, \* The length of the TDM slot
+ CMDS, \* The set of possible DRAM commands
+ Queue_Capacity \* The capacity of the request queue
+
+\*This produces a function that maps requestors to banks
+Requestors == CrRq \cup NCrRq
+tMapping == SetToSeq(Mapping)
+BankMapping == [req \in Requestors |-> tMapping[req]]
+
+ASSUME
+ /\ Cardinality(Requestors) = Cardinality(Mapping)
+
+\*Time passing characteristic
+time_limit == 50
+time_increment == 5
+
+NumberOfSlots == Cardinality(CrRq)
+
+(***************************************************************************)
+(* In TLA+ language, arrays are functions, and can be also seen as a hash *)
+(* map. A record is a analogue to a data structure, where which field is *)
+(* also a function. So, it can also be seen as a two variable function, *)
+(* or a matrix. And finally, in this module, we have a tuple (or *)
+(* sequence) of records, which is analogue to 3d function *)
+(***************************************************************************)
+
+VARIABLES
+ time, \* Natural : represents time evolution
+ continuation, \* Boolean : flag that controls the switching between control and time passing
+ request_queue, \* Tuple of records / 3d function / array of records : represents a queue storing all untreated requests
+ request_count, \* Natural : total number of requests in the system (that have arrived)
+ slot_count, \* Natural : total number of TDM slots that have elapsed
+ slot_owner, \* Natural : current owner of the TDM slot
+ row_buffer, \* Function : maps banks into row buffer situation (open or closed)
+ slack, \* Function : maps critical requests into natural numbers (representing amount of slack they have)
+ bank_state \* Function : maps banks into last DRAM command issued
+
+vars == <<time,continuation,request_queue,request_count,slot_count,slot_owner,row_buffer,slack,bank_state>>
+
+TypeOK ==
+ /\ time \in Nat
+ /\ continuation \in {TRUE,FALSE}
+ /\ request_count \in Nat
+ /\ slot_count \in Nat
+ /\ slot_owner \in Nat
+ /\ row_buffer \in [AllBanks -> {"OPEN","CLOSED"}]
+ /\ slack \in [CrRq -> Nat]
+ /\ bank_state \in [AllBanks -> CMDS]
+
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Init state predicate *)
+(***************************************************************************)
+Init ==
+ /\ time = 0
+ /\ continuation = TRUE
+ /\ request_queue = <<>>
+ /\ request_count = 0
+ /\ slot_count = 1
+ /\ slot_owner = 1
+ /\ row_buffer = [b \in AllBanks |-> "CLOSED"]
+ /\ slack = [req \in CrRq |-> 0]
+ /\ bank_state = [b \in AllBanks |-> "NOP"]
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Actions that representing the issuing of DRAM commands *)
+(***************************************************************************)
+IssueACT(bank) == TRUE
+IssueRD(bank) == TRUE
+IssueWR(bank) == TRUE
+IssuePRE(bank) == TRUE
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* This action has to do the following things 1. Decide which is the next *)
+(* request (on the request queue) is to be treated 2. Decide which *)
+(* is the order of commands that has to be issued for that request 3. *)
+(* Decide to leave the row buffer open or closed based on the amount of *)
+(* slack gained. *)
+(***************************************************************************)
+treat_request == TRUE
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Actions that model the arrival of new tasks into the system. They are *)
+(* stored in the request queue. *)
+(***************************************************************************)
+\* Assuming for now that there there are only critical requests in the system
+\* This is the deadline calculation for critical tasks, that acumulate slack
+request_arrival(req,ty,hm,arrival_rate) ==
+LET so_did == IF slack[req] >= (slot_count*TDM_Slot - time)
+ THEN ModuloSum((slack[req]%TDM_Slot)+1,slot_owner,NumberOfSlots)
+ ELSE slot_owner
+ dist == IF (time = TDM_Slot*(slot_count - 1)) /\ (req = slot_owner)
+ THEN 0
+ ELSE NumberOfSlots - so_did + req
+ calc_deadline == TDM_Slot*(dist + slot_count)
+IN LET request_instance == [number |-> request_count + 1,
+ owner |-> req,
+ target |-> BankMapping[req],
+ issue_date |-> time,
+ delayed_issue_date |-> time + slack[req],
+ deadline |-> calc_deadline,
+ type |-> ty,
+ hit_miss |-> hm]
+IN /\ time % arrival_rate = 0
+ /\ time =< time_limit
+ /\ continuation = FALSE
+ /\ continuation' = TRUE
+ /\ request_count' = request_count + 1
+ /\ request_queue' = Append(request_queue,request_instance)
+ /\ UNCHANGED<<time,slot_count,slot_owner,row_buffer,slack,bank_state>>
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* For now, this models the passage of time and the changing between *)
+(* slot owners *)
+(***************************************************************************)
+time_advancing ==
+LET next_time == time + time_increment
+ next_TDM == slot_count * TDM_Slot
+IN /\ time =< time_limit
+ /\ continuation = TRUE
+ /\ time' = next_time
+ /\ slot_count' = IF next_time >= next_TDM THEN slot_count + 1 ELSE slot_count
+ /\ slot_owner' = IF next_time >= next_TDM THEN ModuloSum(slot_owner,1,NumberOfSlots) ELSE slot_owner
+ /\ continuation' = FALSE
+ /\ UNCHANGED<<request_queue,request_count,row_buffer,slack,bank_state>>
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Next Predicate *)
+(***************************************************************************)
+Next ==
+ \/ time_advancing
+ \/ request_arrival(1,"RD","HIT",5)
+ \*\/ request_arrival(2,"RD","MISS",10)
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Fairness and Temporal Formula *)
+(***************************************************************************)
+L == /\ SF_vars(request_arrival(1,"RD","HIT",5))
+ /\ SF_vars(request_arrival(2,"RD","MISS",10))
+
+Spec == Init /\ [][Next]_vars /\ L
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Invariants *)
+(***************************************************************************)
+FullQueue == Len(request_queue) =< Queue_Capacity
+=============================================================================
+\* Modification History
+\* Last modified Sat Feb 20 12:04:03 CET 2021 by felipe
+\* Created Fri Feb 19 10:11:16 CET 2021 by felipe
--
GitLab