Facebook’s Android app had a performance problem. The UI thread was drowning in work, but moving code to background threads meant race conditions. Crashes in production. Angry users.

They didn’t solve this with better code review or more tests. They built a static analyzer, RacerD, that uses abstract interpretation to prove whether two threads can touch the same mutable state at the same time. It checked millions of lines of Java. It found thousands of real races before they shipped. And it did this by deliberately being wrong about some things.

Race conditions are a cardinality problem

Android’s main thread handles drawing, input, and every View mutation. Do too much there and your app drops frames. The fix seems obvious: offload work to AsyncTask, HandlerThread, or coroutines.

The problem is that Android’s UI toolkit is not thread-safe. Mutating a TextView from a background thread throws. But the real killers are the silent races. Two threads read and write shared model state. The interleaving that explodes only happens on a specific user’s device, on a Tuesday, with slow network.

Dynamic detection tools can catch races, but only on execution paths you actually hit in testing. Facebook’s codebase was too large and the state space too big. They needed to know about races without running the code.

Abstract interpretation, aggressively simplified

RacerD is built on abstract interpretation, a technique for static program analysis. Instead of tracking exact program states (impossible for large codebases), you build a simpler abstract domain and prove properties about it.

The classic example is interval analysis. You don’t track the exact value of x. You track whether it is positive, negative, or zero. The analysis is approximate, but it scales.

RacerD applies this idea to concurrency. It tracks three things per memory access:

  1. Which thread performs the access (UI thread, background thread, or unknown)
  2. What lock, if any, protects it
  3. The access path (e.g., this.mUser.name)

If two accesses to the same path can happen on different threads, and at least one is a write, and neither is guarded by a common lock, RacerD reports a race.

This sounds like it should be intractable for a multi-million-line app. It would be, if they tried to model everything precisely.

Facebook made RacerD intentionally unsound. It ignores Java generics, reflection, virtual dispatch in some cases, and aliasing complexities that would make the analysis cubic or worse. The math is brutal, so they cheated. The result: linear time complexity per method, and the ability to analyze Facebook’s app in under an hour.

Thread ownership and the @ThreadSafe contract

The analysis works by annotating methods with thread constraints. Consider this snippet:

@ThreadSafe
public class UserRepository {
    private User mCurrentUser;
    private final Object mLock = new Object();

    @AnyThread
    public User getUser() {
        synchronized (mLock) {
            return mCurrentUser;
        }
    }

    @AnyThread
    public void setUser(User user) {
        synchronized (mLock) {
            mCurrentUser = user;
        }
    }
}

RacerD sees getUser and setUser annotated with @AnyThread. It notes that mCurrentUser is accessed under mLock in both cases. No race is reported.

Now remove the synchronized blocks:

@AnyThread
public User getUser() {
    return mCurrentUser;  // unsynchronized read
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // unsynchronized write
}

RacerD flags a race on mCurrentUser. Two @AnyThread methods access the same field. One writes. No common lock. This is a precise, actionable report.

The annotations drive the analysis. @UiThread means the method runs only on the main thread. @WorkerThread means background. If a @WorkerThread method and a @UiThread method both touch this.mData without synchronization, that is only a race if one of them writes. RacerD knows this because it tracks read versus write.

The trade-off: unsoundness in exchange for adoption

RacerD does not prove the absence of races. It proves the presence of likely races. This distinction matters.

A sound analyzer would guarantee that if no race is reported, no race exists. Achieving soundness for concurrent Java requires modeling the memory model, all possible thread interleavings, and pointer aliasing precisely. No tool does this at Facebook’s scale in reasonable time.

By choosing unsoundness, RacerD accepts false negatives. Some real races slip through. The bet was that finding 90% of races automatically, nightly, across every diff, is more valuable than finding 100% of races never.

The false positive rate had to stay low. A tool that cries wolf on every third method gets disabled. RacerD kept false positives under 10% by being conservative about what it reports. It does not flag races involving thread-safe immutable types. It understands that final fields are safe after construction. It models common synchronization patterns.

How Facebook deployed it

RacerD ran on every code diff before it landed. It was part of Infer, their open-source static analysis framework. Engineers saw race reports in Phabricator (their code review tool) alongside unit test results.

The workflow looked like this:

  1. Engineer submits a diff that adds a background thread access to shared state.
  2. Infer runs RacerD on the modified methods.
  3. If a race is found, the diff gets a blocking signal. The engineer must fix it or explicitly suppress it.

This shifted the burden left. Race conditions were caught during review, not in production crashes.

Facebook open-sourced Infer, including RacerD, in 2015. You can run it today on Java, C, C++, and Objective-C.

Running Infer on your own Android code

If you want to try this, Infer is a single binary. Install it via Homebrew or download a release:

brew install infer

Run it on your Gradle project:

infer run -- ./gradlew build

Infer will compile your project and analyze the bytecode. For race detection specifically, add thread annotations to your code. Infer ships with annotations in com.facebook.infer.annotation:

import com.facebook.infer.annotation.ThreadSafe;
import com.facebook.infer.annotation.AnyThread;
import com.facebook.infer.annotation.UiThread;

@ThreadSafe
public class SessionManager {
    private String mToken;

    @AnyThread
    public void setToken(String token) {
        mToken = token;  // Infer reports: race on mToken
    }
}

The report tells you the file, line, and conflicting access. Fix it with synchronization, an atomic reference, or by moving state to a thread-confined model.

Where this breaks down

RacerD is not a silver bullet. It struggles with races through non-obvious aliases, races in native code, and races mediated by frameworks it does not model. If you use RxJava or coroutines with complex thread hopping, the thread annotations may not capture the actual execution context.

It also requires discipline. If you lie in your annotations, the analysis lies back. Marking a method @UiThread when it is actually called from a background thread defeats the purpose.

The real lesson

Facebook’s insight was not that abstract interpretation is magical. It was that a slightly wrong analysis, run continuously on every change, beats a perfect analysis run never.

If you are building concurrent Android code today, you do not need to build RacerD yourself. You can adopt Infer, or you can apply the same principle: model which threads touch which state, enforce it with static analysis, and treat thread safety as a compile-time concern, not a production-debugging one.

Your users will not thank you for the races you prevented. They will simply not uninstall your app.