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