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.