用于Android Java的开源死锁检测器

FaceBook的工程师开发了一种新的静态分析器，它可以在不运行代码的情况下捕获Android的Java代码中的死锁。这款分析器与以往研究的不同之处在于它能够用数亿行代码分析代码库中的修改。

FaceBook的工程师已经在Meta的持续集成系统中部署了我们的分析器，在那里它扫描对Android应用程序系列的每一次提交。在过去两年中，开发人员针对死锁报告采取了200多次修复，修复率约为54%。

分析器是开源的：https://github.com/facebook/infer，是Infer静态分析框架的一部分。

工作原理

设计者使用抽象解释技术来设计分析器。对于每个方法，分析器都会计算该方法在锁获取和释放方面的行为总结，以及该方法是在主线程上运行还是在后台线程上运行。这是以一种组合的方式完成的：每个方法最多汇总一次，其汇总用于对其调用方的汇总，以确保可预测的高性能。

摘要的中心部分是该方法的关键对集。一个关键pair (A,B)记录了以下事实：该方法试图获取锁B，此时它已经在集合A中精确地持有锁。通过所有方法计算的这些数据足以让我们回答两个并发方法之间是否可能出现死锁的问题。

为了快速高效，工具避免分析应用程序中的所有源文件。相反，它首先处理修订的修改文件中的所有方法。然后，基于这些数据，它应用一种启发式方法来定位修订之外的方法，这些方法可能会与修订中的一个方法死锁。正是这种启发式方法使我们的分析得以扩展。

在FaceBook的论文中（https://research.facebook.com/file/1020810408701023/A-Compositional-Deadlock-Detector-for-Android-Java.pdf），还证明了他们的分析对于一种只有非确定性控制的抽象编程语言是正确和完整的。换句话说，在这种语言中，可以在没有误报的情况下找到所有死锁。

为什么重要

死锁通常是不可恢复的错误。死锁也是很难诊断的错误，因为线程调度本质上是不确定性的，因此，测试可能需要运行数千或数百万次才能显示问题。

因此，在不运行甚至不构建代码的情况下静态地检测死锁是非常有价值的。FaceBook的方法实现了这一目标，同时也使分析器具有足够的可扩展性，从而可以部署在Meta的大规模代码库上。

原文地址：https://engineering.fb.com/2022/03/08/android/deadlock-detector-for-android-java/