Synthesizing Multi-threaded Tests from Sequential Traces to Detect Communication Deadlocks

Abstract

Multi-threaded libraries, including the ones advertised as thread-safe, may contain concurrency bugs, and worse, may not include relevant test cases that can drive the program execution towards bug-prone interleavings. Also, the effectiveness of dynamic verification, a prominent concurrency bug detection technique, depends critically on the availability of relevant test cases. Generating such test cases automatically to assist dynamic verification is, therefore, a significant problem. Among hard-to-detect concurrency bugs in multi-threaded Java libraries are communication deadlocks, which occur due to the incorrect usage of wait() and notify() communication primitives. In this work, we present a novel technique to systematically synthesize multi-threaded test cases to expose communication deadlocks. We model these deadlocks as global constraints over the events of two sequential program traces of the library APIs. The task of predicting the relevance of combining two sequential program traces is delegated to an SMT solver. We implement our technique in a prototype tool named Revelio, and evaluate it on fifteen classes of popular multi-threaded Java libraries. We find that Revelio is able to synthesize precise tests exposing communication deadlocks, which the state-of-the-art tools cannot.