research-article

Open access

A true positives theorem for a static race detector

Authors:

Nikos Gorogiannis,

Peter W. O'Hearn,

Ilya SergeyAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 57, Pages 1 - 29

https://doi.org/10.1145/3290370

Published: 02 January 2019 Publication History

Abstract

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.

Supplementary Material

WEBM File (a57-gorogiannis.webm)

Download
105.87 MB

References

[1]

Robert Atkey and Donald Sannella. 2015. ThreadSafe: Static Analysis for Java Concurrency. ECEASST 72 (2015).

[2]

Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey. 2018. RacerD: compositional static race detection. PACMPL 2, OOPSLA (2018), 144:1–144:28.

Digital Library

[3]

Stephen Brookes. 2007. A semantics for concurrent separation logic. Th. Comp. Sci. 375, 1-3 (2007).

Digital Library

[4]

Cristian Cadar and Koushik Sen. 2013. Symbolic execution for software testing: three decades later. Commun. ACM 56, 2 (2013), 82–90.

Digital Library

[5]

Andy Chou. 2014. From the Trenches: Static Analysis in Industry. (2014). Invited keynote talk at POPL’14. Available at https://popl.mpi-sws.org/2014/andy.pdf .

[6]

Maria Christakis, Peter Müller, and Valentin Wüstholz. 2015. An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer. In VMCAI (LNCS), Vol. 8931. Springer, 336–354.

Digital Library

[7]

David G. Clarke and Sophia Drossopoulou. 2002. Ownership, encapsulation and the disjointness of type and effect. In OOPSLA . ACM, 292–310.

Digital Library

[8]

Patrick Cousot. 1978. Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes . Ph.D. Dissertation. Université Scientifique et Médicale de Grenoble.

[9]

Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL. ACM, 238–252.

Digital Library

[10]

Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. In POPL. ACM Press, 269–282.

Digital Library

[11]

Patrick Cousot and Radhia Cousot. 1992. Abstract Interpretation Frameworks. J. Log. Comput. 2, 4 (1992), 511–547.

[12]

Cormac Flanagan and Stephen N. Freund. 2009. FastTrack: efficient and precise dynamic race detection. In PLDI. ACM, 121–133.

Digital Library

[13]

Cormac Flanagan, Stephen N. Freund, and Jaeheon Yi. 2008. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In PLDI. ACM, 293–303.

Digital Library

[14]

Roberto Giacobazzi, Francesco Logozzo, and Francesco Ranzato. 2015. Analyzing Program Analyses. In POPL. ACM, 261–273.

Digital Library

[15]

Brian Goetz, Tim Peierls, Joshua Bloch, Joseph Bowbeer, David Holmes, and Doug Lea. 2006. Java Concurrency in Practice. Addison-Wesley.

[16]

Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey. 2018. A True Positives Theorem for a Static Race Detector – Extended Version. CoRR 1811.03503 (2018). arXiv: 1811.03503 https://arxiv.org/abs/1811.03503

Digital Library

[17]

Maurice Herlihy and Nir Shavit. 2008. The art of multiprocessor programming. M. Kaufmann.

Digital Library

[18]

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A promising semantics for relaxedmemory concurrency. In POPL. ACM, 175–189.

Digital Library

[19]

Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28, 9 (1979), 690–691.

Digital Library

[20]

Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondrej Lhoták, José Nelson Amaral, Bor-Yuh Evan Chang, Samuel Z. Guyer, Uday P. Khedker, Anders Møller, and Dimitrios Vardoulakis. 2015. In defense of soundiness: a manifesto. Commun. ACM 58, 2 (2015), 44–46.

Digital Library

[21]

William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti. 2017. Verifying dynamic race detection. In CPP. ACM, 151–163.

Digital Library

[22]

Mayur Naik and Alex Aiken. 2007. Conditional must not aliasing for static race detection. In POPL. ACM, 327–338.

Digital Library

[23]

Mayur Naik, Alex Aiken, and John Whaley. 2006. Effective static race detection for Java. In PLDI. ACM, 308–319.

Digital Library

[24]

Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. 2014. Selective context-sensitivity guided by impact pre-analysis. In PLDI. ACM, 475–484.

Digital Library

[25]

Mukund Raghothaman, Sulekha Kulkarni, Kihong Heo, and Mayur Naik. 2018. Interactive Program Reasoning using Bayesian Inference. In PLDI. ACM, 722–735.

Digital Library

[26]

Francesco Ranzato. 2013. Complete Abstractions Everywhere. In VMCAI (LNCS), Vol. 7737. Springer, 15–26.

Digital Library

[27]

Caitlin Sadowski, Jaeheon Yi, Kenneth Knowles, and Cormac Flanagan. 2008. Proving correctness of a dynamic atomicity analysis in Coq. In Workshop on Mechanizing Metatheory.

[28]

Konstantin Serebryany and Timur Iskhodzhanov. 2009. ThreadSanitizer: data race detection in practice. Proceedings of the Workshop on Binary Instrumentation and Applications, 62–71.

Digital Library

[29]

Robert D. Tennent. 1977. Language Design Methods Based on Semantic Principles. Acta Inf. 8 (1977), 97–112.

[30]

Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In POPL. ACM, 343–356.

Digital Library

[31]

James R. Wilcox, Cormac Flanagan, and Stephen N. Freund. 2018. VerifiedFT: a verified, high-performance precise dynamic race detector. ACM, 354–367.

Digital Library

[32]

Hongseok Yang and Peter O’Hearn. 2002. A Semantic Basis for Local Reasoning. In Foundations of Software Science and Computation Structures . Springer Berlin Heidelberg, 402–416.

Digital Library

Cited By

Liew DCogumbreiro TLange J(2024)Sound and Partially-Complete Static Analysis of Data-Races in GPU ProgramsProceedings of the ACM on Programming Languages10.1145/36897978:OOPSLA2(2434-2461)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689797
Dardinier TLi AMüller P(2024)Hypra: A Deductive Program Verifier for Hyper Hoare LogicProceedings of the ACM on Programming Languages10.1145/36897568:OOPSLA2(1279-1308)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689756
Dardinier TMüller P(2024)Hyper Hoare Logic: (Dis-)Proving Program HyperpropertiesProceedings of the ACM on Programming Languages10.1145/36564378:PLDI(1485-1509)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656437
Show More Cited By

Index Terms

A true positives theorem for a static race detector
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Concurrent programming structures
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

RacerD: compositional static race detection

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 ...
Static analysis for concurrent programs with applications to data race detection

We propose a general framework for static analysis of concurrent multi-threaded programs in the presence of various types of synchronization primitives such as locks and pairwise rendezvous. In order to capture interference between threads, we use the ...
An algorithmic mitigation of large spurious interprocedural cycles in static analysis

We present a simple algorithmic extension of the approximate call-strings approach to mitigate substantial performance degradation caused by spurious interprocedural cycles. Spurious interprocedural cycles are, in a realistic setting, the key reasons ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
1,343
Total Downloads

Downloads (Last 12 months)179
Downloads (Last 6 weeks)27

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liew DCogumbreiro TLange J(2024)Sound and Partially-Complete Static Analysis of Data-Races in GPU ProgramsProceedings of the ACM on Programming Languages10.1145/36897978:OOPSLA2(2434-2461)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689797
Dardinier TLi AMüller P(2024)Hypra: A Deductive Program Verifier for Hyper Hoare LogicProceedings of the ACM on Programming Languages10.1145/36897568:OOPSLA2(1279-1308)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689756
Dardinier TMüller P(2024)Hyper Hoare Logic: (Dis-)Proving Program HyperpropertiesProceedings of the ACM on Programming Languages10.1145/36564378:PLDI(1485-1509)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656437
Sun XGupta RBond MLee JPayer H(2024)SSRD: Shapes and Summaries for Race Detection in Concurrent Data StructuresProceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management10.1145/3652024.3665505(68-81)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652024.3665505
Guo YYao PZhang CChristakis MPradel M(2024)Precise Compositional Buffer Overflow Detection via Heap DisjointnessProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652110(63-75)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652110
Lepers BGiet JZwaenepoel WLawall JFedorova ANarayanan DDi Luna GQuerzoni L(2023)OFence: Pairing Barriers to Find Concurrency Bugs in the Linux KernelProceedings of the Eighteenth European Conference on Computer Systems10.1145/3552326.3567504(33-45)Online publication date: 8-May-2023
https://dl.acm.org/doi/10.1145/3552326.3567504
Costea ATiwari AChianasta SR KRoychoudhury ASergey I(2023)Hippodrome: Data Race Repair Using Static Analysis SummariesACM Transactions on Software Engineering and Methodology10.1145/354694232:2(1-33)Online publication date: 31-Mar-2023
https://dl.acm.org/doi/10.1145/3546942
Liew DCogumbreiro TLange J(2022)Provable GPU Data-Races in Static Race DetectionElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.356.4356(36-45)Online publication date: 24-Mar-2022
https://doi.org/10.4204/EPTCS.356.4
Yan PJiang HYu N(2022)On incorrectness logic for Quantum programsProceedings of the ACM on Programming Languages10.1145/35273166:OOPSLA1(1-28)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527316
Gowda SMa YCheli AGwóźzdź MShah VEdelman ARackauckas C(2022)High-performance symbolic-numerics via multiple dispatchACM Communications in Computer Algebra10.1145/3511528.351153555:3(92-96)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3511528.3511535
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents