Article

Optimized run-time race detection and atomicity checking using partial discovered types

Authors:

Amit Sasturkar,

Scott D. StollerAuthors Info & Claims

ASE '05: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering

Pages 233 - 242

https://doi.org/10.1145/1101908.1101944

Published: 07 November 2005 Publication History

Abstract

Concurrent programs are notorious for containing errors that are difficult to reproduce and diagnose. Two common kinds of concurrency errors are data races and atomicity violations (informally, atomicity means that executing methods concurrently is equivalent to executing them serially). Several static and dynamic (run-time) analysis techniques exist to detect potential races and atomicity violations. Run-time checking may miss errors in unexecuted code and incurs significant run-time overhead. On the other hand, run-time checking generally produces fewer false alarms than static analysis; this is a significant practical advantage, since diagnosing all of the warnings from static analysis of large codebases may be prohibitively expensive.This paper explores the use of static analysis to significantly decrease the overhead of run-time checking. Our approach is based on a type system for analyzing data races and atomicity. A type discovery algorithm is used to obtain types for as much of the program as possible (complete type inference for this type system is NP-hard, and parts of the program might be untypable). Warnings from the typechecker are used to identify parts of the program from which run-time checking can safely be omitted. The approach is completely automatic, scalable to very large programs, and significantly reduces the overhead of run-time checking for data races and atomicity violations.

References

[1]

R. Agarwal, A. Sasturkar, and S. D. Stoller. Type discovery for parameterized race-free Java. Technical Report DAR-04-16, Computer Science Department, SUNY at Stony Brook, Sept. 2004. Available at http://www.cs.sunysb.edu/~stoller/type-discovery/.

[2]

R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized run-time race detection and atomicity checking using partial discovered types. Technical Report DAR-05-22, Computer Science Department, SUNY at Stony Brook, June 2005. Available at http://www.cs.sunysb.edu/~ragarwal/.

[3]

R. Agarwal and S. D. Stoller. Type inference for parameterized race-free Java. In Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation, volume 2937 of Lecture Notes in Computer Science, pages 149--160. Springer-Verlag, Jan. 2004.

[4]

C. Boyapati. SafeJava: A Unified Type System for Safe Programming. PhD thesis, Laboratory for Computer Science, MIT, Feb. 2004. Available at http://www.eecs.umich.edu/~bchandra/.

Digital Library

[5]

C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In Proc. 17th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 211--230, Nov. 2002.

Digital Library

[6]

C. Boyapati and M. C. Rinard. A parameterized type system for race-free Java programs. In Proc. 16th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), volume 36(11) of SIGPLAN Notices, pages 56--69. ACM Press, 2001.

Digital Library

[7]

J.-D. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 258--269. ACM Press, 2002.

Digital Library

[8]

D. R. Engler and K. Ashcraft. RacerX : Effective, static detection of race conditions and deadlocks. pages 237--252. ACM Press, Oct. 2003. Available at http://www.stanford.edu/~engler/.

Digital Library

[9]

C. Flanagan and S. Freund. Type-based race detection for Java. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 219--232. ACM Press, 2000.

Digital Library

[10]

C. Flanagan and S. Freund. Type inference against races. In Proc. 11th International Static Analysis Symposium (SAS), volume 3148 of Lecture Notes in Computer Science. Springer-Verlag, Aug. 2004.

[11]

C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In Proc. 31st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Jan. 2004.

Digital Library

[12]

C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 338--349. ACM Press, 2003.

Digital Library

[13]

K. Havelund. Using runtime analysis to guide model checking of java programs. In Proc. 7th Int'l. SPIN Workshop on Model Checking of Software, volume 1885 of Lecture Notes in Computer Science, pages 245--264. Springer-Verlag, Aug. 2000.

Digital Library

[14]

T. A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In Proc. 26th ACM Conference on Programming Language Design and Implementation. ACM Press, 2004.

Digital Library

[15]

Jigsaw --- W3C 's Server. Available at http://www.w3.org/Jigsaw/.

[16]

R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975.

Digital Library

[17]

R. O'Callahan and J.-D. Choi. Hybrid dynamic data race detection. In Proc. ACM SIGPLAN 2003 Symposium on Principles and Practice of Parallel Programming (PPoPP), June 2003.

Digital Library

[18]

A. Sasturkar, R. Agarwal, L. Wang, and S. D. Stoller. Automated type-based analysis of data races and atomicity. In Proc. ACM SIGPLAN 2005 Symposium on Principles and Practice of Parallel Programming (PPoPP). ACM Press, June 2005.

Digital Library

[19]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems, 15(4):391--411, Nov. 1997.

Digital Library

[20]

C. von Praun and T. R. Gross. Object race detection. In Proc. 16th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), volume 36(11) of SIGPLAN Notices, pages 70--82. ACM Press, Oct. 2001.

