Path-Sensitive Timing Analysis
Joxan Jaffar, Jorge Navas and Andrew Santosa
Abstract
We address the problem of estimating the Wost-Case Execution Time
(WCET) for loop-bounded programs. It is well known that for
efficiency reasons, current techniques take little or no account of
infeasible paths in the symbolic execution tree, thus limiting their
accuracy. To consider all infeasible paths, ie. to be path-sensitive,
would generally entail an impractical full path enumeration of the
tree. In this paper, we present an algorithm that is
\emph{systematically} path-sensitive. That is, the algorithm detects
all infeasible paths within the unsurmountable limitations of (a)
being able to generate a sufficient loop-invariant, and (b) having the
power of the underlying theorem-prover to decide feasibitily. Thus,
eg. for loop-free programs whose infeasible paths are decidable, our
algorithm is perfectly accurate.
\hspace*{8mm} There are two main features: \emph{interpolation} and
\emph{witness paths}. The algorithm traverses the symbolic execution
tree, in a post-order manner, and discovers an interpolant which
generalizes the execution context of the tree. Trees satisfying the
more general context contain no more paths than the original. While
the interpolant potentially enables the \emph{reuse} of the longest
path estimate obtained from one subtree in order to cover another
subtree, a complimentary problem is that infeasible paths in the
subsumed subtree but feasible in the original subtree are not taken
into account. We deal with this by storing in each traversed subtree
a representative ``witness'' path which defines the longest path
estimate in the subtree. Thus covering of subtrees now depend on both
the interpolant and the witness path of the traversed subtree. In
summary, we provide what is essentially a
\emph{dynamic programming} algorithm which can avoid full enumeration.
We finally present empirical data with real %medium-size
programs to demonstrate practicality.