Language Strength Reduction
Nicholas Kidd, Akash Lal, and Thomas Reps
This paper concerns methods to check for atomic-set
serializability violations in concurrent Java programs. The straightforward
way to encode a reentrant lock is to model it with a context-free language
to track the number of successive lock acquisitions. We present
a construction that replaces the context-free language that describes a
reentrant lock by a regular language that describes a non-reentrant lock.
We call this replacement language strength reduction. Language strength
reduction produces an average speedup (geometric mean) of 3.4. Moreover,
for 2 programs that previously exhausted available space, the tool
is now able to run to completion.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)
University of Wisconsin