144:2 Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey write—in Java programs. Races are one of the most basic forms of concurrency errors, and removing them can help simplify the mental task of understanding a concurrent program. RacerD is a static analysis: it employs formal symbolic reasoning to cover many paths through a program without running it. It has been in production at Facebook for over a year, during which time over 2500 concurrency issues it has flagged have been fixed by engineers before reaching production.
Also, even though it is possible to generate artificial false negatives (data races that the analysis does not flag), only three have been reported from production during the past year, and these were due to (since corrected) implementation errors on our part. Even more significantly, RacerD has been used to support the conversion of the layout portion of the News Feed in Facebook’s main Android app from a single-threaded to multi-threaded architecture. One of the Facebook Android engineers, Benjamin Jaeger, stated the impact as follows: Without Infer, multithreading in News Feed would not have been tenable. 1 This conversion also had a positive effect on the performance of the Android app.
Thus, not only is our static analysis used to find and fix problems, it is enabling the new development of important industrial code. (Note that the quote is not saying that Infer/RacerD is the only tool that might ever exist that could have enabled multi-threading in News Feed, but rather that they would not have been able to tackle the project without it or some other similarly effective data race detector. That practicing engineers regard a static analysis as enabling code they write can be taken to be a positive for static race detection in general, not only RacerD.) From the point of view of its users, RacerD has four important features:
(i) speed, reporting issues quickly; (ii) scale, ability to run on large codebases; (iii) low friction, can be run without huge startup time for developers in terms of annotating code; (iv) effective signal, its reports are seen as valuable and not ignored by developers. Speed and scale together are necessary to cope with the kind of high momentum software engi- neering practiced at Facebook, where a codebase in the millions of lines of code undergoes frequent modification by thousands of programmers. RacerD performs continuous reasoning ( O’Hearn 2018a ) by analyzing these code changes (known as diffs ) as they are submitted to the internal code review process.
With each diff, an instance of RacerD is spun up in Facebook’s continuous integration system, so it acts as a bot participating in code review by automatically commenting on the code. Low friction allows RacerD to achieve incremental impact on existing codebases, without starting from scratch. In particular, RacerD does not rely on annotations for saying which pieces of memory are guarded by what locks. These kinds of annotations, which are used in @GuardedBy type systems for Java ( Ernst et al . 2016 ; Goetz et al . 2006 ) and in Rust ( e.g.
, the Mutex type), are useful when present, but requiring them to get started causes considerable friction; enough that relying on them in the conversion of Facebook Android News Feed would have been a show stopper. Effective signal is related to the concept of false positive rate , but is not the same thing. It is entirely possible to have an analysis with a low false positive rate, but where developers ignore the reports; this phenomenon has been observed multiple times in industrial program analysis ( Ayewah et al . 2008 ; Bessey et al . 2010 ; Sadowski et al . 2018 ).
Effectiveness of signal is partly dependent on false positive rate, but also on speed of reporting and on the deployment model. Our continuous reasoning takes place as part of code review, in the developers’ workflow, when they are thinking about a code change; it avoids the mental effort of human context switch which comes with, for example, batch deployment. 1 RacerD is part of the Infer analysis platform. This quote was from https://code.facebook.com/posts/1985913448333055/ multithreaded-rendering-on-android-with-litho-and-infer/ Proc. ACM Program. Lang., Vol. 2, No. OOPSLA, Article 144. Publication date: November 2018.