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 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00 | |||
13:30 22mTalk | Atlas: Leveraging Locks for Non-volatile Memory Consistency OOPSLA Link to publication | ||
13:52 22mTalk | 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 22mTalk | 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 22mTalk | 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 |