FacebookのAndroidアプリにはパフォーマンス上の問題があった。UIスレッドが仕事に溺れていたが、コードをバックグラウンドスレッドに移すと競合状態が生じた。プロダクションでのクラッシュ。怒ったユーザー。

彼らはより良いコードレビューやより多くのテストでこれを解決しなかった。彼らはRacerDという静的解析ツールを構築した。これは抽象解釈を用いて、2つのスレッドが同時に同じ可変状態に触れる可能性があるかを証明する。数百万行のJavaを検証し、数千の実際の競合を出荷前に発見した。そして、それは意図的にいくつかの点で間違うことで成し遂げられた。

競合状態は濃度の問題である

Androidのメインスレッドは描画、入力、およびすべてのViewの変更を処理する。そこで処理しすぎると、アプリはフレームを落とす。修正は明らかだように思える：作業をAsyncTask、HandlerThread、またはコルーチンにオフロードする。

問題は、AndroidのUIツールキットがスレッドセーフでないことだ。バックグラウンドスレッドからTextViewを変更すると例外が投げられる。しかし、本当の殺し屋は静かな競合状態だ。2つのスレッドが共有モデル状態を読み書きする。爆発するインターリービングは、特定のユーザーのデバイス上で、火曜日に、遅いネットワーク環境でのみ発生する。

動的検出ツールは競合を捉えることができるが、テスト中に実際に到達した実行パス上でのみだ。Facebookのコードベースは大きすぎ、状態空間も広すぎた。彼らはコードを実行せずに競合を知る必要があった。

積極的に単純化された抽象解釈

RacerDは、静的プログラム解析技術である抽象解釈を基盤としている。大規模なコードベースでは不可能な正確なプログラム状態の追跡の代わりに、より単純な抽象ドメインを構築し、その性質を証明する。

古典的な例は区間解析だ。xの正確な値を追跡しない。それが正数、負数、またはゼロかを追跡する。解析は近似的だが、スケールする。

RacerDはこのアイデアを並行性に適用する。メモリアクセスごとに3つのことを追跡する：

  1. どのスレッドがアクセスを実行するか（UIスレッド、バックグラウンドスレッド、または不明）
  2. どのロックが、もしあれば、それを保護するか
  3. アクセスパス（例：this.mUser.name）

同じパスへの2つのアクセスが異なるスレッド上で発生しうる場合、かつ少なくとも一方が書き込みであり、かつ共通のロックによって保護されていない場合、RacerDは競合を報告する。

これは数百万行規模のアプリでは扱いきれないように聞こえる。すべてを正確にモデル化しようとすれば、確かにそうなる。

FacebookはRacerDを意図的にunsound（不完全）にした。Javaジェネリクス、リフレクション、仮想ディスパッチ（一部のケース）、およびエイリアシングの複雑性を無視する。これらを考慮すると解析の計算量は3次以上になってしまう。数学的に厳密に行くのは厳しいので、彼らはカンニングをした。結果：メソッドあたりの線形時間計算量、そしてFacebookのアプリを1時間未満で解析する能力だ。

スレッド所有権と@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の下でアクセスされることに注目する。競合は報告されない。

次にsynchronizedブロックを削除する：

@AnyThread
public User getUser() {
    return mCurrentUser;  // 非同期化された読み取り
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // 非同期化された書き込み
}

RacerDはmCurrentUserでの競合をフラグ付けする。2つの@AnyThreadメソッドが同じフィールドにアクセスする。一方が書き込む。共通のロックがない。これは正確で実行可能な報告だ。

注釈が解析を推進する。@UiThreadはそのメソッドがメインスレッド上でのみ実行されることを意味する。@WorkerThreadはバックグラウンドを意味する。@WorkerThreadメソッドと@UiThreadメソッドの両方が同期なしにthis.mDataに触れる場合、それは一方が書き込む場合にのみ競合だ。RacerDは読み取り対書き込みを追跡するのでこれを知っている。

トレードオフ：導入との引き換えのunsoundness

RacerDは競合の不在を証明しない。起こりそうな競合の存在を証明する。この区別は重要だ。

健全な（sound）解析器は、競合が報告されなければ競合が存在しないことを保証するだろう。並行Javaで健全性を達成するには、メモリモデル、すべての可能なスレッドインターリービング、およびポインタエイリアシングを正確にモデル化する必要がある。Facebookの規模で合理的な時間内にこれを行うツールは存在しない。

unsoundnessを選ぶことで、RacerDは偽陰性を受け入れる。いくつかの実際の競合は見逃される。賭けは、毎晩、すべてのdiffで、自動的に90%の競合を発見することが、100%の競合を決して発見しないことよりも価値があるというものだった。

偽陽性率は低く保たれなければならなかった。3つのメソッドごとに狼少年を叫ぶツールは無効化される。RacerDは報告内容について保守的であることで偽陽性を10%未満に保った。スレッドセーフな不変型を含む競合をフラグ付けしない。finalフィールドは構築後に安全であることを理解する。一般的な同期パターンをモデル化する。

Facebookがどのように展開したか

RacerDは、コードが展開される前のすべてのコード差分上で実行された。これはInfer（彼らのオープンソースの静的解析フレームワーク）の一部だった。エンジニアはユニットテスト結果と並んで、コードレビューツールPhabricatorで競合レポートを見た。

ワークフローは次のようだった：

  1. エンジニアが共有状態へのバックグラウンドスレッドアクセスを追加するdiffを提出する。
  2. Inferが変更されたメソッドでRacerDを実行する。
  3. 競合が見つかれば、diffはブロッキングシグナルを受ける。エンジニアはそれを修正するか、明示的に抑制しなければならない。

これにより負担が左にシフトされた。競合状態は本番のクラッシュではなく、レビュー中に捉えられた。

Facebookは2015年にRacerDを含むInferをオープンソース化した。今日、Java、C、C++、およびObjective-C上で実行できる。

独自のAndroidコードでInferを実行する

これを試したい場合、Inferは単一のバイナリだ。Homebrew経由でインストールするか、リリースをダウンロードする：

brew install infer

Gradleプロジェクトで実行する：

infer run -- ./gradlew build

Inferはプロジェクトをコンパイルしてバイトコードを解析する。競合検出のために、コードにスレッド注釈を追加する。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は報告: mTokenでの競合
    }
}

レポートはファイル、行、および競合するアクセスを伝える。同期、アトミック参照、またはスレッド閉鎖モデルへの状態移動で修正する。

どこで機能しないか

RacerDは万能薬ではない。非自明なエイリアスを介した競合、ネイティブコード内の競合、およびモデル化していないフレームワークを介した競合には苦労する。RxJavaや複雑なスレッドホッピングを伴うコルーチンを使用する場合、スレッド注釈は実際の実行コンテキストを捉えない可能性がある。

また、規律も必要だ。注釈で嘘をつくと、解析も嘘をつく。メソッドが実際にはバックグラウンドスレッドから呼ばれているのに@UiThreadとマークすると、目的を損なう。

本当の教訓

Facebookの洞察は、抽象解釈が魔法であるということではなかった。常に少し間違った解析が、決して実行されない完璧な解析に勝るということだった。

今日、並行Androidコードを構築しているなら、RacerDを自分で構築する必要はない。Inferを採用するか、同じ原則を適用できる：どのスレッドがどの状態に触れるかをモデル化し、静的解析でそれを強制し、スレッド安全性をプロダクションデバッグではなくコンパイル時の懸念事項として扱う。

ユーザーは防止した競合には感謝しない。単にアプリをアンインストールしないだけだ。