G (2010) Combining Abstract Interpretation with Model Checking for Timing Analysis of Multicore Software

Abstract—It is predicted that multicores will be increasingly used in future embedded real-time systems for high perfor-mance and low energy consumption. The major obstacle is that we may not predict and provide any guarantee on real-time properties of software on such platforms. The shared memory bus is among the most critical resources, which severely degrade the timing predictability of multicore software due to the access contention between cores. In this paper, we study a multicore architecture where each core has a local L1 cache and all cores use a shared bus to access the off-chip memory. We use Abstract Interpretation (AI) to analyze the local cache behavior of a program running on a dedicated core. Based on the cache analysis, we construct a Timed Automaton (TA) to model the precise timing information of the program on when to access the memory bus (i.e. when a cache miss occurs). Then we model the shared bus also using timed automata. The TA models for the bus and programs running on separated cores will be explored using the UPPAAL model checker to find the WECTs for the respective programs. Based on the presented techniques, we have developed a tool for multicore timing analysis, which allows automatic generation of the TA models from binary code and WCET estimation for any given TA model of the shared bus. Extensive experiments have been conducted, showing that the combined approach can significantly tighten the estimations. As examples, we have studied the TDMA and FCFS buses. In both cases, the WCET bounds can be tightened by up to 240 % and 82 % respectively, compared with the worst-case bounds estimated based on cache misses and maximal delays for bus access. Keywords-abstract interpretation, model checking, WCET, multicore, shared bus I