L’application Android de Facebook avait un problème de performance. Le thread UI était noyé sous le travail, mais déplacer du code vers des threads d’arrière-plan signifiait des race conditions. Des crashes en production. Des utilisateurs en colère.

Ils n’ont pas résolu cela avec de meilleures revues de code ou plus de tests. Ils ont construit un analyseur statique, RacerD, qui utilise l’interprétation abstraite pour prouver si deux threads peuvent toucher le même état mutable en même temps. Il a vérifié des millions de lignes de Java. Il a trouvé des milliers de races réelles avant qu’elles ne soient livrées. Et il a fait cela en se tromphant délibérément sur certaines choses.

Les race conditions sont un problème de cardinalité

Le thread principal d’Android gère le dessin, les entrées et chaque mutation de View. En faire trop là-bas et votre application perd des frames. Le correctif semble évident : décharger le travail vers AsyncTask, HandlerThread ou des coroutines.

Le problème est que la boîte à outils UI d’Android n’est pas thread-safe. Muter une TextView depuis un thread d’arrière-plan lance une exception. Mais les vrais tueurs sont les races silencieuses. Deux threads lisent et écrivent un état de modèle partagé. L’entrelacement qui explose n’arrive que sur l’appareil d’un utilisateur spécifique, un mardi, avec un réseau lent.

Les outils de détection dynamique peuvent attraper des races, mais uniquement sur les chemins d’exécution que vous atteignez réellement lors des tests. La codebase de Facebook était trop grande et l’espace d’états trop vaste. Ils avaient besoin de connaître les races sans exécuter le code.

Interprétation abstraite, agressivement simplifiée

RacerD est construit sur l’interprétation abstraite, une technique d’analyse statique de programmes. Au lieu de suivre des états de programme exacts (impossible pour les grandes codebases), vous construisez un domaine abstrait plus simple et vous prouvez des propriétés à son sujet.

L’exemple classique est l’analyse d’intervalles. Vous ne suivez pas la valeur exacte de x. Vous suivez si elle est positive, négative ou nulle. L’analyse est approximative, mais elle passe à l’échelle.

RacerD applique cette idée à la concurrence. Il suit trois choses par accès mémoire :

  1. Quel thread effectue l’accès (thread UI, thread d’arrière-plan ou inconnu)
  2. Quel lock, s’il y en a un, le protège
  3. Le chemin d’accès (par exemple, this.mUser.name)

Si deux accès au même chemin peuvent arriver sur des threads différents, et qu’au moins un est une écriture, et qu’aucun n’est protégé par un lock commun, RacerD signale une race.

Cela semble comme si cela devrait être intractable pour une application de plusieurs millions de lignes. Ce le serait, s’ils essayaient de tout modéliser avec précision.

Facebook a rendu RacerD intentionnellement unsound. Il ignore les génériques Java, la réflexion, le dispatch virtuel dans certains cas, et les complexités d’aliasing qui rendraient l’analyse cubique ou pire. Les mathématiques sont brutales, alors ils ont triché. Le résultat : une complexité temporelle linéaire par méthode, et la capacité d’analyser l’application de Facebook en moins d’une heure.

Propriété des threads et le contrat @ThreadSafe

L’analyse fonctionne en annotant les méthodes avec des contraintes de thread. Considérez cet extrait :

@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 voit getUser et setUser annotés avec @AnyThread. Il note que mCurrentUser est accédé sous mLock dans les deux cas. Aucune race n’est signalée.

Maintenant retirez les blocs synchronized :

@AnyThread
public User getUser() {
    return mCurrentUser;  // lecture non synchronisée
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // écriture non synchronisée
}

RacerD signale une race sur mCurrentUser. Deux méthodes @AnyThread accèdent au même champ. L’une écrit. Pas de lock commun. C’est un rapport précis et actionnable.

Les annotations pilotent l’analyse. @UiThread signifie que la méthode ne s’exécute que sur le thread principal. @WorkerThread signifie l’arrière-plan. Si une méthode @WorkerThread et une méthode @UiThread touchent toutes deux this.mData sans synchronisation, ce n’est une race que si l’une d’elles écrit. RacerD le sait car il suit la lecture par rapport à l’écriture.

