La aplicación de Android de Facebook tenía un problema de rendimiento. El hilo de la interfaz se estaba ahogando en trabajo, pero mover código a hilos de fondo significaba condiciones de carrera. Crashes en producción. Usuarios enfadados.

No resolvieron esto con mejores revisiones de código o más pruebas. Construyeron un analizador estático, RacerD, que usa interpretación abstracta para probar si dos hilos pueden tocar el mismo estado mutable al mismo tiempo. Revisó millones de líneas de Java. Encontró miles de carreras reales antes de enviarlas. Y lo hizo siendo deliberadamente incorrecto en algunas cosas.

Las condiciones de carrera son un problema de cardinalidad

El hilo principal de Android maneja el dibujado, la entrada y cada mutación de View. Hacer demasiado allí y tu aplicación pierde frames. La solución parece obvia: descargar trabajo a AsyncTask, HandlerThread o coroutines.

El problema es que el kit de herramientas de interfaz de Android no es seguro para hilos. Mutar un TextView desde un hilo de fondo lanza una excepción. Pero los verdaderos asesinos son las carreras silenciosas. Dos hilos leen y escriben estado compartido del modelo. El interleaving que explota solo ocurre en el dispositivo de un usuario específico, un martes, con red lenta.

Las herramientas de detección dinámica pueden atrapar carreras, pero solo en caminos de ejecución que realmente alcanzas en las pruebas. La codebase de Facebook era demasiado grande y el espacio de estados demasiado amplio. Necesitaban saber sobre carreras sin ejecutar el código.

Interpretación abstracta, agresivamente simplificada

RacerD se basa en la interpretación abstracta, una técnica de análisis estático de programas. En lugar de rastrear estados exactos del programa (imposible para grandes codebases), construyes un dominio abstracto más simple y pruebas propiedades sobre él.

El ejemplo clásico es el análisis de intervalos. No rastreas el valor exacto de x. Rastreas si es positivo, negativo o cero. El análisis es aproximado, pero escala.

RacerD aplica esta idea a la concurrencia. Rastrea tres cosas por acceso a memoria:

  1. Qué hilo realiza el acceso (hilo de interfaz, hilo de fondo o desconocido)
  2. Qué lock, si lo hay, lo protege
  3. El camino de acceso (por ejemplo, this.mUser.name)

Si dos accesos al mismo camino pueden ocurrir en hilos diferentes, y al menos uno es una escritura, y ninguno está protegido por un lock común, RacerD reporta una carrera.

Esto suena como si debería ser intratable para una aplicación de millones de líneas. Lo sería, si intentaran modelar todo con precisión.

Facebook hizo que RacerD fuera intencionalmente unsound. Ignora los genéricos de Java, la reflexión, el dispatch virtual en algunos casos, y las complejidades de aliasing que harían que el análisis fuera cúbico o peor. Las matemáticas son brutales, así que hicieron trampa. El resultado: complejidad de tiempo lineal por método, y la capacidad de analizar la aplicación de Facebook en menos de una hora.

Propiedad de hilos y el contrato @ThreadSafe

El análisis funciona anotando métodos con restricciones de hilo. Considera este fragmento:

@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 ve getUser y setUser anotados con @AnyThread. Observa que mCurrentUser se accede bajo mLock en ambos casos. No se reporta ninguna carrera.

Ahora elimina los bloques synchronized:

@AnyThread
public User getUser() {
    return mCurrentUser;  // lectura no sincronizada
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // escritura no sincronizada
}

RacerD marca una carrera en mCurrentUser. Dos métodos @AnyThread acceden al mismo campo. Uno escribe. No hay lock común. Este es un reporte preciso y accionable.

Las anotaciones impulsan el análisis. @UiThread significa que el método solo se ejecuta en el hilo principal. @WorkerThread significa hilo de fondo. Si un método @WorkerThread y un método @UiThread tocan this.mData sin sincronización, eso solo es una carrera si uno de ellos escribe. RacerD sabe esto porque rastrea lectura versus escritura.

El trade-off: unsoundness a cambio de adopción

RacerD no prueba la ausencia de carreras. Prueba la presencia de carreras probables. Esta distinción importa.

Un analizador sound garantizaría que si no se reporta una carrera, no existe una carrera. Lograr soundness para Java concurrente requiere modelar el modelo de memoria, todos los posibles interleavings de hilos y el aliasing de punteros con precisión. Ninguna herramienta hace esto a la escala de Facebook en tiempo razonable.

Al elegir la unsoundness, RacerD acepta falsos negativos. Algunas carreras reales se escapan. La apuesta fue que encontrar el 90% de las carreras automáticamente, cada noche, en cada diff, es más valioso que encontrar el 100% de las carreras nunca.

La tasa de falsos positivos tenía que mantenerse baja. Una herramienta que grita lobo en cada tercer método se desactiva. RacerD mantuvo los falsos positivos por debajo del 10% siendo conservador sobre lo que reporta. No marca carreras que involucren tipos inmutables seguros para hilos. Entiende que los campos final son seguros después de la construcción. Modela patrones de sincronización comunes.

Cómo Facebook lo desplegó

RacerD se ejecutaba en cada diff de código antes de que aterrizara. Era parte de Infer, su framework de análisis estático de código abierto. Los ingenieros veían los reportes de carreras en Phabricator (su herramienta de revisión de código) junto con los resultados de las unit tests.

El flujo de trabajo se veía así:

  1. El ingeniero envía un diff que agrega un acceso de hilo de fondo a estado compartido.
  2. Infer ejecuta RacerD en los métodos modificados.
  3. Si se encuentra una carrera, el diff recibe una señal de bloqueo. El ingeniero debe corregirla o suprimirla explícitamente.

Esto desplazó la carga hacia la izquierda. Las condiciones de carrera se capturaban durante la revisión, no en crashes de producción.

Facebook liberó Infer como open source, incluyendo RacerD, en 2015. Puedes ejecutarlo hoy en Java, C, C++ y Objective-C.

Ejecutando Infer en tu propio código de Android

Si quieres probar esto, Infer es un solo binario. Instálalo vía Homebrew o descarga un release:

brew install infer

Ejecútalo en tu proyecto Gradle:

infer run -- ./gradlew build

Infer compilará tu proyecto y analizará el bytecode. Para la detección de carreras específicamente, agrega anotaciones de hilo a tu código. Infer incluye anotaciones en 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: carrera en mToken
    }
}

El reporte te dice el archivo, la línea y el acceso conflictivo. Arréglalo con sincronización, una referencia atómica, o moviendo el estado a un modelo confinado a un hilo.

Donde esto se desmorona

RacerD no es una bala de plata. Tiene dificultades con carreras a través de aliases no obvios, carreras en código nativo, y carreras mediadas por frameworks que no modela. Si usas RxJava o coroutines con complejos saltos de hilo, las anotaciones de hilo pueden no capturar el contexto de ejecución real.

También requiere disciplina. Si mientes en tus anotaciones, el análisis miente de vuelta. Marcar un método como @UiThread cuando en realidad se llama desde un hilo de fondo frustra el propósito.

La lección real

La idea de Facebook no fue que la interpretación abstracta es mágica. Fue que un análisis ligeramente incorrecto, ejecutado continuamente en cada cambio, supera a un análisis perfecto que nunca se ejecuta.

Si estás construyendo código concurrente para Android hoy, no necesitas construir RacerD tú mismo. Puedes adoptar Infer, o puedes aplicar el mismo principio: modela qué hilos tocan qué estado, hazlo cumplir con análisis estático, y trata la seguridad de hilos como una preocupación en tiempo de compilación, no de depuración en producción.

Tus usuarios no te agradecerán por las carreras que preveniste. Simplemente no desinstalarán tu aplicación.