O aplicativo Android do Facebook tinha um problema de performance. A thread da interface estava afogada em trabalho, mas mover código para threads de fundo significava race conditions. Crashes em produção. Usuários irritados.

Eles não resolveram isso com revisões de código melhores ou mais testes. Eles construíram um analyzer estático, RacerD, que usa interpretação abstrata para provar se duas threads podem tocar o mesmo estado mutável ao mesmo tempo. Ele verificou milhões de linhas de Java. Encontrou milhares de corridas reais antes de enviá-las. E fez isso sendo deliberadamente errado sobre algumas coisas.

race conditions são um problema de cardinalidade

A thread principal do Android lida com desenho, entrada e cada mutação de View. Fazer muito lá e seu aplicativo perde frames. A correção parece óbvia: transferir trabalho para AsyncTask, HandlerThread ou coroutines.

O problema é que o kit de ferramentas de interface do Android não é thread-safe. Mutar uma TextView de uma thread de fundo lança uma exceção. Mas os verdadeiros assassinos são as corridas silenciosas. Duas threads leem e escrevem estado compartilhado do modelo. O interleaving que explode só acontece no dispositivo de um usuário específico, em uma terça-feira, com rede lenta.

Ferramentas de detecção dinâmica podem capturar corridas, mas apenas em caminhos de execução que você realmente atinge nos testes. A codebase do Facebook era muito grande e o espaço de estados muito grande. Eles precisavam saber sobre corridas sem executar o código.

Interpretação abstrata, agressivamente simplificada

RacerD é construído sobre interpretação abstrata, uma técnica de análise estática de programas. Em vez de rastrear estados exatos do programa (impossível para grandes codebases), você constrói um domínio abstrato mais simples e prova propriedades sobre ele.

O exemplo clássico é análise de intervalos. Você não rastreia o valor exato de x. Você rastreia se é positivo, negativo ou zero. A análise é aproximada, mas escala.

RacerD aplica essa ideia à concorrência. Ele rastreia três coisas por acesso à memória:

  1. Qual thread realiza o acesso (thread da interface, thread de fundo ou desconhecida)
  2. Qual lock, se houver, o protege
  3. O caminho de acesso (por exemplo, this.mUser.name)

Se dois acessos ao mesmo caminho podem acontecer em threads diferentes, e pelo menos um é uma escrita, e nenhum é protegido por um lock comum, RacerD reporta uma corrida.

Isso soa como deveria ser intratável para um aplicativo de milhões de linhas. Seria, se tentassem modelar tudo com precisão.

O Facebook tornou o RacerD intencionalmente unsound. Ele ignora generics Java, reflection, dispatch virtual em alguns casos, e complexidades de aliasing que tornariam a análise cúbica ou pior. A matemática é brutal, então eles trapacearam. O resultado: complexidade de tempo linear por método, e a capacidade de analisar o aplicativo do Facebook em menos de uma hora.

Propriedade de threads e o contrato @ThreadSafe

A análise funciona anotando métodos com restrições de thread. Considere este trecho:

@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 vê getUser e setUser anotados com @AnyThread. Ele nota que mCurrentUser é acessado sob mLock em ambos os casos. Nenhuma corrida é reportada.

Agora remova os blocos synchronized:

@AnyThread
public User getUser() {
    return mCurrentUser;  // leitura não sincronizada
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // escrita não sincronizada
}

RacerD sinaliza uma corrida em mCurrentUser. Dois métodos @AnyThread acessam o mesmo campo. Um escreve. Nenhum lock comum. Este é um relatório preciso e acionável.

As anotações impulsionam a análise. @UiThread significa que o método roda apenas na thread principal. @WorkerThread significa em segundo plano. Se um método @WorkerThread e um método @UiThread tocam this.mData sem sincronização, isso só é uma corrida se um deles escrever. RacerD sabe disso porque rastreia leitura versus escrita.

O trade-off: insoundness em troca de adoção

RacerD não prova a ausência de corridas. Ele prova a presença de corridas prováveis. Essa distinção importa.

Um analyzer sound garantiria que se nenhuma corrida é reportada, nenhuma corrida existe. Alcançar soundness para Java concorrente requer modelar o modelo de memória, todos os possíveis interleavings de threads, e aliasing de ponteiros com precisão. Nenhuma ferramenta faz isso na escala do Facebook em tempo razoável.

Ao escolher a insoundness, RacerD aceita falsos negativos. Algumas corridas reais escapam. A aposta era que encontrar 90% das corridas automaticamente, toda noite, em cada diff, é mais valioso que encontrar 100% das corridas nunca.

A taxa de falsos positivos tinha que permanecer baixa. Uma ferramenta que chora lobo a cada terceiro método é desativada. RacerD manteve falsos positivos abaixo de 10% sendo conservador sobre o que reporta. Ele não sinaliza corridas envolvendo tipos imutáveis thread-safe. Ele entende que campos final são seguros após a construção. Ele modela padrões de sincronização comuns.

Como o Facebook o implantou

RacerD rodava em cada diff de código antes dele aterrissar. Era parte do Infer, seu framework de análise estática open source. Os engenheiros viam relatórios de corridas no Phabricator (sua ferramenta de revisão de código) ao lado dos resultados dos testes unitários.

O fluxo de trabalho parecia assim:

  1. O engenheiro envia um diff que adiciona um acesso de thread de fundo a estado compartilhado.
  2. Infer executa o RacerD nos métodos modificados.
  3. Se uma corrida é encontrada, o diff recebe um sinal de bloqueio. O engenheiro deve corrigi-la ou suprimi-la explicitamente.

Isso deslocou o fardo para a esquerda. race conditions eram capturadas durante a revisão, não em crashes de produção.

O Facebook liberou o Infer como open source, incluindo o RacerD, em 2015. Você pode executá-lo hoje em Java, C, C++ e Objective-C.

Executando Infer no seu próprio código Android

Se você quer experimentar isso, Infer é um binário único. Instale-o via Homebrew ou baixe um release:

brew install infer

Execute-o no seu projeto Gradle:

infer run -- ./gradlew build

Infer compilará seu projeto e analisará o bytecode. Para detecção de corridas especificamente, adicione anotações de thread ao seu código. Infer inclui anotações em 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 reporta: corrida em mToken
    }
}

O relatório diz o arquivo, a linha e o acesso conflitante. Corrija-o com sincronização, uma referência atômica, ou movendo o estado para um modelo confinado a uma thread.

Onde isso quebra

RacerD não é uma bala de prata. Ele luta com corridas através de aliases não óbvios, corridas em código nativo, e corridas mediadas por frameworks que ele não modela. Se você usa RxJava ou coroutines com complexos saltos de thread, as anotações de thread podem não capturar o contexto de execução real.

Também requer disciplina. Se você mente em suas anotações, a análise mente de volta. Marcar um método @UiThread quando ele é na verdade chamado de uma thread de fundo derrota o propósito.

A lição real

A ideia do Facebook não foi que a interpretação abstrata é mágica. Foi que uma análise ligeiramente errada, executada continuamente a cada mudança, vence uma análise perfeita executada nunca.

Se você está construindo código Android concorrente hoje, você não precisa construir o RacerD você mesmo. Você pode adotar o Infer, ou pode aplicar o mesmo princípio: modele quais threads tocam qual estado, faça-o cumprir com análise estática, e trate a segurança de threads como uma preocupação em tempo de compilação, não de depuração em produção.

Seus usuários não lhe agradecerão pelas corridas que você preveniu. Eles simplesmente não desinstalarão seu aplicativo.