Skip to content
Snippets Groups Projects
Commit 2132dd22 authored by Felipe Lisboa Malaquias's avatar Felipe Lisboa Malaquias
Browse files

TLA+ updated v6, using countdown timers to advance through time

parent 271d0b5b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
TLAplus/TDMv5/TDMv5.tla
+ 217
− 78
View file @ 2132dd22
------------------------------- MODULE TDMv5 -------------------------------
EXTENDS Reals, Integers
EXTENDS Integers, FiniteSets, Sequences, SequencesExt
Max(a,b) == IF a >= b THEN a ELSE b
\* Utility predicates
Max2Numbers(a,b) == IF a >= b THEN a ELSE b
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
Banks,
\* Intra-bank constraints
t_RCD,
t_RP,
......@@ -21,30 +24,75 @@ CONSTANTS
t_WRtoRD,
t_CCD,
t_WTR,
t_BURST
t_BURST,
\* Other constants
Banks,
CrRq,
NCrRq,
Mapping,
Queue_Capacity
\* This creates a function that maps each requestor to a bank
Requestors == CrRq \cup NCrRq
tMapping == SetToSeq(Mapping)
BankMapping == [req \in Requestors |-> tMapping[req]]
\* Length of the TDM slot. Worst case is a write miss
TDM_Slot == t_RCD + t_WL + t_BURST + t_WR + t_RP + 1
\* Peridiocity of the TDM
TDM_Period == Cardinality(CrRq)
ASSUME
/\ Cardinality(Requestors) = Cardinality(Mapping)
VARIABLES
state,
lbtimer,
now,
req_under_treatment
cmds_lbtimer, \* Lower bound timers, used for expressing timing constraints. There is one per bank per command type.
arvl_lbtimer, \* Upper bound timers, used for modelling arrival of requests. There is one per requestor. Could be any type of timer. SF required.
chsl_lbtimer, \* Lower bound timer, used for modelling the change in slot_owner. Coulbe be any type of timer. SF required.
now, \* Current time
bank_state, \* Used to control the issue of commands to each bank
queue, \* A sequence of records containing the requests that have arrived in the system
req_under_treatment, \* A record representing the request currently under treatment
request_count, \* Counts how many requests per requestor have arrived
slot_count, \* Counts how many TDM slots have elapsed at total
slot_owner, \* The requestor who currently owns the TDM slot
row_buffer, \* A function that maps banks to a row buffer situation, i.e open or closed
slack, \* A function that maps each critical request to a value of slack
control \* A variable that controls the general advance of the system
vars == <<state,lbtimer,now,req_under_treatment>>
vars == <<cmds_lbtimer,arvl_lbtimer,chsl_lbtimer,now,
bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
\* Auxiliary sets
CMDS == {"IDLE","USEBUS","RLSBUS","ACT","RD","WR","PRE"}
\* How to express the type predicate for lbtimer ?
CONTROL == {"INIT","ARRIVAL","TREATMENT","COMPLETED"}
-----------------------------------------------------------------------------
\* What is the rule for changing the slot owner ? Have to make an action for that ?
\* How to express the type predicate for cmds_lbtimer ?
\* Bounding time for now
maxtime == 100
-----------------------------------------------------------------------------
TimeTypeOK ==
\* /\ cmds_lbtimer \in [Banks \X {CMDS \{"IDLE"}} -> Int]
/\ arvl_lbtimer \in [Requestors -> Int]
/\ chsl_lbtimer \in Int
/\ now \in 0..maxtime
\* No type invariance for now : req_under_treatment, queue
TypeOK ==
/\ state \in [Banks -> CMDS]
/\ now \in 0..maxtime
/\ bank_state \in [Banks -> CMDS]
/\ request_count \in [Requestors -> Nat]
/\ slot_count \in Nat
/\ slot_owner \in 1..Cardinality(CrRq)
/\ row_buffer \in [Banks -> {"OPEN","CLOSED"}]
/\ slack \in [CrRq -> Nat]
/\ control \in CONTROL
Init ==
/\ state = [b \in Banks |-> "IDLE"]
/\ lbtimer = [b \in Banks, c \in CMDS |-> 0]
/\ cmds_lbtimer = [b \in Banks, c \in CMDS\{"IDLE"} |-> 0]
/\ arvl_lbtimer = [req \in Requestors |-> 0]
/\ chsl_lbtimer = 0
/\ now = 0
/\ bank_state = [b \in Banks |-> "IDLE"]
/\ req_under_treatment = [type |-> "NONE",
deadline |-> 0,
target |-> "NONE",
......@@ -53,104 +101,195 @@ Init ==
issue_date |-> 0,
delayed_issue_date |-> 0,
hit_miss |-> "NONE"]
\* QUESTION : How could I model the request arrival and treatment with this new model ?
\* Opt 1. By bounds as well.
/\ queue = <<>>
/\ request_count = [r \in Requestors |-> 0]
/\ slot_count = 1
/\ slot_owner = 1
/\ row_buffer = [b \in Banks |-> "CLOSED"]
/\ slack = [req \in CrRq |-> 0]
/\ control = "INIT"
-----------------------------------------------------------------------------
SetTimer(a,b,timer,value) == timer' = [timer EXCEPT ![a,b] = value]
TimedOut(a,b,timer) == timer[a,b] = 0
Set2dimTimer(a,b,timer,value) == timer' = [timer EXCEPT ![a,b] = value]
Set1dimTimer(a,timer,value) == timer' = [timer EXCEPT ![a] = value]
TimedOut_2dim(a,b,timer) == timer[a,b] = 0
TimedOut_1dim(a,timer) == timer[a] = 0
-----------------------------------------------------------------------------
IssueACT(this_bank) ==
/\ state[this_bank] = "ACT"
\* Checks if command is both intra and inter-ready
/\ \A bank \in Banks : TimedOut(bank,"ACT",lbtimer)
\* Sets intra bank timers
/\ SetTimer(this_bank,"RD",lbtimer,t_RCD)
/\ SetTimer(this_bank,"WR",lbtimer,t_RCD)
/\ SetTimer(this_bank,"ACT",lbtimer,t_RC)
/\ SetTimer(this_bank,"PRE",lbtimer,t_RAS)
\* Sets inter bank timers
/\ \A other_bank \in Banks \ {this_bank} : SetTimer(other_bank,"ACT",lbtimer,t_RRD)
\* Decide the next command to be issued
/\ state' = IF req_under_treatment.type = "RD"
THEN [state EXCEPT ![this_bank] = "RD"]
ELSE [state EXCEPT ![this_bank] = "WR"]
/\ UNCHANGED<<now,req_under_treatment>>
/\ bank_state[this_bank] = "ACT"
/\ control = "TREATMENT"
/\ bank_state' = [bank_state EXCEPT ![this_bank] = "RD"]
/\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
IssueRD(this_bank) ==
/\ state[this_bank] = "RD"
/\ bank_state[this_bank] = "RD"
/\ control = "TREATMENT"
\* Checks if command is both intra and inter-ready
/\ \A bank \in Banks : TimedOut(bank,"RD",lbtimer)
/\ \A bank \in Banks : TimedOut_2dim(bank,"RD",cmds_lbtimer)
\* Sets intra bank timers
/\ SetTimer(this_bank,"USEBUS",lbtimer,t_RL)
/\ SetTimer(this_bank,"PRE",lbtimer,t_RTP)
/\ Set2dimTimer(this_bank,"USEBUS",cmds_lbtimer,t_RL)
/\ Set2dimTimer(this_bank,"PRE",cmds_lbtimer,t_RTP)
\* Sets inter and inter bank timers
/\ \A bank \in Banks : /\ SetTimer(bank,"WR",lbtimer,t_RTW)
/\ SetTimer(bank,"RD",lbtimer,t_CCD)
/\ state' = [state EXCEPT ![this_bank] = "USEBUS"]
/\ UNCHANGED<<now,req_under_treatment>>
/\ \A bank \in Banks : /\ Set2dimTimer(bank,"WR",cmds_lbtimer,t_RTW)
/\ Set2dimTimer(bank,"RD",cmds_lbtimer,t_CCD)
/\ bank_state' = [bank_state EXCEPT ![this_bank] = "USEBUS"]
/\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
slot_count,slot_owner,row_buffer,slack,control>>
IssueWR(this_bank) ==
/\ state[this_bank] = "WR"
/\ bank_state[this_bank] = "WR"
/\ control = "TREATMENT"
\* Checks if command is both intra and inter-ready
/\ \A bank \in Banks : TimedOut(bank,"RD",lbtimer)
/\ \A bank \in Banks : TimedOut_2dim(bank,"RD",cmds_lbtimer)
\* Sets intra bank timers
/\ SetTimer(this_bank,"USEBUS",lbtimer,t_WL)
/\ SetTimer(this_bank,"PRE",lbtimer,t_RTP)
/\ Set2dimTimer(this_bank,"USEBUS",cmds_lbtimer,t_WL)
/\ Set2dimTimer(this_bank,"PRE",cmds_lbtimer,t_RTP)
\* Sets inter bank timers
/\ \A other_bank \in Banks \ {this_bank} : SetTimer(other_bank,"RD",lbtimer,t_WRtoRD)
/\ state' = [state EXCEPT ![this_bank] = "USEBUS"]
/\ UNCHANGED<<now,req_under_treatment>>
/\ \A other_bank \in Banks \ {this_bank} : Set2dimTimer(other_bank,"RD",cmds_lbtimer,t_WRtoRD)
/\ bank_state' = [bank_state EXCEPT ![this_bank] = "USEBUS"]
/\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
slot_count,slot_owner,row_buffer,slack,control>>
UseBus(this_bank) ==
/\ state[this_bank] = "USEBUS"
/\ \A bank \in Banks : TimedOut(bank,"USEBUS",lbtimer)
/\ \A bank \in Banks : SetTimer(bank,"RLSBUS",lbtimer,t_BURST)
/\ state' = [state EXCEPT ![this_bank] = "RLSBUS"]
/\ UNCHANGED<<now,req_under_treatment>>
/\ bank_state[this_bank] = "USEBUS"
/\ control = "TREATMENT"
/\ \A bank \in Banks : TimedOut_2dim(bank,"USEBUS",cmds_lbtimer)
/\ \A bank \in Banks : Set2dimTimer(bank,"RLSBUS",cmds_lbtimer,t_BURST)
/\ bank_state' = [bank_state EXCEPT ![this_bank] = "RLSBUS"]
/\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
slot_count,slot_owner,row_buffer,slack,control>>
ReleaseBus(this_bank) ==
/\ state[this_bank] = "RLSBUS"
/\ \A bank \in Banks : TimedOut(bank,"RLSBUS",lbtimer)
/\ bank_state[this_bank] = "RLSBUS"
/\ control = "TREATMENT"
/\ \A bank \in Banks : TimedOut_2dim(bank,"RLSBUS",cmds_lbtimer)
/\ IF req_under_treatment.type = "WR"
THEN SetTimer(this_bank,"PRE",lbtimer,t_WR)
THEN Set2dimTimer(this_bank,"PRE",cmds_lbtimer,t_WR)
ELSE TRUE
/\ \A bank \in Banks : IF req_under_treatment.type = "WR"
THEN SetTimer(bank,"RD",lbtimer,t_WTR)
THEN Set2dimTimer(bank,"RD",cmds_lbtimer,t_WTR)
ELSE TRUE
/\ state' = [state EXCEPT ![this_bank] = "PRE"]
/\ UNCHANGED<<now,req_under_treatment>>
/\ bank_state' = [bank_state EXCEPT ![this_bank] = "PRE"]
/\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
slot_count,slot_owner,row_buffer,slack,control>>
IssuePRE(this_bank) ==
/\ state[this_bank] = "PRE"
/\ \A bank \in Banks : TimedOut(bank,"PRE",lbtimer)
/\ bank_state[this_bank] = "PRE"
/\ control = "TREATMENT"
/\ \A bank \in Banks : TimedOut_2dim(bank,"PRE",cmds_lbtimer)
\* Intra-bank : PRE to ACT
/\ SetTimer(this_bank,"ACT",lbtimer,t_RP)
/\ Set2dimTimer(this_bank,"ACT",cmds_lbtimer,t_RP)
\* Complection : bank becomes idle again
/\ state' = [state EXCEPT ![this_bank] = "IDLE"]
/\ UNCHANGED<<now,req_under_treatment>>
/\ bank_state' = [bank_state EXCEPT ![this_bank] = "IDLE"]
/\ UNCHANGED<<arvl_lbtimer,chsl_lbtimer,now,queue,req_under_treatment,request_count,
slot_count,slot_owner,row_buffer,slack,control>>
-----------------------------------------------------------------------------
treat_request ==
LET deadlines == {queue[n].deadline : n \in 1..Len(queue)}
min_deadline == Min(deadlines)
selected_req == SelectSeq(queue, LAMBDA elem: elem.deadline = min_deadline)[1]
StartTreatment == /\ queue' = Remove(queue,selected_req)
/\ req_under_treatment' = selected_req
/\ bank_state' = [bank_state EXCEPT ![selected_req.target] = "ACT"]
ResumeTreatment == UNCHANGED<<queue,req_under_treatment,bank_state>>
IN /\ (control = "ARRIVAL") \/ (control = "COMPLETE" /\ queue /= <<>>)
/\ control' = "TREATMENT"
/\ IF req_under_treatment.owner = 0
THEN StartTreatment
ELSE ResumeTreatment
/\ UNCHANGED<<arvl_lbtimer,cmds_lbtimer,chsl_lbtimer,now,request_count,slot_count,slot_owner,
row_buffer,slack>>
-----------------------------------------------------------------------------
\* so_did : slot owner considering the delayed issue date
\* dist : distance to the next slot owned by the requestor
request_arrival(req,ty,hm,arrival_rate) ==
LET so_did == IF slack[req] >= (slot_count*TDM_Slot - now)
THEN ModuloSum((slack[req]%TDM_Slot)+1,slot_owner,TDM_Period)
ELSE slot_owner
dist == IF (now = TDM_Slot*(slot_count - 1)) /\ (req = slot_owner)
THEN 0
ELSE IF req = so_did
THEN TDM_Period
ELSE IF req - so_did >= 0
THEN req - so_did
ELSE so_did - req
calc_deadline == IF req \in CrRq
THEN TDM_Slot*(slot_count + dist)
ELSE TDM_Slot*(slot_count + 1)
request_instance == [number |-> request_count[req] + 1,
owner |-> req,
target |-> BankMapping[req],
issue_date |-> now,
delayed_issue_date |-> now + slack[req],
deadline |-> calc_deadline,
type |-> ty,
hit_miss |-> hm,
period |-> arrival_rate]
IN \* Only one request per requestor in the queue
/\ req \notin {queue[n].owner : n \in 1..Len(queue)}
\* No consecutive arrivals
/\ control \in CONTROL \{"ARRIVAL"}
\* Sets up the timer for the next TDM slot
/\ IF control = "INIT" THEN chsl_lbtimer' = TDM_Slot ELSE UNCHANGED<<chsl_lbtimer>>
\* The next arrival should happen at max arrival_rate cycles after this
/\ TimedOut_1dim(req,arvl_lbtimer)
/\ Set1dimTimer(req,arvl_lbtimer,arrival_rate)
/\ control' = "ARRIVAL"
/\ request_count' = [request_count EXCEPT ![req] = request_count[req] + 1]
/\ queue' = Append(queue,request_instance)
/\ UNCHANGED<<cmds_lbtimer,now,bank_state,req_under_treatment,
slot_count,slot_owner,row_buffer,slack>>
-----------------------------------------------------------------------------
SlotChange ==
/\ control /= "INIT"
\* Checks if the timer has timed_out
/\ chsl_lbtimer = 0
\* Sets it aggain
/\ chsl_lbtimer' = TDM_Slot
/\ slot_count' = slot_count + 1
/\ slot_owner' = ModuloSum(slot_owner,1,TDM_Period)
/\ UNCHANGED<<cmds_lbtimer,arvl_lbtimer,now,bank_state,queue,req_under_treatment,request_count,row_buffer,slack,control>>
-----------------------------------------------------------------------------
Tick ==
\E d \in {r \in Real: r > 0}:
/\ now' = now + d
/\ lbtimer' = [b \in Banks, c \in CMDS |-> Max(0,lbtimer[b,c]-d)]
/\ UNCHANGED<<state,req_under_treatment>>
TNext(bank) == \/ IssueACT(bank)
\/ IssueRD(bank)
\/ IssueWR(bank)
\/ UseBus(bank)
\/ ReleaseBus(bank)
\/ IssuePRE(bank)
Next == Tick \/ (\E bank \in Banks : TNext(bank))
Tick == LET d == 1 IN
/\ ~\E bank \in Banks : TNext(bank)
/\ \neg ENABLED (treat_request \/ request_arrival(1,"RD","HIT",10) \/ request_arrival(2,"WR","MISS",15) \/ SlotChange)
/\ now' = now + d
/\ arvl_lbtimer' = [req \in Requestors |-> Max2Numbers(0,arvl_lbtimer[req]-d)]
/\ cmds_lbtimer' = [b \in Banks, c \in CMDS \{"IDLE"} |-> Max2Numbers(0,cmds_lbtimer[b,c]-d)]
/\ chsl_lbtimer' = Max2Numbers(0,chsl_lbtimer-d)
/\ UNCHANGED<<bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
-----------------------------------------------------------------------------
Next == \/ Tick
\/ \E bank \in Banks : TNext(bank)
\/ treat_request
\/ SlotChange
\/ request_arrival(1,"RD","HIT",10)
\/ request_arrival(2,"WR","MISS",15)
-----------------------------------------------------------------------------
SafetySpec == Init /\ [][Next]_vars
FullQueue == Len(queue) =< Queue_Capacity
THEOREM SafetySpec => FullQueue
-----------------------------------------------------------------------------
Liveness == /\ \A bank \in Banks : WF_vars(TNext(bank))
/\ \A r \in Real : <>(now > r)
Spec == SafetySpec /\ Liveness
Fairness == /\ \A b \in Banks :
/\ SF_vars(IssueACT(b))
/\ SF_vars(IssueRD(b))
/\ SF_vars(IssueWR(b))
/\ SF_vars(IssuePRE(b))
/\ SF_vars(UseBus(b))
/\ SF_vars(ReleaseBus(b))
/\ WF_vars(SlotChange)
/\ WF_vars(treat_request)
/\ WF_vars(request_arrival(1,"RD","HIT",10))
/\ WF_vars(request_arrival(2,"WR","MISS",15))
Spec == SafetySpec /\ Fairness
=============================================================================
\* Modification History
\* Last modified Wed Mar 03 23:08:30 CET 2021 by felipe
\* Last modified Fri Mar 05 10:32:19 CET 2021 by felipe
\* Created Wed Mar 03 20:37:54 CET 2021 by felipe
TLAplus/TDMv6/TDMv6.tla 0 → 100644
+ 225
− 0
View file @ 2132dd22
------------------------------- MODULE TDMv6 -------------------------------
EXTENDS Integers, FiniteSets, Sequences, SequencesExt
-----------------------------------------------------------------------------
Max2Numbers(a,b) == IF a >= b THEN a ELSE b
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)
-----------------------------------------------------------------------------
Infinity == 1000
Real == 0..100 \cup Infinity
-----------------------------------------------------------------------------
CONSTANTS
\* Intra-bank constraints
t_RCD,
t_RP,
t_RC,
t_RAS,
t_RL,
t_WL,
t_RTP,
t_WR,
\* Inter-bank constraints
t_RRD,
\* Inter- and intra-bank constraints
t_RTW,
t_WRtoRD,
t_CCD,
t_WTR,
t_BURST,
\* Other constants
Banks,
CrRq,
NCrRq,
Mapping,
Queue_Capacity
\* This creates a function that maps each requestor to a bank
Requestors == CrRq \cup NCrRq
tMapping == SetToSeq(Mapping)
BankMapping == [req \in Requestors |-> tMapping[req]]
\* Length of the TDM slot. Worst case is a write miss
TDM_Slot == t_RCD + t_WL + t_BURST + t_WR + t_RP + 1
\* Peridiocity of the TDM
TDM_Period == Cardinality(CrRq)
ASSUME
/\ Cardinality(Requestors) = Cardinality(Mapping)
VARIABLES
now,
ACT_lbtimer,
RD_lbtimer,
WR_lbtimer,
PRE_lbtimer,
USEBUS_lbtimer,
RLSBUS_lbtimer,
ARV_lbtimer,
SLOT_lbtimer,
bank_state,
queue,
req_under_treatment,
request_count,
slot_count,
slot_owner,
row_buffer,
slack,
control
vars == <<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,ARV_lbtimer,SLOT_lbtimer,
bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
-----------------------------------------------------------------------------
CMDS == {"ACT","RD","WR","PRE","IDLE","USEBUS","RLSBUS"}
CONTROL == {"INIT","ARRIVAL","TREATMENT","COMPLETED"}
-----------------------------------------------------------------------------
TimeTypeOK ==
/\ now \in Real
/\ ACT_lbtimer \in [Banks -> Real]
/\ RD_lbtimer \in [Banks -> Real]
/\ WR_lbtimer \in [Banks -> Real]
/\ PRE_lbtimer \in [Banks -> Real]
/\ USEBUS_lbtimer \in [Banks -> Real]
/\ RLSBUS_lbtimer \in [Banks -> Real]
/\ ARV_lbtimer \in [Requestors -> Real]
/\ SLOT_lbtimer \in Real
\* No type invariance for now : req_under_treatment, queue
TypeOK ==
/\ bank_state \in [Banks -> CMDS]
/\ request_count \in [Requestors -> Nat]
/\ slot_count \in Nat
/\ slot_owner \in 1..Cardinality(CrRq)
/\ row_buffer \in [Banks -> {"OPEN","CLOSED"}]
/\ slack \in [CrRq -> Nat]
/\ control \in CONTROL
Init ==
/\ now = 0
/\ ACT_lbtimer = [b \in Banks |-> 0]
/\ RD_lbtimer = [b \in Banks |-> 0]
/\ WR_lbtimer = [b \in Banks |-> 0]
/\ PRE_lbtimer = [b \in Banks |-> 0]
/\ USEBUS_lbtimer = [b \in Banks |-> 0]
/\ RLSBUS_lbtimer = [b \in Banks |-> 0]
/\ ARV_lbtimer = [req \in Requestors |-> 0]
/\ SLOT_lbtimer = 0
/\ bank_state = [b \in Banks |-> "IDLE"]
/\ queue = <<>>
/\ req_under_treatment = [type |-> "NONE",deadline |-> 0,target |-> "NONE",number |-> 0,owner |-> 0,
issue_date |-> 0,delayed_issue_date |-> 0,hit_miss |-> "NONE"]
/\ request_count = [r \in Requestors |-> 0]
/\ slot_count = 1
/\ slot_owner = 1
/\ row_buffer = [b \in Banks |-> "CLOSED"]
/\ slack = [req \in CrRq |-> 0]
/\ control = "INIT"
-----------------------------------------------------------------------------
TimedOut(timer,index) == timer[index] = 0
SetLBTimer(timer,index,value) == timer' = [timer EXCEPT ![index] = value]
-----------------------------------------------------------------------------
IssueACT(bank) ==
/\ control = "TREATMENT"
/\ bank_state[bank] = "ACT"
/\ ACT_lbtimer["N1"] = 0
/\ ACT_lbtimer["N2"] = 0
/\ control' = "INIT"
/\ UNCHANGED<<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,ARV_lbtimer,SLOT_lbtimer,
bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack>>
-----------------------------------------------------------------------------
treat_request ==
LET deadlines == {queue[n].deadline : n \in 1..Len(queue)}
min_deadline == Min(deadlines)
selected_req == SelectSeq(queue, LAMBDA elem: elem.deadline = min_deadline)[1]
IN /\ (control = "ARRIVAL") \/ (control = "COMPLETE" /\ queue /= <<>>)
/\ control' = "TREATMENT"
/\ queue' = IF req_under_treatment.owner = 0 THEN Remove(queue,selected_req) ELSE queue
/\ req_under_treatment' = IF req_under_treatment.owner = 0 THEN selected_req ELSE req_under_treatment
/\ bank_state' = IF req_under_treatment.owner = 0 THEN [bank_state EXCEPT ![selected_req.target] = "ACT"] ELSE bank_state
/\ UNCHANGED<<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,ARV_lbtimer,SLOT_lbtimer,
request_count,slot_count,slot_owner,row_buffer,slack>>
-----------------------------------------------------------------------------
request_arrival(req,ty,hm,arrival_rate) ==
LET so_did == IF slack[req] >= (slot_count*TDM_Slot - now)
THEN ModuloSum((slack[req]%TDM_Slot)+1,slot_owner,TDM_Period)
ELSE slot_owner
dist == IF (now = TDM_Slot*(slot_count - 1)) /\ (req = slot_owner)
THEN 0
ELSE IF req = so_did
THEN TDM_Period
ELSE IF req - so_did >= 0
THEN req - so_did
ELSE so_did - req
calc_deadline == IF req \in CrRq
THEN TDM_Slot*(slot_count + dist)
ELSE TDM_Slot*(slot_count + 1)
request_instance == [number |-> request_count[req] + 1,
owner |-> req,
target |-> BankMapping[req],
issue_date |-> now,
delayed_issue_date |-> now + slack[req],
deadline |-> calc_deadline,
type |-> ty,
hit_miss |-> hm,
period |-> arrival_rate]
IN /\ req \notin {queue[n].owner : n \in 1..Len(queue)}
/\ control \in CONTROL \{"ARRIVAL"}
/\ TimedOut(ARV_lbtimer,req)
\* Primed
/\ SLOT_lbtimer' = IF control = "INIT" THEN TDM_Slot ELSE SLOT_lbtimer
/\ SetLBTimer(ARV_lbtimer,req,arrival_rate)
/\ control' = "ARRIVAL"
/\ request_count' = [request_count EXCEPT ![req] = request_count[req] + 1]
/\ queue' = Append(queue,request_instance)
/\ UNCHANGED<<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,
bank_state,req_under_treatment,slot_count,slot_owner,row_buffer,slack>>
-----------------------------------------------------------------------------
SlotChange ==
/\ control /= "INIT"
/\ SLOT_lbtimer = 0
/\ SLOT_lbtimer' = TDM_Slot
/\ slot_count' = slot_count + 1
/\ slot_owner' = ModuloSum(slot_owner,1,TDM_Period)
/\ UNCHANGED<<now,ACT_lbtimer,RD_lbtimer,WR_lbtimer,PRE_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,ARV_lbtimer,
bank_state,queue,req_under_treatment,request_count,row_buffer,slack,control>>
-----------------------------------------------------------------------------
\*TNext(bank) == IssueACT(bank)
-----------------------------------------------------------------------------
\*Tick == \E d \in 0..100:
\* \* The Tick action is only allowed to happen when other decision actions are not possible
\* /\ ~\E bank \in Banks : IssueACT(bank)
\* /\ \neg ENABLED (treat_request \/ request_arrival(1,"RD","HIT",10) \/ request_arrival(2,"WR","MISS",15) \/ SlotChange)
\* /\ now' = now + d
\* /\ ACT_lbtimer' = [b \in Banks |-> Max2Numbers(0,ACT_lbtimer[b]-d)]
\* /\ RD_lbtimer' = [b \in Banks |-> Max2Numbers(0,RD_lbtimer[b]-d)]
\* /\ WR_lbtimer' = [b \in Banks |-> Max2Numbers(0,WR_lbtimer[b]-d)]
\* /\ PRE_lbtimer' = [b \in Banks |-> Max2Numbers(0,PRE_lbtimer[b]-d)]
\* /\ USEBUS_lbtimer' = [b \in Banks |-> Max2Numbers(0,USEBUS_lbtimer[b]-d)]
\* /\ RLSBUS_lbtimer' = [b \in Banks |-> Max2Numbers(0,RLSBUS_lbtimer[b]-d)]
\* /\ ARV_lbtimer' = [b \in Banks |-> Max2Numbers(0,ARV_lbtimer[b]-d)]
\* /\ SLOT_lbtimer' = Max2Numbers(0,SLOT_lbtimer-d)
\* /\ UNCHANGED<<bank_state,queue,req_under_treatment,request_count,slot_count,slot_owner,row_buffer,slack,control>>
-----------------------------------------------------------------------------
Next == \/ request_arrival(1,"RD","HIT",10)
\/ request_arrival(2,"WR","MISS",15)
\*\/ Tick
\/ treat_request
\/ SlotChange
\/ \E bank \in Banks : IssueACT(bank)
-----------------------------------------------------------------------------
SafetySpec == Init /\ [][Next]_vars
FullQueue == Len(queue) =< Queue_Capacity
THEOREM SafetySpec => FullQueue
-----------------------------------------------------------------------------
Fairness == /\ SF_vars(SlotChange)
/\ SF_vars(treat_request)
/\ SF_vars(request_arrival(1,"RD","HIT",10))
/\ SF_vars(request_arrival(2,"WR","MISS",15))
/\ \A b \in Banks : SF_vars(IssueACT(b))
Spec == SafetySpec /\ Fairness
=============================================================================
\* Modification History
\* Last modified Fri Mar 05 14:21:57 CET 2021 by felipe
\* Created Wed Mar 03 20:37:54 CET 2021 by felipe
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment