Meta has developed a static analyzer that detects deadlocks in Android Java code without even running the code itself. It is capable of auditing codebases with hundreds of millions of lines.

The analyzer is deployed on the Meta continuous integration system, where it scans every commit in the Android app family. Over the past two years, developers have made over 200 fixes in response to deadlock reports, accounting for about 54% of all fixes.

The Meta analyzer is open source and is part of the Infer static analysis system.

The developers used methods of abstract interpretation. For each method, the parser calculates a summary of how it will behave in terms of acquiring and releasing the lock, as well as whether the method will run on the main thread or a background thread. This is done in a compositional manner: each method is summarized at most once, and the summary is used when the callers are summarized, which provides predictable high performance.

The central part of the method is the set of critical pairs. The critical pair (A,B) captures the following fact: a method is trying to acquire a lock on B, and at that time it already holds exactly that many locks in set A. This data, computed over all methods, is enough to answer the question of whether deadlock between two concurrent methods.

The tool does not parse all source files in the application. Instead, it first processes all methods in changed revision files. Then, based on this data, it applies heuristics to find methods outside the revision that could potentially block one of them in the revision.

The developers claim that their approach makes the analyzer scalable enough to be deployed on large codebases in Meta.

bbabo.Net