Modelling and proving the monotonicity of processor pipelines in Coq

From bibtex.

Abstract

In critical real-time systems, the worst-case execution time (WCET) of software tasks must be statically bounded in order to guarantee that they all satisfy their timing constraints (e.g. deadlines). Obtaining such bounds is challenging due to the complexity of the software and of the acceleration mechanisms implemented in the hardware. Particular behaviors, known as timing anomalies, break some simplifying assumptions for the computation of WCET in single and multi-core processors. Some cores have been designed to implement a pipeline-level property known as monotonicity that guarantees that no timing anomaly can occur in the pipeline. Proving the monotonicity of a pipeline is tedious and error-prone, and so is reading the proof and convincing oneself of its validity. We thus propose to rely on the Coq proof assistant to guarantee the soundness of the proofs. In this paper, we show how the monotonicity property and the standard elements composing a pipeline can be modelled in Coq. Using an example based on an open-hardware RISC-V core from the literature, we introduce the main elements of the proof and discuss their reusability for other cores. We conclude that the model and proofs that we provide can be easily adapted to describe other in-order pipelines of equivalent complexity.