ProTiPP is a research project funded by the French Research Agency
(Grant number ANR-22-CE25-0004)
Today embedded and cyber-physical systems employ computationally intensive algorithms and must be deployed on multicore platforms. Besides, many of these systems are expected to meet deadlines and thus require timing verification.
The challenge of timing verification of multicore systems is to safely account for interference over shared resources. For tractability reasons, state-of-the-art approaches assume timing compositionality, which allows decoupling the analysis of worst-case execution times (WCET) on each core from the analysis of the latencies to external shared resources (including the impact of task interference). But timing compositionality requires processing cores to be free from timing anomalies which is hardly ever checked and is likely to be wrong for most of off-the-shelves processors. Unfortunately, the community is lacking tools that would help to verify this property formally. The ProTiPP project will fill these gaps by:
- reconciling timing predictability and performance in processing cores. Academic processors designed with timing predictability in mind do not fulfill performance requirements because they usually disable advanced mechanisms that are complex to analyze (e.g. out-of-order execution). We will explore ways to make these mechanisms predictable.
- providing a formal framework to prove timing predictability. We will design formal models of processors microarchitectures, allowing the expression and the formal verification of time-related properties. Several frameworks will be explored (proof assistants, refinement-based formal development platforms) in order to cope with the increasing complexity of processors.
We will demonstrate our approach by designing a proved timing-predictable
RISC-V processor. We will produce an FPGA prototype as well as a WCET analysis tool to evaluate the average and worst-case performance. Our contributions will be released as open-source hardware and software.
Participants:
Jean-Paul Bodeveix, Thomas Carle, Hugues Cassé, Mamoun Filali,
Alban Gruin, Christine Rochange, Pascal Sainrat