Detecting Potential Deadlocks with Static Analysis and Runtime Monitoring.
Rahul Agarwal, Liqiang Wang, and Scott D. Stoller

Concurrent programs are notorious for containing errors that are difficult to reproduce and diagnose. A common kind of concurrency error is a deadlock which occurs when a set of threads is blocked each trying to acquire a lock held by another thread in that set. Both static and dynamic (run-time) analysis techniques exist to detect deadlocks. The GoodLock algorithm can detect potential deadlocks at run-time. However, it detects only potential deadlocks involving two threads, i.e., each of those threads is blocked trying to acquire a lock held by the other thread. This paper presents a generalized version of the GoodLock algorithm that detects potential deadlocks involving any number of threads. Run-time checking may miss errors in unexecuted code. On the other hand, run-time checking generally produces fewer false alarms than static analysis; this is a significant practical advantage, since diagnosing all of the warnings from static analysis of large codebases may be expensive. This paper explores the use of static analysis to significantly decrease the overhead of run-time checking. Our approach is based on a type system for analyzing deadlocks. We extend our type system, Extended Parameterized Atomic Java (EPAJ), which ensures absence of races and atomicity violations, with Boyapati et al.'s deadlock types. A static type inference algorithm is used to infer deadlock types. Run-time checking can safely be omitted for typable parts of the program. The approach is completely automatic, and significantly reduces the overhead of run-time checking for potential deadlocks. The resulting type system, called Deadlock-Free EPAJ (DEPAJ), has the added benefit of giving stronger atomicity guarantees than previous atomicity type systems, which do not consider deadlocks and hence may classify a method as atomic even if it could deadlock in the middle---something that cannot happen if the method executes without interruption by other threads.

PDF, BibTeX