WCET Analysis meets Virtual Prototyping: Improving Source-Level Timing Annotations

In this paper we discuss the problem of relating machine instructions to source level constructs, and how it has been addressed in the domains of Virtual Prototyping (VP) and Worst-Case Execution Time (WCET) analysis. It has been handled in different ways, although the goals and requirements between both domains are not far from another. This paper shows that there exists a mutual benefit in exchanging solutions between the two research domains, by demonstrating the applicability and utility of VP methods for WCET analysis, and highlighting their shortcomings. After an evaluation of existing methods, we carefully rework and combine them to a sound and generic mapping algorithm for source-level WCET analysis. As a result, we obtain WCET estimates that outperform classic binary analyzers especially under moderate compiler optimization. Our approach is based on hierarchical flow matching, control-dependency- and dominator-homomorphic maps, and dominator lumping to soundly fill the gaps in the mapping. WCET estimation is performed using Model Checking, which maximally exploits the information available in the source, and highlights remaining weaknesses in the mapping methods. Last but not least, we discuss further chances of synergy between both research communities which could enable support for more complex microarchitectures with caches, pipelines and speculative execution in both source-level WCET analysis and VP.