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

Amelioration on time continuous model, many concepts are now implemented

parent 82956f11
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 56 additions and 20 deletions
TLAplus/TDMv3/TDMv3.tla
+ 56
− 20
View file @ 9f3ee2b3
......@@ -44,10 +44,11 @@ VARIABLES
slot_owner,
row_buffer,
slack,
bank_state
bank_state,
timer
vars == <<time,control,req_under_treatment,queue,request_count,
slot_count,slot_owner,row_buffer,slack,bank_state>>
slot_count,slot_owner,row_buffer,slack,bank_state,timer>>
CMDS == {"NOP","ACT","RD","BUS","WR","PRE","REF"}
Control == {"IDLE","ARRIVAL","TREATMENT","COMPLETED"}
......@@ -60,7 +61,7 @@ max_requests == 100
\* For now there are no type constraints on : queue, req_under_treatment
TypeOK ==
/\ time \in 0..max_time
/\ time \in 0..500
/\ control \in Control
/\ request_count \in [Requestors -> 0..max_requests]
/\ slot_count \in 1..10
......@@ -68,7 +69,15 @@ TypeOK ==
/\ row_buffer \in [AllBanks -> {"OPEN","CLOSED"}]
/\ slack \in [CrRq -> Nat]
/\ bank_state \in [AllBanks -> CMDS]
(***************************************************************************)
(* O problema de usar o modelo com contatdores e clocks (ideal e seguro) é *)
(* a complexidade de checagem do modelo. Pode-se argumentar então que o *)
(* modelo aqui representado não corresponde exatamente ao controlador. O *)
(* controlador implementado em hardware seria correto por design (timing *)
(* constraints usadas como contadores) ou baseado em um modelo tal que *)
(* esse? O controlador desta especificação não representa o mesmo da outra *)
(***************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* Init state predicate *)
......@@ -91,6 +100,7 @@ Init ==
/\ row_buffer = [b \in AllBanks |-> "CLOSED"]
/\ slack = [req \in CrRq |-> 0]
/\ bank_state = [b \in AllBanks |-> "NOP"]
/\ timer = 0
-----------------------------------------------------------------------------
(***************************************************************************)
(* Actions that representing the issuing of DRAM commands, they are the *)
......@@ -104,7 +114,7 @@ IssueACT(bank) ==
THEN [bank_state EXCEPT ![bank] = "RD"]
ELSE [bank_state EXCEPT ![bank] = "WR"]
/\ UNCHANGED<<control,req_under_treatment,queue,request_count,
slot_count,slot_owner,row_buffer,slack>>
slot_count,slot_owner,row_buffer,slack,timer>>
IssueRD(bank) ==
LET t_RCD == 6
......@@ -113,7 +123,7 @@ IN /\ control = "TREATMENT"
/\ time' = time + t_RCD
/\ bank_state' = [bank_state EXCEPT ![bank] = "BUS"]
/\ UNCHANGED<<control,req_under_treatment,queue,request_count,
slot_count,slot_owner,row_buffer,slack>>
slot_count,slot_owner,row_buffer,slack,timer>>
IssueWR(bank) ==
LET t_RCD == 6
......@@ -122,7 +132,7 @@ IN /\ control = "TREATMENT"
/\ time' = time + t_RCD
/\ bank_state' = [bank_state EXCEPT ![bank] = "BUS"]
/\ UNCHANGED<<control,req_under_treatment,queue,request_count,
slot_count,slot_owner,row_buffer,slack>>
slot_count,slot_owner,row_buffer,slack,timer>>
\* For RD requests, the PRE command can be issued instanteneously, as for WR requests
\* there is a WR to PRE timing constraint
......@@ -140,9 +150,9 @@ IN /\ control = "TREATMENT"
THEN time + t_RTP - (t_RL + t_BURST)
ELSE time
/\ bank_state' = [bank_state EXCEPT ![bank] = "NOP"]
/\ req_under_treatment' = [req_under_treatment EXCEPT !.owner = "NONE"]
/\ req_under_treatment' = [req_under_treatment EXCEPT !.owner = 0]
/\ UNCHANGED<<queue,request_count,
slot_count,slot_owner,row_buffer,slack>>
slot_count,slot_owner,row_buffer,slack,timer>>
UsingBus(bank) ==
LET t_RL == 6
......@@ -155,8 +165,9 @@ IN /\ control = "TREATMENT"
ELSE time + t_WL + t_BURST
/\ bank_state' = [bank_state EXCEPT ![bank] = "PRE"]
/\ UNCHANGED<<control,req_under_treatment,queue,request_count,
slot_count,slot_owner,row_buffer,slack>>
slot_count,slot_owner,row_buffer,slack,timer>>
-----------------------------------------------------------------------------
\* Have to create a completed action, which will say
(***************************************************************************)
(* 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 *)
......@@ -176,10 +187,10 @@ LET deadlines == {queue[n].deadline : n \in 1..Len(queue)}
ResumeTreatment == UNCHANGED<<queue,req_under_treatment,bank_state>>
IN /\ (control = "ARRIVAL") \/ (control = "COMPLETE" \/ queue /= <<>>)
/\ control' = "TREATMENT"
/\ IF req_under_treatment.type = "NONE"
/\ IF req_under_treatment.owner = 0
THEN StartTreatment
ELSE ResumeTreatment
/\ UNCHANGED<<time,request_count,slot_count,slot_owner,row_buffer,slack>>
/\ UNCHANGED<<time,request_count,slot_count,slot_owner,row_buffer,slack,timer>>
-----------------------------------------------------------------------------
(***************************************************************************)
(* Actions that model the arrival of new tasks into the system. They are *)
......@@ -207,32 +218,46 @@ LET so_did == IF slack[req] >= (slot_count*TDM_Slot - time)
deadline |-> calc_deadline,
type |-> ty,
hit_miss |-> hm]
IN /\ time - request_count[req]*arrival_rate >= 0
\*/\ control \in {"IDLE","COMPLETED"}
\* Requist arrival
\* 1. Only one request per requestor in the queue
\* 2. No consecutive arrivals
\* 3. There are at least arrival_rate cycles between two requests of the same requestor
IN /\ req \notin {queue[n].owner : n \in 1..Len(queue)}
/\ control /= "ARRIVAL"
/\ time - request_count[req]*arrival_rate >= 0
/\ control' = "ARRIVAL"
/\ request_count' = [request_count EXCEPT ![req] = request_count[req] + 1]
/\ queue' = Append(queue,request_instance)
/\ UNCHANGED<<time,req_under_treatment,slot_count,slot_owner,row_buffer,slack,bank_state>>
/\ UNCHANGED<<time,req_under_treatment,slot_count,slot_owner,row_buffer,slack,bank_state,timer>>
-----------------------------------------------------------------------------
\* From RealTimeNew Module
IntervalLB(t,Acts,B,v,min,lb) ==
LET TNext == t' = IF <<B>>_v \/ \neg(ENABLED <<Acts \/ B>>_v)'
THEN 0
ELSE t + (time' - time)
LowerBound == B => IF lb THEN t >= min ELSE t > min
IN /\ TNext
/\ LowerBound
-----------------------------------------------------------------------------
(***************************************************************************)
(* Next Predicate *)
(***************************************************************************)
Next ==
\/ request_arrival(1,"RD","HIT",5)
\/ request_arrival(2,"WR","MISS",10)
\/ request_arrival(1,"RD","HIT",10)
\/ request_arrival(2,"WR","HIT",20)
\/ treat_request
\/ \E b \in AllBanks : \/ IssueACT(b)
\/ IssueRD(b)
\/ IssueWR(b)
\/ IssuePRE(b)
\/ UsingBus(b)
/\ LET t_RCD == 6 IN \A b \in AllBanks: IntervalLB(timer,TRUE,IssueRD(b),vars,t_RCD,TRUE)
-----------------------------------------------------------------------------
(***************************************************************************)
(* Fairness and Temporal Formula *)
(***************************************************************************)
L == /\ WF_vars(request_arrival(1,"RD","HIT",5))
/\ WF_vars(request_arrival(2,"WR","MISS",10))
L == /\ WF_vars(request_arrival(1,"RD","HIT",10))
/\ WF_vars(request_arrival(2,"WR","HIT",12))
/\ WF_vars(treat_request)
/\ \A b \in AllBanks : /\ SF_vars(IssueACT(b))
/\ SF_vars(IssueRD(b))
......@@ -245,8 +270,19 @@ Spec == Init /\ [][Next]_vars /\ L
(***************************************************************************)
(* Invariants *)
(***************************************************************************)
\* The queue never becomes full
FullQueue == Len(queue) =< Queue_Capacity
\* The queue never has two requests of the same requestor
OneRequestInTheQueue ==
LET Owners == {queue[n].owner : n \in 1..Len(queue)}
IN \A requestor \in Requestors : Cardinality({owner \in Owners : owner = requestor}) =< 1
(***************************************************************************)
(* Temporal Properties *)
(***************************************************************************)
\* Requests are eventually served
MaxTime == <>(time = max_time)
=============================================================================
\* Modification History
\* Last modified Tue Feb 23 13:59:40 CET 2021 by felipe
\* Last modified Fri Feb 26 18:53:51 CET 2021 by felipe
\* Created Fri Feb 19 10:11:16 CET 2021 by felipe
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