У приложения Facebook для Android была проблема с производительностью. UI-thread тонул в работе, но перенос кода в фоновые потоки означал race conditions. Краши в production. Разгневанные пользователи.

Они не решили это лучшим code review или большим количеством тестов. Они построили статический анализатор, RacerD, который использует abstract interpretation, чтобы доказать, могут ли два потока одновременно коснуться одного и того же mutable state. Он проверял миллионы строк Java. Находил тысячи реальных race conditions до того, как они попадали в релиз. И делал это, намеренно ошибаясь в некоторых вещах.

Race conditions — это проблема мощности

Главный поток Android обрабатывает отрисовку, ввод и каждую мутацию View. Слишком много работы там — и приложение начинает пропускать кадры. Исправление кажется очевидным: перенести работу в AsyncTask, HandlerThread или coroutines.

Проблема в том, что UI toolkit Android не является thread-safe. Мутация TextView из фонового потока бросает исключение. Но настоящие убийцы — это тихие race conditions. Два потока читают и пишут shared model state. Interleaving, который взрывается, происходит только на устройстве конкретного пользователя, во вторник, при медленной сети.

Инструменты динамического обнаружения могут ловить race conditions, но только на путях выполнения, которые вы действительно достигаете при тестировании. Кодовая база Facebook была слишком велика, а пространство состояний слишком огромно. Им нужно было знать о race conditions без запуска кода.

Abstract interpretation, агрессивно упрощённая

RacerD построен на abstract interpretation, технике статического анализа программ. Вместо отслеживания точных состояний программы (невозможно для больших codebases) строится более простой abstract domain, и доказываются свойства о нём.

Классический пример — interval analysis. Вы не отслеживаете точное значение x. Вы отслеживаете, положительно ли оно, отрицательно или ноль. Анализ приближённый, но масштабируется.

RacerD применяет эту идею к concurrency. Он отслеживает три вещи за каждым доступом к памяти:

  1. Какой поток выполняет доступ (UI-поток, фоновый поток или неизвестно)
  2. Какой lock, если есть, его защищает
  3. Путь доступа (например, this.mUser.name)

Если два доступа к одному и тому же пути могут произойти на разных потоках, и хотя бы один — запись, и ни один не защищён общим lock, RacerD сообщает о race.

Это звучит так, будто должно быть неподъёмно для многомиллионного приложения. Так бы и было, если бы они пытались моделировать всё точно.

Facebook сделал RacerD намеренно unsound. Он игнорирует Java generics, reflection, виртуальный dispatch в некоторых случаях, и сложности aliasing, которые сделали бы анализ кубичным или хуже. Математика жестока, поэтому они схитрили. Результат: линейная временная сложность на метод, и способность анализировать приложение Facebook менее чем за час.

Владение потоками и контракт @ThreadSafe

Анализ работает, аннотируя методы ограничениями потоков. Рассмотрим этот фрагмент:

@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 видит getUser и setUser, аннотированные @AnyThread. Он отмечает, что mCurrentUser доступен под mLock в обоих случаях. Race не сообщается.

Теперь уберите блоки synchronized:

@AnyThread
public User getUser() {
    return mCurrentUser;  // несинхронизированное чтение
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // несинхронизированная запись
}

RacerD помечает race на mCurrentUser. Два метода @AnyThread обращаются к одному и тому же полю. Один пишет. Нет общего lock. Это точный, пригодный к действию отчёт.

Аннотации управляют анализом. @UiThread означает, что метод выполняется только в главном потоке. @WorkerThread означает фоновый поток. Если метод @WorkerThread и метод @UiThread оба касаются this.mData без синхронизации, это race только если один из них пишет. RacerD знает это, потому что отслеживает чтение против записи.

Компромисс: unsoundness в обмен на adoption

RacerD не доказывает отсутствие race conditions. Он доказывает наличие вероятных race conditions. Это различие важно.

Sound analyzer гарантировал бы, что если race не сообщается, то race не существует. Достижение soundness для concurrent Java требует моделирования memory model, всех возможных interleavings потоков и точного aliasing указателей. Ни один инструмент не делает это в масштабах Facebook за разумное время.

Выбирая unsoundness, RacerD принимает false negatives. Некоторые реальные race conditions проскальзывают. Ставка была на то, что нахождение 90% race conditions автоматически, каждую ночь, на каждом diff, ценнее, чем нахождение 100% race conditions никогда.

Уровень false positives должен был оставаться низким. Инструмент, который кричит волк на каждом третьем методе, отключается. RacerD удерживал false positives ниже 10%, будучи консервативным в том, что он сообщает. Он не помечает race conditions, связанные с thread-safe immutable типами. Он понимает, что final поля безопасны после конструкции. Он моделирует общие паттерны синхронизации.

Как Facebook развёртывал это

RacerD запускался на каждом code diff до его попадания в основную ветку. Он был частью Infer, их open source framework для статического анализа. Инженеры видели отчёты о race conditions в Phabricator (их инструменте code review) наряду с результатами unit tests.

Рабочий процесс выглядел так:

  1. Инженер отправляет diff, добавляющий доступ фонового потока к shared state.
  2. Infer запускает RacerD на изменённых методах.
  3. Если найден race, diff получает блокирующий сигнал. Инженер должен исправить его или явно подавить.

Это сдвинуло бремя влево. Race conditions ловились во время ревью, а не в production crashes.

Facebook open-sourced Infer, включая RacerD, в 2015 году. Вы можете запустить его сегодня на Java, C, C++ и Objective-C.

Запуск Infer на собственном Android-коде

Если вы хотите попробовать это, Infer — один бинарный файл. Установите его через Homebrew или скачайте release:

brew install infer

Запустите на вашем Gradle-проекте:

infer run -- ./gradlew build

Infer скомпилирует ваш проект и проанализирует bytecode. Для обнаружения race conditions специально добавьте thread annotations в ваш код. Infer поставляет аннотации в 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 сообщает: race на mToken
    }
}

Отчёт сообщает файл, строку и конфликтующий доступ. Исправьте это синхронизацией, atomic reference или перемещением состояния в thread-confined модель.

Где это ломается

RacerD — не серебряная пуля. Он испытывает трудности с race conditions через неочевидные aliases, race conditions в нативном коде и race conditions, опосредованные фреймворками, которые он не моделирует. Если вы используете RxJava или coroutines со сложными перепрыгиваниями потоков, thread annotations могут не захватить фактический контекст выполнения.

Это также требует дисциплины. Если вы лжёте в своих аннотациях, анализ лжёт в ответ. Пометка метода @UiThread, когда он фактически вызывается из фонового потока, сводит на нет цель.

Настоящий урок

Инсайт Facebook состоял не в том, что abstract interpretation — это магия. Он состоял в том, что слегка неправильный анализ, запускаемый непрерывно при каждом изменении, превосходит идеальный анализ, который никогда не запускается.

Если вы сегодня строите concurrent Android-код, вам не нужно строить RacerD самостоятельно. Вы можете внедрить Infer или применить тот же принцип: моделируйте, какие потоки касаются какого состояния, обеспечивайте это статическим анализом и рассматривайте thread safety как проблему времени компиляции, а не отладки в production.

Ваши пользователи не поблагодарят вас за предотвращённые race conditions. Они просто не удалят ваше приложение.