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，或者你可以应用同样的原则：建模哪些线程接触哪些状态，用静态分析强制执行，并将线程安全性视为编译时问题，而不是投产调试问题。

你的用户不会感谢你阻止的竞态。他们只是不会卸载你的应用。