一句话：为 RacerD 静态竞态检测器证明真阳性定理，并给出与原版对比的实现评估。
本文为工业界有效的静态数据竞争检测器 RacerD 提供准确性理论基础。RacerD 已帮助开发者修复数千个数据竞争，并支持 Facebook Android 渲染基础设施从单线程迁移到多线程，但其分析并不健全。作者证明：在特定假设下，一个理想化的理论版本不会报告假阳性，即“真阳性定理”。技术上，该分析计算的是过近似的欠近似，与静态分析常见的欠近似之上的过近似相反。该定理用于解释生产环境中 RacerD 异常准确的信号，并指导了分析器设计。作者还实现该分析并与原版 RacerD 进行实证评估，说明此类定理可用于理解、论证和设计有效的缺陷检测分析。
RacerD is a static race detector that has been proven to be effective in engineering practice: it has seen thousands of data races fixed by developers before reaching production, and has supported the migration of Facebook's Android app rendering infrastructure from a single-threaded to a multi-threaded architecture. We prove a True Positives Theorem stating that, under certain assumptions, an idealized theoretical version of the analysis never reports a false positive. We also provide an empirical evaluation of an implementation of this analysis, versus the original RacerD. The theorem was motivated in the first case by the desire to understand the observation from production that RacerD was providing remarkably accurate signal to developers, and then the theorem guided further analyzer design decisions. Technically, our result can be seen as saying that the analysis computes an under-approximation of an over-approximation, which is the reverse of the more usual (over of under) situation in static analysis. Until now, static analyzers that are effective in practice but unsound have often been regarded as ad hoc; in contrast, we suggest that, in the future, theorems of this variety might be generally useful in understanding, justifying and designing effective static analyses for bug catching.
@article{paperbot675,
title = {A true positives theorem for a static race detector},
author = {Nikos Gorogiannis and Peter W. O'Hearn and Ilya Sergey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290370}
}