Variable and Thread Bounding for Systematic Testing of Multithreaded Programs

Previous approaches to systematic state-space exploration for test-ing multi-threaded programs have proposed context-bounding [20] and depth-bounding [6] to be effective ranking algorithms for test-ing 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 in-volved 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 com-mon bugs in fewer number of execution runs, compared with pre-vious approaches. We also show that using v and t improves the lower bounds on the probability of finding bugs through random-ized algorithms. Systematic exploration of schedules requires instrumenting each variable access made by a program, which can be very ex-pensive and severely limits the applicability of this approach. Pre-vious work [6, 20] 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