  Previous approaches to systematic state-space exploration for testing
multi-threaded programs have proposed context-bounding and depth-bounding to be
effective ranking algorithms for testing multithreaded programs. This paper
proposes two new metrics to rank thread schedules for systematic state-space
exploration. Our metrics are based on characterization of a concurrency bug
using v (the minimum number of distinct variables that need to be involved for
the bug to manifest) and t (the minimum number of distinct threads among which
scheduling constraints are required to manifest the bug). Our algorithm is
based on the hypothesis that in practice, most concurrency bugs have low v
(typically 1- 2) and low t (typically 2-4) characteristics. We iteratively
explore the search space of schedules in increasing orders of v and t. We show
qualitatively and empirically that our algorithm finds common bugs in fewer
number of execution runs, compared with previous approaches. We also show that
using v and t improves the lower bounds on the probability of finding bugs
through randomized algorithms.
  Systematic exploration of schedules requires instrumenting each variable
access made by a program, which can be very expensive and severely limits the
applicability of this approach. Previous work [5, 19] has avoided this problem
by interposing only on synchronization operations (and ignoring other variable
accesses). We demonstrate that by using variable bounding (v) and a static
imprecise alias analysis, we can interpose on all variable accesses (and not
just synchronization operations) at 10-100x less overhead than previous
approaches.
