Enabling timing predictability in the presence of store buffers

Alban Gruin (1, 2) , Thomas Carle (1) , Christine Rochange (1) , Pascal Sainrat (1)

1 IRIT-TRACES - Groupe de Recherche en Architecture et Compilation pour les systèmes embarqués
2 UT3 - Université Toulouse III - Paul Sabatier

We study the effect of store buffers on the timing predictability of processor pipelines. We show that the concurrency between the load unit and the store buffer to access the memory bus is an obstacle to timing predictability, even in simple scalar in-order pipeline designs. We then propose a gating mechanism that removes these shortcomings. We model subsets of pipelines that implement our mechanism using an established logic framework. Using the Coq proof assistant, we prove that it enables timing predictability. Finally, we show that the performance cost of our mechanism measured on an FPGA-synthesized RISC-V core is around 2% only on average, with a minimal increase in resource usage.

Keywords: Computer architecture; Timing predictability; Timing anomalies; Coq

Domains: Hardware Architecture [cs.AR]

Alban Gruin, Thomas Carle, Christine Rochange, Pascal Sainrat. Enabling timing predictability in the presence of store buffers. 31st International Conference on Real-Time Networks and Systems (RTNS 2023), Jun 2023, Dortmund, Germany. pp.1-10, ⟨10.1145/3575757.3593653⟩. ⟨hal-04082519⟩