[TLA+,WIP] - Complete model

TLAplus/TDMv3/TDMv3.tla

+------------------------------- 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