  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.
