Parallelism analysis: Precise WCET values for complex multi-core systems

In the verification of safety-critical real-time systems, the problem of determining the worst-case execution time (WCET) of a task is of utmost importance. Safe formal methods have been established for solving the single-task, single-core WCET problem. The de-facto standard approach uses abstract interpretation to derive basic block execution times and a combinatorial path analysis which derives the longest path through the program. WCET analyses for multi-core computers have extended this methodology by assuming that shared resources are partitioned in either time or space and that therefore each core can still be analyzed separately. For real-world multi-cores this assumption is often not true, making the classic WCET analysis approach either inapplicable or very imprecise. To overcome this, we present a technique to explore the interleavings of a parallel task system as well as an exclusion criterion to prove that certain interleavings can never occur. We show how this technique can be integrated into existing WCET analysis approaches and finally show that the average WCET of a collection of real-time benchmarks could be reduced by a factor of up to 11.96 using this new analysis type.