Symbolic Deadlock Analysis in Concurrent Libraries and Their Clients

Methods in object-oriented concurrent libraries hide internal synchronization details. However, information hiding may result in clients causing thread safety violations by invoking methods in an unsafe manner. Given such a library, we present a technique for inferring interface contracts that specify permissible concurrent method calls and patterns of aliasing among method arguments, such that the derived contracts guarantee deadlock free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding for tracking lock dependencies, allowing us to synthesize contracts using a SMT solver. Our prototype tool analyzes over a million lines of code for some widely-used Java libraries within an hour, thus demonstrating its scalability and efficiency. Furthermore, the contracts inferred by our approach have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have been a part of bug-reports filed by users and developers of the client code.