Facebooks Android-App hatte ein Performance-Problem. Der UI-Thread ertrank in Arbeit, aber Code auf Background-Threads zu verschieben bedeutete Race Conditions. Crashes in der Produktion. Wütende Nutzer.

Sie haben das nicht mit besserem Code Review oder mehr Tests gelöst. Sie bauten einen Static Analyzer, RacerD, der Abstract Interpretation nutzt, um zu beweisen, ob zwei Threads gleichzeitig denselben mutable State berühren können. Er prüfte Millionen Zeilen Java. Er fand Tausende echte Races, bevor sie ausgeliefert wurden. Und das, indem er bewusst bei manchen Dingen falsch lag.

Race Conditions sind ein Kardinalitätsproblem

Androids Main-Thread kümmert sich um Zeichnen, Input und jede View-Mutation. Zu viel dort und Ihre App lässt Frames ausfallen. Der Fix scheint offensichtlich: Arbeit auf AsyncTask, HandlerThread oder Coroutines auslagern.

Das Problem ist, dass Androids UI-Toolkit nicht thread-safe ist. Eine TextView von einem Background-Thread zu mutieren wirft eine Exception. Aber die wirklichen Killer sind die stillen Races. Zwei Threads lesen und schreiben gemeinsamen Model-State. Das Interleaving, das explodiert, passiert nur auf dem Gerät eines bestimmten Nutzers, an einem Dienstag, mit langsamem Netzwerk.

Dynamische Erkennungstools können Races fangen, aber nur auf Ausführungspfaden, die Sie tatsächlich beim Testen treffen. Facebooks Codebase war zu groß und der State Space zu riesig. Sie mussten über Races wissen, ohne den Code auszuführen.

Abstract interpretation, aggressiv vereinfacht

RacerD basiert auf Abstract Interpretation, einer Technik zur statischen Programmanalyse. Statt exakte Programmstates zu tracken (unmöglich für große Codebases), baut man eine einfachere abstrakte Domain und beweist Eigenschaften über sie.

Das klassische Beispiel ist Interval Analysis. Man trackt nicht den exakten Wert von x. Man trackt, ob er positiv, negativ oder null ist. Die Analyse ist approximativ, aber sie skaliert.

RacerD wendet diese Idee auf Concurrency an. Es trackt drei Dinge pro Memory-Access:

  1. Welcher Thread den Zugriff ausführt (UI-Thread, Background-Thread oder unbekannt)
  2. Welcher Lock, falls vorhanden, ihn schützt
  3. Der Access Path (z. B. this.mUser.name)

Wenn zwei Zugriffe auf denselben Path auf verschiedenen Threads passieren können, und mindestens einer ein Write ist, und keiner von einem gemeinsamen Lock geschützt ist, meldet RacerD einen Race.

Das klingt, als sollte es für eine Multi-Million-Line-App untrackbar sein. Es wäre es auch, wenn sie versucht hätten, alles präzise zu modellieren.

Facebook machte RacerD absichtlich unsound. Es ignoriert Java-Generics, Reflection, virtuellen Dispatch in manchen Fällen und Aliasing-Komplexitäten, die die Analyse kubisch oder schlimmer machen würden. Die Mathematik ist brutal, also haben sie geschummelt. Das Ergebnis: lineare Zeitkomplexität pro Methode und die Fähigkeit, Facebooks App in unter einer Stunde zu analysieren.

Thread-Ownership und der @ThreadSafe-Vertrag

Die Analyse arbeitet, indem sie Methoden mit Thread-Constraints annotiert. Betrachten Sie diesen Ausschnitt:

@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 sieht getUser und setUser mit @AnyThread annotiert. Es stellt fest, dass mCurrentUser in beiden Fällen unter mLock zugegriffen wird. Kein Race wird gemeldet.

Entfernen Sie nun die synchronized-Blöcke:

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

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

RacerD markiert einen Race auf mCurrentUser. Zwei @AnyThread-Methoden greifen auf dasselbe Feld zu. Eine schreibt. Kein gemeinsamer Lock. Das ist ein präziser, handlungsbarer Report.

Die Annotations treiben die Analyse. @UiThread bedeutet, die Methode läuft nur auf dem Main-Thread. @WorkerThread bedeutet Background. Wenn eine @WorkerThread-Methode und eine @UiThread-Methode beide this.mData ohne Synchronisation berühren, ist das nur dann ein Race, wenn eine von ihnen schreibt. RacerD weiß das, weil es Read versus Write trackt.

