A True Positives Theorem for a Static Race Detector
A True Positives Theorem for a Static Race Detector
复制标题
DOI：
10.1145/3290370
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Sergey, Ilya
中科院分区：
文献类型：
--
作者：
Gorogiannis, Nikos;O'Hearn, Peter W.;Sergey, Ilya
RACERD是一个静态竞赛检测器，在工程实践中被证明是有效的：它已经看到开发人员在投入生产之前修复了数千个数据竞赛，并且支持Facebook的Android应用渲染基础架构从单线程迁移到多线程架构。我们证明了一个真正定理，说明在某些假设下，分析的理想理论版本从不报告假阳性。我们还提供了对该分析的实现的经验评估，与最初的RACERD相比。在第一种情况下，该定理的动机是希望理解从生产中观察到的RACERD为开发人员提供了非常准确的信号，然后该定理指导了进一步的分析器设计决策。从技术上讲，我们的结果可以看作是说分析计算了一个过近似值的过近似值，这与静态分析中更常见的（过近似值或过近似值）情况相反。到目前为止，在实践中有效但不健全的静态分析器通常被认为是临时的；相反，我们建议，在未来，这种类型的定理可能在理解、证明和设计有效的静态分析bug捕获方面普遍有用。
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 ideali ed 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.