Precise Cache Timing Analysis via Symbolic Simulation
Chu Duc Jiep, Joxan Jaffar and Rasool Maghareh
Abstract
We present a framework for WCET analysis of programs with emphasis on
cache micro-architecture. Such an analysis is challenging primarily
because of the timing model of a dynamic nature, that is, the timing
of a basic block is heavily dependent on the context in which it is
executed. At its core, our algorithm is based on symbolic execution,
and an analysis is obtained by locating the longest symbolic
execution path. Clearly a challenge is the intractable number of paths
in the symbolic execution tree. Traditionally this challenge is met by
performing some form of abstraction in the path generation process but
this leads to a loss of path-sensitivity and thus precision in the
analysis. The key feature of our algorithm is the ability for
reuse. This is critical for maintaining a high- level of
path-sensitivity, which in turn produces significantly increased
accuracy. In other words, reuse allows scalability in path-sensitive
exploration. Finally, we present an experimental evaluation on well
known benchmarks in order to show two things: that systematic
path-sensitivity in fact brings significant accuracy gains, and that
the algorithm still scales well.