Der Trade-off: Unsoundness im Austausch für Adoption

RacerD beweist nicht die Abwesenheit von Races. Es beweist das Vorhandensein wahrscheinlicher Races. Dieser Unterschied ist wichtig.

Ein sound Analyzer würde garantieren, dass wenn kein Race gemeldet wird, kein Race existiert. Soundness für concurrent Java zu erreichen erfordert das Modellieren des Memory-Models, aller möglichen Thread-Interleavings und präzises Pointer-Aliasing. Kein Tool macht das in Facebooks Größenordnung in vertretbarer Zeit.

Durch die Wahl der Unsoundness akzeptiert RacerD false negatives. Einige echte Races schlüpfen durch. Die Wette war, dass 90% der Races automatisch, nächtlich, über jeden Diff hinweg zu finden wertvoller ist als 100% der Races nie zu finden.

Die False-Positive-Rate musste niedrig bleiben. Ein Tool, das bei jeder dritten Methode wolfcries, wird deaktiviert. RacerD hielt False Positives unter 10%, indem es konservativ darüber berichtet, was es meldet. Es markiert keine Races, die thread-safe immutable Types involvieren. Es versteht, dass final-Felder nach der Konstruktion sicher sind. Es modelliert gängige Synchronisations-Patterns.

Wie Facebook es deployed hat

RacerD lief auf jedem Code-Diff, bevor er gelandet ist. Es war Teil von Infer, ihrem open-source Static-Analysis-Framework. Ingenieure sahen Race-Reports in Phabricator (ihrem Code-Review-Tool) neben Unit-Test-Ergebnissen.

Der Workflow sah so aus:

  1. Ingenieur reicht einen Diff ein, der einen Background-Thread-Zugriff auf shared state hinzufügt.
  2. Infer führt RacerD auf den modifizierten Methoden aus.
  3. Wenn ein Race gefunden wird, bekommt der Diff ein blocking signal. Der Ingenieur muss ihn fixen oder explizit suppressen.

Das hat die Last nach links verschoben. Race Conditions wurden während des Reviews gefangen, nicht in Production-Crashes.

Facebook hat Infer, einschließlich RacerD, 2015 open-sourced. Sie können es heute auf Java, C, C++ und Objective-C ausführen.

Infer auf eigenem Android-Code ausführen

Wenn Sie das ausprobieren wollen, Infer ist ein einzelnes Binary. Installieren Sie es über Homebrew oder laden Sie ein Release herunter:

brew install infer

Führen Sie es auf Ihrem Gradle-Projekt aus:

infer run -- ./gradlew build

Infer kompiliert Ihr Projekt und analysiert den Bytecode. Für Race Detection speziell fügen Sie Thread-Annotations zu Ihrem Code hinzu. Infer liefert mit 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
    }
}

Der Report sagt Ihnen die Datei, Zeile und den widersprüchlichen Zugriff. Fixen Sie es mit Synchronisation, einer Atomic Reference oder indem Sie den State in ein Thread-confined-Model verschieben.

Wo das zusammenbricht

RacerD ist keine Silver Bullet. Es hat Probleme mit Races durch nicht-offensichtliche Aliases, Races in nativem Code und Races, die durch Frameworks vermittelt werden, die es nicht modelliert. Wenn Sie RxJava oder Coroutines mit komplexem Thread-Hopping nutzen, erfassen die Thread-Annotations den tatsächlichen Ausführungskontext möglicherweise nicht.

Es erfordert auch Disziplin. Wenn Sie in Ihren Annotations lügen, lügt die Analyse zurück. Eine Methode @UiThread zu markieren, wenn sie tatsächlich von einem Background-Thread aufgerufen wird, untergräbt den Zweck.

Die wahre Lektion

Facebooks Erkenntnis war nicht, dass Abstract Interpretation magisch ist. Es war, dass eine leicht falsche Analyse, die kontinuierlich bei jeder Änderung läuft, eine perfekte Analyse schlägt, die nie läuft.

Wenn Sie heute concurrent Android-Code bauen, müssen Sie RacerD nicht selbst bauen. Sie können Infer adoptieren, oder Sie können dasselbe Prinzip anwenden: modellieren, welche Threads welchen State berühren, erzwingen Sie es mit Static Analysis, und behandeln Sie Thread-Safety als Compile-Time-Angelegenheit, nicht als Production-Debugging.

Ihre Nutzer werden sich nicht für die Races bedanken, die Sie verhindert haben. Sie werden Ihre App einfach nicht deinstallieren.