A POP ⋆ is Born: Formal Predictable Out-of-Order Processor Model

Modern processors, even at the mid-range level, include multi-level caches, pipelines with branch predictors, or Out-of-Order (OoO) execution. While these are essential for average-case performance, they also increase the complexity of worst-case execution time analysis. OoO execution, for instance, is prone to timing anomalies and, due to the lack of efficient abstractions, quickly leads to state-space explosion. Consequently, it remains highly challenging in the context of critical real-time systems.This work proposes the first generic approach to predictable OoO execution, which is formally modeled and proven in the F* language and experimentally evaluated through simulations in gem5. Performance is evaluated on different processor models for MiBench and Embench programs. The average slowdown for an ARM A710-like processor model amounts to about 18.3% due to an implementation particularity of gem5. Eliminating bias from this issue reduces the slowdown to only 8.8%-10.4%.