Reducing Concurrent Analysis Under a Context Bound to
Sequential Analysis
Akash Lal and Thomas Reps
This paper addresses the analysis of concurrent programs with shared
memory. Such an analysis is undecidable in the presence of multiple
procedures. One approach used in recent work obtains
decidability by providing only a partial guarantee of
correctness: the approach bounds the number of context switches allowed
in the concurrent program, and aims to prove safety, or find bugs,
under the given bound. In this paper, we show how to obtain simple and
efficient algorithms for the analysis of concurrent programs with a
context bound. We give a general reduction from a concurrent program
P, and a given context bound K, to a sequential
program PsK such that the analysis of
PsK can be used to prove
properties about P. The reduction introduces symbolic constants and
assume statements in PsK.
Thus, any sequential analysis that can
deal with these two additions can be extended to handle concurrent
programs as well, under a context bound.
We give instances of the reduction for common
program models used in model checking, such as Boolean programs,
pushdown systems (PDSs), and symbolic PDSs.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)
University of Wisconsin