In a joint research, London University College and Facebook researchers created a new deadlock detector for Android Java code now available as part of open-source Infer static analysis tool. The new analyzer is able to process large codebases efficiently thanks to its incremental approach specifically designed for integration in a CI pipeline.
In the paper describing their results, the researchers show the core algorithm of the deadlock analysis tool runs in quasi-exponential (NP) time.
The first step in the analysis is modelling the real code through an abstract language that can be seen as a simplified model of Java and supports nested, re-entrant locks, non-deterministic iteration and branching, and non-recursive procedure calls. All other details of the language, including variable and memory assignment, are not modelled.
For each method, the analyzer computes a summary of how the method behaves in terms of lock acquisition and release, as well as whether the method will run on the main thread or on a background thread.
The summary for a method includes a list of all locks that it tries to acquire along with any lock that it is holding at the same time. This data is used to build a list of critical pairs (A, B), where A and B are the two mentioned locks.
This data, computed across all methods, is enough to let us answer the question of whether a deadlock is possible between two concurrent methods.
To maximize performance, the analyzer does not analyze the entire codebase at once. Instead, it processes only the methods that were modified in a given revision, then attempts to identify all other methods that could deadlock with any of the methods in the revision. This is the key aspect to making the new analyzer efficient with large codebases and it sets it apart from other deadlock analysis tools, be they static, dynamic, or hybrid, say the researchers.
The deadlock analyzer has been used at Facebook for the last two years as part of their CI pipeline, which runs Infer for each commit submitted to code review. According to Facebook, the deadlock analyzer has processed hundreds of thousands of commits and generated over 500 deadlock reports, of which 54% were fixed. Each run took an average 213 seconds per commit to complete.
A part of those non-fixed reports are related to false positives, e.g. a reported deadlock between two methods that cannot run concurrently. In other cases, the developer decided not to fix the deadlock due to its unlikeliness, or the fix was provided through an unrelated commit. Unfortunately, Facebook cannot provide precise figure for each of these categories so it is not clear how frequent false positives were.