Digital Library

[21]

L. Wang and S. D. Stoller. Run-time analysis for atomicity. In Proc. Third Workshop on Runtime Verification (RV), volume 89(2) of Electronic Notes in Theoretical Computer Science. Elsevier, July 2003. A revised and expanded version appeared as Technical Report DAR 04-14, Computer Science Department, SUNY Stony Brook, July 2004 (revised May 2005). Available at http://www.cs.sunysb.edu/~stoller/.

Cited By

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
Yu BTian CXing HYang ZSu JLu XYang JZhao LLi XDuan ZChandra SBlincoe KTonella P(2023)Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-TriggeringProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616276(1153-1164)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3616276
Jahić JBauer TKuhn TWehn NAntonino P(2020)FERA: A Framework for Critical Assessment of Execution Monitoring Based Approaches for Finding Concurrency BugsIntelligent Computing10.1007/978-3-030-52249-0_5(54-74)Online publication date: 4-Jul-2020
https://doi.org/10.1007/978-3-030-52249-0_5
Show More Cited By

Index Terms

Recommendations

Automated type-based analysis of data races and atomicity
PPoPP '05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming

Concurrent programs are notorious for containing errors that are difficult to reproduce and diagnose at run-time. This motivated the development of type systems that statically ensure the absence of some common kinds of concurrent programming errors ...
Types for atomicity: Static checking and inference for Java

Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads. Atomic ...
Dynamic race detection for C++11
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

The intricate rules for memory ordering and synchronisation associated with the C/C++11 memory model mean that data races can be difficult to eliminate from concurrent programs. Dynamic data race analysis can pinpoint races in large and complex ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '05: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering

November 2005

482 pages

ISBN:1581139934

DOI:10.1145/1101908

General Chair:
David Redmiles
University of California, Irvine, CA
,
Program Chairs:
Tom Ellman
Vassar College
,
Andrea Zisman
City University, UK

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part 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 components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 November 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ASE05

Sponsor:

ASE05: International Conference on Automated Software Engineering 2005

November 7 - 11, 2005

CA, Long Beach, USA

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

56
Total Citations
View Citations
388
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)2

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Yu BTian CXing HYang ZSu JLu XYang JZhao LLi XDuan ZChandra SBlincoe KTonella P(2023)Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-TriggeringProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616276(1153-1164)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3616276
Jahić JBauer TKuhn TWehn NAntonino P(2020)FERA: A Framework for Critical Assessment of Execution Monitoring Based Approaches for Finding Concurrency BugsIntelligent Computing10.1007/978-3-030-52249-0_5(54-74)Online publication date: 4-Jul-2020
https://doi.org/10.1007/978-3-030-52249-0_5
Jahić JKuhn TJung MWehn NMudge TPnevmatikatos D(2018)BOSMIProceedings of the 18th International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation10.1145/3229631.3229641(131-138)Online publication date: 15-Jul-2018
https://dl.acm.org/doi/10.1145/3229631.3229641
Bianchi FMargara APezze M(2018)A Survey of Recent Trends in Testing Concurrent Software SystemsIEEE Transactions on Software Engineering10.1109/TSE.2017.270708944:8(747-783)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1109/TSE.2017.2707089
Jahic JJung MKuhn TKestel CWehn N(2018)A Framework for Non-intrusive Trace-driven Simulation of Manycore Architectures with Dynamic Tracing ConfigurationRuntime Verification10.1007/978-3-030-03769-7_28(458-468)Online publication date: 8-Nov-2018
https://doi.org/10.1007/978-3-030-03769-7_28
Wu ZLu KWang X(2016)Surveying concurrency bug detectors based on types of detected bugs根据bug类型综述并行bug检测器Science China Information Sciences10.1007/s11432-015-0203-260:3Online publication date: 13-Oct-2016
https://doi.org/10.1007/s11432-015-0203-2
Parízek PLhoták O(2015)Model checking of concurrent programs with static analysis of field accessesScience of Computer Programming10.1016/j.scico.2014.10.00898:P4(735-763)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.10.008
Araujo WBriand LLabiche Y(2014)On the Effectiveness of Contracts as Test Oracles in the Detection and Diagnosis of Functional Faults in Concurrent Object-Oriented SoftwareIEEE Transactions on Software Engineering10.1109/TSE.2014.233982940:10(971-992)Online publication date: 1-Oct-2014
https://doi.org/10.1109/TSE.2014.2339829
Yoshiura NWei W(2014)Static Data Race Detection for Java Programs with Dynamic Class LoadingInternet and Distributed Computing Systems10.1007/978-3-319-11692-1_14(161-173)Online publication date: 2014
https://doi.org/10.1007/978-3-319-11692-1_14
Show More Cited By

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents