Variable and Thread Bounding for Systematic Testing of Multithreaded Programs

TL;DR

This paper introduces variable and thread bounding metrics to improve systematic testing of multithreaded programs, enabling more efficient bug detection by focusing on low-v and low-t characteristics, reducing overhead and increasing bug-finding effectiveness.

Contribution

It proposes new metrics based on variable and thread bounds for ranking schedules, and demonstrates their effectiveness in finding bugs more efficiently than prior methods.

Findings

Finds common bugs with fewer execution runs.

Improves lower bounds on bug detection probability.

Reduces overhead in variable access instrumentation by 10-100x.

Abstract

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.