Le trade-off : l’insoundness en échange de l’adoption

RacerD ne prouve pas l’absence de races. Il prouve la présence de races probables. Cette distinction est importante.

Un analyseur sound garantirait que si aucune race n’est signalée, aucune race n’existe. Atteindre la soundness pour du Java concurrent nécessite de modéliser le modèle mémoire, tous les entrelacements de threads possibles, et l’aliasing de pointeurs avec précision. Aucun outil ne fait cela à l’échelle de Facebook en un temps raisonnable.

En choisissant l’insoundness, RacerD accepte les faux négatifs. Certaines races réelles passent à travers. Le pari était que trouver 90% des races automatiquement, chaque nuit, à chaque diff, est plus précieux que de trouver 100% des races jamais.

Le taux de faux positifs devait rester bas. Un outil qui crie au loup à chaque troisième méthode est désactivé. RacerD a maintenu les faux positifs sous 10% en étant conservateur sur ce qu’il rapporte. Il ne signale pas les races impliquant des types immuables thread-safe. Il comprend que les champs final sont sûrs après la construction. Il modélise les patterns de synchronisation communs.

Comment Facebook l’a déployé

RacerD tournait sur chaque diff de code avant qu’il n’atterrisse. Il faisait partie d’Infer, leur framework d’analyse statique open source. Les ingénieurs voyaient les rapports de races dans Phabricator (leur outil de revue de code) aux côtés des résultats des tests unitaires.

Le flux de travail ressemblait à ceci :

  1. L’ingénieur soumet un diff qui ajoute un accès de thread d’arrière-plan à un état partagé.
  2. Infer exécute RacerD sur les méthodes modifiées.
  3. Si une race est trouvée, le diff reçoit un signal bloquant. L’ingénieur doit la corriger ou la supprimer explicitement.

Cela a déplacé la charge vers la gauche. Les race conditions étaient capturées pendant la revue, pas dans les crashes de production.

Facebook a rendu Infer open source, y compris RacerD, en 2015. Vous pouvez l’exécuter aujourd’hui sur Java, C, C++ et Objective-C.

Exécuter Infer sur votre propre code Android

Si vous voulez essayer cela, Infer est un binaire unique. Installez-le via Homebrew ou téléchargez une release :

brew install infer

Exécutez-le sur votre projet Gradle :

infer run -- ./gradlew build

Infer compilera votre projet et analysera le bytecode. Pour la détection de races spécifiquement, ajoutez des annotations de thread à votre code. Infer inclut des annotations dans 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 rapporte : race sur mToken
    }
}

Le rapport vous indique le fichier, la ligne et l’accès conflictuel. Corrigez-le avec de la synchronisation, une référence atomique, ou en déplaçant l’état vers un modèle confiné à un thread.

Où cela s’effondre

RacerD n’est pas une balle d’argent. Il a des difficultés avec les races à travers des aliases non évidents, les races dans du code natif, et les races médiées par des frameworks qu’il ne modélise pas. Si vous utilisez RxJava ou des coroutines avec des sauts de threads complexes, les annotations de threads peuvent ne pas capturer le contexte d’exécution réel.

Cela nécessite aussi de la discipline. Si vous mentez dans vos annotations, l’analyse ment en retour. Marquer une méthode @UiThread quand elle est en fait appelée depuis un thread d’arrière-plan défait le but.

La vraie leçon

L’aperçu de Facebook n’était pas que l’interprétation abstraite est magique. C’était qu’une analyse légèrement incorrecte, exécutée en continu à chaque changement, bat une analyse parfaite exécutée jamais.

Si vous construisez du code Android concurrent aujourd’hui, vous n’avez pas besoin de construire RacerD vous-même. Vous pouvez adopter Infer, ou vous pouvez appliquer le même principe : modélisez quels threads touchent quel état, faites-le respecter avec l’analyse statique, et traitez la sécurité des threads comme une préoccupation en temps de compilation, pas de débogage en production.

Vos utilisateurs ne vous remercieront pas pour les races que vous avez prévenues. Ils désinstalleront simplement pas votre application.