Facebook的Android應用程式有一個效能問題。UI執行緒被工作淹沒，但將程式碼移到背景執行緒意味著競態條件。投產當機。憤怒的使用者。

他們沒有透過更好的程式碼審查或更多的測試來解決這個問題。他們建構了一個名為RacerD的靜態分析器，它使用抽象詮釋來證明兩個執行緒是否可以同時接觸同一個可變狀態。它檢查了數百萬行Java程式碼。在發布前發現了數千個真實的競態。而它是透過在某些事情上故意出錯來做到這一點的。

競態條件是一個基數問題

Android的主執行緒處理繪製、輸入和每個View的變更。在那裡做太多工作，你的應用程式就會掉幀。修復方法似乎很明顯：將工作卸載到AsyncTask、HandlerThread或協程。

問題是Android的UI工具包不是執行緒安全的。從背景執行緒變更TextView會拋出例外。但真正致命的是無聲的競態。兩個執行緒讀寫共享模型狀態。導致崩潰的交錯只發生在某個特定使用者的裝置上，某個星期二，網路緩慢時。

動態檢測工具可以捕獲競態，但僅限於你在測試中實際命中的執行路徑。Facebook的程式碼庫太大，狀態空間也太廣。他們需要在不執行程式碼的情況下了解競態。

積極簡化的抽象詮釋

RacerD建立在抽象詮釋之上，這是一種靜態程式分析技術。不是追蹤精確的程式狀態（對於大型程式碼庫來說不可能），而是建構一個更簡單的抽象領域並證明其屬性。

經典例子是區間分析。你不追蹤x的精確值。你追蹤它是正數、負數還是零。分析是近似的，但可擴展。

RacerD將這一想法應用於並行性。它追蹤每次記憶體存取的三件事：

  1. 哪個執行緒執行存取（UI執行緒、背景執行緒或未知）
  2. 如果有的話，哪個鎖保護它
  3. 存取路徑（例如，this.mUser.name）

如果同一條路徑上的兩次存取可能發生在不同執行緒上，且至少有一次是寫入，且兩者都沒有被共同的鎖保護，RacerD就會報告一個競態。

這聽起來對於數百萬行的應用程式來說應該是難以處理的。如果他們試圖精確地建模一切，確實會如此。

Facebook讓RacerD有意地不完整。它忽略Java泛型、反射、某些情況下的虛擬分派，以及會使分析複雜度達到立方或更糟的別名複雜性。數學上太殘酷了，所以他們作弊了。結果：每個方法的線性時間複雜度，以及在一小時內分析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下被存取。沒有報告競態。

現在移除synchronized區塊：

@AnyThread
public User getUser() {
    return mCurrentUser;  // 未同步讀取
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // 未同步寫入
}

RacerD標記mCurrentUser上的競態。兩個@AnyThread方法存取同一個欄位。一個寫入。沒有共同的鎖。這是一個精確、可操作的報告。

註釋驅動分析。@UiThread意味著該方法只在主執行緒上執行。@WorkerThread意味著背景。如果一個@WorkerThread方法和一個@UiThread方法都未同步地接觸this.mData，只有其中一個寫入時才構成競態。RacerD知道這一點，因為它追蹤讀與寫。

權衡：用不完整性換取採用

RacerD不證明競態的不存在。它證明可能存在競態。這個區別很重要。

一個健全的分析器會保證，如果沒有報告競態，就不存在競態。為並行Java實現健全性需要精確地建模記憶體模型、所有可能的執行緒交錯和指標別名。沒有工具能在Facebook的規模上以合理的時間做到這一點。

透過選擇不完整性，RacerD接受偽陰性。一些真實的競態會漏掉。賭注是，每晚自動在每個差異提交上發現90%的競態，比永遠發現100%的競態更有價值。

誤報率必須保持低位。每第三個方法就喊狼來了的工具會被停用。RacerD透過對其報告內容保持保守，將誤報率控制在10%以下。它不標記涉及執行緒安全不可變型別的競態。它理解final欄位在構造後是安全的。它建模常見的同步模式。

Facebook如何部署它

RacerD在每次程式碼差異提交落地前執行。它是Infer（他們的開源靜態分析框架）的一部分。工程師在Phabricator（他們的程式碼審查工具）中 alongside 單元測試結果看到競態報告。

工作流程如下：

  1. 工程師提交一個新增了背景執行緒存取共享狀態的差異。
  2. Infer在修改過的方法上執行RacerD。
  3. 如果發現競態，該差異會收到一個阻塞訊號。工程師必須修復它或明確抑制它。

這將負擔左移。競態條件在審查期間被捕获，而不是在投產當機中。

Facebook在2015年將Infer（包括RacerD）開源。你今天可以在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，或者你可以應用同樣的原則：建模哪些執行緒接觸哪些狀態，用靜態分析強制執行，並將執行緒安全性視為編譯時問題，而不是投產除錯問題。

你的使用者不會感謝你阻止的競態。他們只是不會解除安裝你的應用程式。