Revisiting Underapproximate Reachability for Multipushdown Systems
389
several technical challenges which are specific to the timed setting. Implementing
this approach in BHIM makes it, to the best of our knowledge, the first tool that
can analyze timed multi-stack pushdown automata with closed guards.
We analyze the performance of BHIM in practice, by considering benchmarks
from the literature, and generating timed variants of some of them. One of our
benchmarks is a variant of the Bluetooth example [11,23], where BHIM was
able to catch a known race detection error. Another interesting benchmark is
a model of a parameterized multiple producer consumer example, having parameters M, N on the quantities of two items A, B produced. Here, BHIM could
detect bugs by finding witnesses having just 2 holes, while, it is unlikely that existing tools working on scope/context bounded underapproximations can handle
them as the number of scope/context switches is dependent on M, N (in fact,
it is twice the least common multiple of M and N ). In the timed setting, one
of the main challenges has been the unavailability of timed benchmarks; even in
the untimed setting, many benchmarks were unavailable due to their proprietary
nature. Due to lack of space, proofs, technical details and parametric plots of
experiments are in [4].
Related Work. Among other under-approximations, scope bounded [27] subsumes context and round bounded underapproximations, and it also paves path
for GetaFix [21], a tool to analyze recursive (and multi-threaded) boolean programs. As mentioned earlier hole boundedness strictly subsumes scope boundedness. On the other hand, GetaFix uses symbolic approaches via BDDs, which is
orthogonal to the improvements made in this paper. Indeed, our next step would
be to build a symbolic version of BHIM which extends the hole-bounded approach
to work with symbolic methods. Given that BHIM can already handle synthetic
examples with 12-13 holes (see [4]), we expect this to lead to even more drastic
improvements and applicability. For sequential programs, a summary-based algorithm is used in [21]; summaries are like our well-nested sequences, except that
well-nested sequences admit contexts from different stacks unlike summaries. As
a result, our class of bounded hole behaviors generalizes summaries. Many other
different theoretical results like phase bounded [18], order bounded [8] which
gives interesting underapproximations of MPDA, are subsumed in tree-width
bounded behaviors, but they do not seem to have practical implementations.
Adding real-time information to pushdown automata by using clocks or timed
stacks has been considered, both in the discrete and dense-timed settings. Recently, there has been a flurry of theoretical results in the topic [10,1,2,5,6]. However, to the best of our knowledge none of these algorithms have been successfully
implemented (except [6] which implements a tree-automata based technique for
single-stack timed systems) for multi-stack systems. One reason is that these algorithms do not employ scalable fix-point based techniques, but instead depend
on region automaton-based search or tree automata-based search techniques.
2 Underapproximations in MPDA
A multi-stack pushdown automaton (MPDA) is a tuple M = (S, Δ, s 0 , S f ,
n, Σ, Γ ) where, S is a finite non-empty set of locations, Δ is a finite set of
389
several technical challenges which are specific to the timed setting. Implementing
this approach in BHIM makes it, to the best of our knowledge, the first tool that
can analyze timed multi-stack pushdown automata with closed guards.
We analyze the performance of BHIM in practice, by considering benchmarks
from the literature, and generating timed variants of some of them. One of our
benchmarks is a variant of the Bluetooth example [11,23], where BHIM was
able to catch a known race detection error. Another interesting benchmark is
a model of a parameterized multiple producer consumer example, having parameters M, N on the quantities of two items A, B produced. Here, BHIM could
detect bugs by finding witnesses having just 2 holes, while, it is unlikely that existing tools working on scope/context bounded underapproximations can handle
them as the number of scope/context switches is dependent on M, N (in fact,
it is twice the least common multiple of M and N ). In the timed setting, one
of the main challenges has been the unavailability of timed benchmarks; even in
the untimed setting, many benchmarks were unavailable due to their proprietary
nature. Due to lack of space, proofs, technical details and parametric plots of
experiments are in [4].
Related Work. Among other under-approximations, scope bounded [27] subsumes context and round bounded underapproximations, and it also paves path
for GetaFix [21], a tool to analyze recursive (and multi-threaded) boolean programs. As mentioned earlier hole boundedness strictly subsumes scope boundedness. On the other hand, GetaFix uses symbolic approaches via BDDs, which is
orthogonal to the improvements made in this paper. Indeed, our next step would
be to build a symbolic version of BHIM which extends the hole-bounded approach
to work with symbolic methods. Given that BHIM can already handle synthetic
examples with 12-13 holes (see [4]), we expect this to lead to even more drastic
improvements and applicability. For sequential programs, a summary-based algorithm is used in [21]; summaries are like our well-nested sequences, except that
well-nested sequences admit contexts from different stacks unlike summaries. As
a result, our class of bounded hole behaviors generalizes summaries. Many other
different theoretical results like phase bounded [18], order bounded [8] which
gives interesting underapproximations of MPDA, are subsumed in tree-width
bounded behaviors, but they do not seem to have practical implementations.
Adding real-time information to pushdown automata by using clocks or timed
stacks has been considered, both in the discrete and dense-timed settings. Recently, there has been a flurry of theoretical results in the topic [10,1,2,5,6]. However, to the best of our knowledge none of these algorithms have been successfully
implemented (except [6] which implements a tree-automata based technique for
single-stack timed systems) for multi-stack systems. One reason is that these algorithms do not employ scalable fix-point based techniques, but instead depend
on region automaton-based search or tree automata-based search techniques.
2 Underapproximations in MPDA
A multi-stack pushdown automaton (MPDA) is a tuple M = (S, Δ, s 0 , S f ,
n, Σ, Γ ) where, S is a finite non-empty set of locations, Δ is a finite set of