Static deadlock analysis for Android, scaled to billions of lines

Meta has open-sourced a new static analyzer for Java deadlocks on Android, built on top of the Infer framework. The tool is designed to analyze every commit across Meta’s Android app family, a codebase that reaches hundreds of millions of lines. Over the past two years, developers have acted on more than 200 of its reports, with a fix rate of roughly 54 percent.

The analyzer never executes the code it inspects. Instead, it relies on abstract interpretation to build a compositional summary for each method, recording how the method acquires and releases locks and whether it runs on the main thread or a background thread. Each method is summarized at most once, and the summaries feed directly into the analysis of callers, which keeps performance predictable at scale.

The summary’s core component is a set of critical pairs. A critical pair (A, B) captures the fact that a method tries to acquire lock B while holding precisely the set of locks A. Aggregating these pairs across all methods makes it possible to determine whether two concurrent methods can deadlock.

To stay efficient, the tool avoids a full scan of the app. It starts by processing every method in the modified files of a given revision. A heuristic then identifies methods elsewhere in the codebase that could deadlock with those newly changed methods. That two-phase approach is what allows the analysis to scale to Meta-sized repositories.

Formal guarantees

The accompanying paper proves that the analysis is both sound and complete for an abstract language with non-deterministic control flow. In that idealized setting, the tool can detect every possible deadlock without producing false positives. The paper covers the full formal model and its assumptions.

Why static detection matters

Deadlocks are typically unrecoverable at runtime and notoriously difficult to reproduce, since thread scheduling is non-deterministic. A bug may need thousands or millions of test runs to surface. Analyzing code statically — without building it — sidesteps that problem entirely. The analyzer achieves this without sacrificing the scalability required to run on very large, continuously integrated codebases.

The tool and its source code are available as part of the open-source Infer framework.