SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Thu 23 Oct 2014 14:15 - 14:37 at Salon F - Concurrency Chair(s): David Grove

Designing and implementing thread-safe multithreaded libraries can be a daunting task as developers of these libraries need to ensure that their implementations are free from concurrency bugs including deadlocks. The usual practice involves employing software testing and/or dynamic analysis to detect deadlocks. Their effectiveness is dependent on well-designed multithreaded test cases. Unsurprisingly, developing multithreaded tests is easily an order of magnitude harder than developing single threaded tests for obvious reasons.

In this paper, we address the problem of automatically synthesizing multithreaded tests that can induce deadlocks. The key insight to our approach is that a subset of the properties observed when a deadlock manifests in a concurrent execution can also be observed in a single threaded execution. We design a novel, automatic, scalable and directed approach that identifies these properties and synthesizes a multithreaded test that realizes these properties simultaneously revealing a potential deadlock. The input to our approach is only the library implementation under consideration and the output is a set of deadlock revealing multithreaded tests.

We have implemented our approach as part of our tool, named OMEN, and applied it on many multithreaded Java libraries. OMEN synthesizes multithreaded tests for all these libraries that include classes that are documented as thread-safe in COLT (a popular high performance scientific computing library) where it enables detection of 35 real deadlocks. Moreover, our experimental results show that randomized approaches for detecting deadlocks are ineffective. We also conducted a user study and found that software testing/dynamic analysis on multithreaded tests developed by the participants did not reveal any deadlocks either. Because the input to OMEN is the library implementation alone, it can be seamlessly integrated into the software development process.

Thu 23 Oct

Displayed time zone: Tijuana, Baja California change

13:30 - 15:00
ConcurrencyOOPSLA at Salon F
Chair(s): David Grove IBM Research
13:30
22m
Talk
Atlas: Leveraging Locks for Non-volatile Memory Consistency
OOPSLA
Dhruva Chakrabarti HP Labs, Hans-J. Boehm Google, Kumud Bhandari Rice University
Link to publication
13:52
22m
Talk
Fast Splittable Pseudorandom Number Generators
OOPSLA
Guy L. Steele Jr. Oracle Labs, Doug Lea State University of New York (SUNY) Oswego, Christine H. Flood Red Hat
Link to publication
14:15
22m
Talk
Multithreaded Test Synthesis for Deadlock Detection
OOPSLA
Malavika Samak Indian Institute of Science, Bangalore, Murali Krishna Ramanathan Indian Institute of Science, Bangalore
Link to publication
14:37
22m
Talk
Symbolic Execution of Multithreaded Programs from Arbitrary Program Contexts
OOPSLA
Tom Bergan University of Washington, Dan Grossman University of Washington, Luis Ceze University of Washington
Link to publication