The goal is to come up with a model of a dynamic TDM, which implements slack [1]. From this point, we could model the dynamic row buffer policy. Writing a model allows us to perform formal verification of our algorithms. In the context of latency analysis for DRAM controllers, this is an attractive idea, since it’s less prone to errors, besides being less pedantic.
We explored two modeling tools / languages for the time being. The first one is TLA+. By being based on a pure mathematical description of systems, TLA+ is a very powerful tool. Concerning the system, no clear distinctions are made between the scheduler, the DRAM banks and the requestors. Following a private-bank policy, we assume that each requestor accesses a different DRAM bank. Therefore, we only specify the set of banks in the system. The system simulates a situation in which every TDM slot has a request to be served (which is the most stressed scenario), therefore, modelling requesters wasn’t necessary until this point.
The solution is elegant, because it stays very close to what a hardware implementation would look like. It uses a number of functions (representing counters) to track how much time has elapsed between the issue of different commands, and correctness by design is easily achievable (correctness can be additionally checked by the model checker, obviously). By running TLC, the TLA+ model checker, we can easily look for safety errors (checking for invariants), which, if existent, will show up early.
However, for the system we envision, which consists of a clocked digital system, time representation is a major **drawback**. By using the explicit-time approach [2], time is represented as a variable, which can be incremented by one by a “Step” action or by a certain real value d, the former approach being known as discrete time and the latter as continuous time.
Simply put, by using the discrete time approach, **the state space explodes**. What I’ve done in my model is to check for liveness properties until a certain time. While probabilistic speaking we could ensure that everything is fine, the deterministic nature of our problem tells us that this isn’t a good enough solution.
As discussed in [3], other low-level model checkers (as in UPPAAL) try to do better by using continuous time rather than discrete. Using continuous rather than discrete time in our model could improve our performances and allow us to check larger sets of banks, even if the model would result in something further from a potential hardware implementation. The concept of symmetry on time translation [4] could also be of use, but the nature of absolute time values of the described system could make that hard to achieve, or even impossible.
A second drawback lies in the complex relationship between different modules in TLA+. It is not trivial to modularize solutions and use the model checker on different specs simultaneously. This, for instance, is easily done in UPPAAL.
# References
1. Hebbache, Farouk, et al. "Work-conserving dynamic time-division multiplexing for multi-criticality systems." Real-Time Systems 56.2 (2020): 124-170.
2. Lamport, Leslie. "Real time is really simple." Microsoft Research (2005): 2005-30.
4. Lamport, Leslie. "Real-time model checking is really simple." Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Springer, Berlin, Heidelberg, 2005.
# What has to be done
1. Look into continuous time representation in UPPAAL to save computational power.
2. Increment model with arrival times and deadlines of memory requests.
3. Reach a final decision. Can we model our system with TLA + ? If not, try COC for formal proofing, or stick with UPPAAL.
# Questions do be answered
1. What would justify the use of TLA+ ?
⋅⋅⋅ I find it pretty elegant and powerful. But my preference for it does not justify the use if I cannot model the systme I want with it. Also, by explicitely handling a time variable, the model is very close to what it would look like in a hardware implementation.
