RacerD: Compositional Static Race Detection 144:3 1 @ThreadSafe 2 class RaceWithMainThread { 3 int mCount; 4 void protectedWriteOnMainThread_OK() { 5 OurThreadUtils.assertMainThread(); 6 synchronized ( this ) { mCount = 1; } 7 } 8 int unprotectedReadOnMainThread_OK() { 9 OurThreadUtils.assertMainThread(); 10 return mCount; 11 } 12 synchronized int protectedReadOffMainThread_OK() { 13 return mCount; 14 } 15 synchronized void 16 protectedWriteOffMainThread_BAD() { 17 mCount = 2; 18 } 19 int unprotectedReadOffMainThread_BAD() { 20 return mCount; 21 } Fig. 1. Top: simple example capturing a common safety pattern used in Android apps:
threading information is used to limit the amount of synchronization required. As a comment from the original code explains: mCount is written to only by the main thread with the lock held, read from the main thread with no lock held, or read from any other thread with the lock held.” Bottom: unsafe additions to RaceWithMainThread.java . From the point of view of the analysis designer, the distinguishing technical property of RacerD is that it is compositional : the analysis result of a composite program can be obtained from the results of its parts. This means, in particular, that an “analysis result of a part” is meaningful independently of the context (composite program) it is placed in.
Compositionality opens the way to analyzing a code fragment ( e.g. , the code change under review) without knowing the context that it will run in. This is useful for checking a piece of code for thread-safety issues before placing it in a concurrent context. It is also fairly straightforward to parallelize a compositional analysis, helping it scale to big code, which is important given the size of codebases at Facebook. Our analysis differs from much previous static analysis work in that we are not aiming to prove absence of races, but rather to report a set of high-confidence races; we are favoring reduction of false positives over false negatives.
This presents different challenges, but also allows us to make tradeoffs ( cf. Section 8 ) that would not be justified if the aim were to show absence of races. In the remainder of the paper we describe RacerD’s design, implementation, deployment and evaluation. 2 We present a number of design decisions which can be seen alternately as limitations or, more positively, as engineering compromises that unlock the potential for impact. The primary evidence for our claim of effectiveness comes from RacerD’s deployment at Facebook. As far as we are aware, no previous static race detector has demonstrated comparable impact as part of the software development process for major industrial products.
We additionally present case studies comparing RacerD to other open-source Java race detectors. Note that we are using the terminology ‘race detector’ to refer to a tool which accepts a piece of code and then searches for races within that, without the human first adding annotations describing (say) the relationships between locks and fields. The latter form of tool, though still useful, is less automatic and functions like a type checker. We will describe how RacerD fits into the broader context of race detectors and other concurrency checking tools in Section 7 .
2 A BEGINNING EXAMPLE To help ground the discussion that follows we begin with a simple example in Figure 1 (top) that illustrates some of RacerD’s ideas. The example is motivated by a coding pattern used in Components*.java classes in the Litho codebase to avoid excess synchronization. 3 2 A tutorial on RacerD is available at http://fbinfer.com/docs/racerd.html . 3 https://github.com/facebook/litho Proc. ACM Program. Lang., Vol. 2, No. OOPSLA, Article 144. Publication date: November 2018.