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.
e give a general reduction from a concurrent program P,
and a given context bound K, to a slightly larger
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 the 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)
University of Wisconsin