Directed Synthesis of Failing Concurrent Executions
Detecting concurrency-induced bugs in multithreaded libraries can be challenging due to the intricacies associated with their manifestation. This includes invocation of multiple methods, synthesis of inputs to the methods to reach the failing location, and crafting of thread interleavings that cause the erroneous behavior. Neither fuzzing-based testing techniques nor over-approximate static analyses are well positioned to detect such subtle defects while retaining high accuracy alongside satisfactory coverage.
In this paper, we propose a directed, iterative and scalable testing engine that combines the strengths of static and dynamic analysis to help synthesize concurrent executions to expose complex concurrency-induced bugs. Our engine accepts as input the library, its client (either sequential or concurrent) and a specification of correctness. Then, it iteratively refines the client to generate an execution that can break the input specification. Each step of the iterative process includes statically identifying sub-goals towards the goal of failing the specification, generating a plan toward meeting these goals, and merging of the paths traversed dynamically with the plan computed statically via constraint solving to generate a new client. The engine reports full reproduction scenarios, guaranteed to be true, for the bugs it finds.
We have created a prototype of our approach named MINION. We validated MINION by applying it to well-tested concurrent classes from popular Java libraries, including the latest versions of openjdk and google-guava. We were able to detect 31 real crashes across 10 classes in a total of 23 minutes, including previously unknown bugs. Comparison with three other tools reveals that combined, they report only 9 of the 31 crashes (and no other crashes beyond MINION). This is because several of these bugs manifest under deeply nested path conditions (observed
maximum of 11), deep nesting of method invocations (observed maximum of 6) and multiple refinement iterations to generate the crash-inducing client.
Thu 3 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10
Concurrency Analysis and Model CheckingOOPSLA at Matterhorn 1
Chair(s): Thomas Gross ETH Zurich
|Directed Synthesis of Failing Concurrent Executions|
Malavika Samak Indian Institute of Science, Bangalore, Omer Tripp IBM Research, USA, Murali Krishna Ramanathan Indian Institute of Science, BangaloreDOI Media Attached
|Maximal Causality Reduction for TSO and PSO|
Shiyou Huang Texas A&M University, Jeff Huang Texas A&M UniversityDOI
|Stateless Model Checking with Data-Race Preemption Points|
Ben Blum Carnegie Mellon University, Garth Gibson Carnegie Mellon UniversityDOI Pre-print Media Attached
|Precise and Maximal Race Detection from Incomplete Traces|
Jeff Huang Texas A&M University, Arun Krishnakumar Rajagopalan Texas A&M UniversityDOI Media Attached