RacerD: Compositional Static Race Detection TEPLOCOM (EN)

1 Introduction

RacerD: Compositional Static Race Detection SAM BLACKSHEAR, Facebook, USA NIKOS GOROGIANNIS, Facebook and Middlesex University London, UK PETER W. O’HEARN, Facebook and University College London, UK ILYA SERGEY , Yale-NUS College and University College London, Singapore and UK Automatic static detection of data races is one of the most basic problems in reasoning about concurrency. We present RacerD—a static program analysis for detecting data races in Java programs which is fast, can scale to large code, and has proven effective in an industrial software engineering scenario.

To our knowledge, RacerD is the first inter-procedural, compositional data race detector which has been empirically shown to have non-trivial precision and impact. Due to its compositionality, it can analyze code changes quickly, and this allows it to perform continuous reasoning about a large, rapidly changing codebase as part of deployment within a continuous integration ecosystem. In contrast to previous static race detectors, its design favors reporting high-confidence bugs over ensuring their absence. RacerD has been in deployment for over a year at Facebook, where it has flagged over 2500 issues that have been fixed by developers before reaching production.

It has been important in enabling the development of new code as well as fixing old code: it helped support the conversion of part of the main Facebook Android app from a single-threaded to a multi-threaded architecture. In this paper we describe RacerD’s design, implementation, deployment and impact. CCS Concepts: Theory of computation Program analysis ; Software and its engineering Concurrent programming structures ; Additional Key Words and Phrases: Concurrency, Static Analysis, Race Freedom ACM Reference Format: Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey. 2018. RacerD: Compositional Static Race Detection. Proc. ACM Program. Lang.

2, OOPSLA, Article 144 (November 2018), 28 pages. https://doi.org/ 10.1145/3276514 1 INTRODUCTION Concurrent programming is hard. It is difficult for humans to think about the vast number of potential interactions between processes, and this makes concurrent programs hard to get right in the first place. Further, concurrency errors are difficult to debug and even reproduce after they have been observed, making them time-consuming to fix. Because of both its difficulty and importance, formal reasoning about concurrency has been studied for over 40 years and has seen many research advances.

However, despite numerous interesting ideas not much of the work has made it out of the research setting and into deployment, where it can help programmers in their daily jobs. At Facebook, we are working on techniques for automated reasoning about concurrency. RacerD, our new race detector, searches for data races—unsynchronized memory accesses, where one is a Work done while employed as a part-time contractor at Facebook. Authors’ addresses: Sam Blackshear, Facebook, USA, shb@fb.com; Nikos Gorogiannis, Facebook and Middlesex University London, UK, nikosgorogiannis@fb.com; Peter W.

O’Hearn, Facebook and University College London, UK, peteroh@fb.com; Ilya Sergey, Yale-NUS College and University College London, Singapore and UK, i.sergey@ucl.ac.uk. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). © 2018 Copyright held by the owner/author(s). 2475-1421/2018/11-ART144 https://doi.org/10.1145/3276514 Proc. ACM Program. Lang., Vol.

2, No. OOPSLA, Article 144. Publication date: November 2018. 144

Стр. 1

1 Introduction

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.

Стр. 2

2 A Beginning Example

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.

Стр. 3

2 A Beginning Example

144:4 Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey If we run RacerD on this code it doesn’t find a problem. The unprotected read at line 10 and the protected write at line 6 do not race with one another because they are known to be on the same thread. This code illustrates just one way that developers try to write thread safe code while avoiding synchronization in places for performance reasons. RacerD works by first computing a summary for each method in a class, which records potential accesses together with information such as whether they are protected by a lock or confined to a thread.

While analysing a method, RacerD might consult summaries for methods it calls if they are present in cache, or make a recursive call to the analyzer to provide such summaries on demand if they are not present. The creation of summaries is done in a context-independent way; a procedure body will not need to be processed multiple times taking into account different call sites. Next, RacerD looks through all the summaries for the class in question checking for potential conflicts. In this example, the summaries record an approximation of the information that the accesses to mCount are both protected by being on the same thread: protectedWriteOnMainThread_OK() Thread: true, Lock:

true, Write to this.RaceWithMainThread.mCount at line 6 unprotectedReadOnMainThread_OK() Thread: true, Lock: false, Read of this.RaceWithMainThread.mCount at line 10 protectedReadOffMainThread_OK() Thread: false, Lock: true, Read of this.RaceWithMainThread.mCount at line 13 Thus, RacerD’s summary processing phase concludes that a race is not possible because the threading information for the accesses indicates mutual exclusion. On the other hand, if we include additional methods that do conflict, then RacerD will report potential races, as in Figure 1 , bottom. The summaries for the additional methods record information about the accesses as follows: protectedWriteOffMainThread_BAD() Thread:

false, Lock: true, Write to this.RaceWithMainThread.mCount at line 17 unprotectedReadOffMainThread_BAD() Thread: false, Lock: false, Read of this.RaceWithMainThread.mCount at line 20 When we look at the summary for protectedWriteOffMainThread_BAD we can see the potential conflict with the unprotected read on the main thread. One is protected by a lock, and the other is protected by knowledge that it is on the main thread, but these are not sufficient to provide mutual exclusion: RacerD reports a race between this access and the one at line 8. Similarly, the access at line 20 in unprotectedReadOffMainThread_BAD is protected by neither a lock nor a thread.

RacerD will report it as racing with both the access at line 6 and the access at line 17. In general, RacerD accepts a Java program as input and checks each of its classes for data races between the non- private methods of the class when run in parallel with one another. It looks for “deep” races arising from arbitrarily long chains of method calls into other classes. 4 RacerD checks classes marked @ThreadSafe in the program, as well as classes marked with other annotations that we treat as aliases of @ThreadSafe (this aliasing facility was used in the application to News Feed multithreading).

In addition, RacerD performs concurrent context inference to trigger race checking on classes that use locks or otherwise indicate that they are intended to be used concurrently, even when they are not annotated as @ThreadSafe . We have also developed a system of annotations in collaboration with Android engineers for documenting certain assumptions, such as that a method behaves functionally or that a method is only used on the UI thread. These annotations help the user experience, but are not necessary for getting started. RacerD can be run on any Java program without adding annotations.

4 According to a recent survey, 65% of the races found by Infer required inspecting multiple procedures and/or multiple files: https://code.facebook.com/posts/1537144479682247/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer/ Proc. ACM Program. Lang., Vol. 2, No. OOPSLA, Article 144. Publication date: November 2018.

Стр. 4