Article

Detecting race conditions in large programs

Authors:

Cormac Flanagan,

Stephen N. FreundAuthors Info & Claims

PASTE '01: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering

Pages 90 - 96

https://doi.org/10.1145/379605.379687

Published: 01 June 2001 Publication History

Abstract

The race condition checker \rcc{} statically identifies potential races in concurrent Java programs. This paper describes improvements to \rcc{} that enable it to be used on large, realistic programs. These improvements include not only extensions to the underlying analysis, but also an annotation inference algorithm and a user interface to help programmers understand warnings generated by the tool. Experience with programs containing up to 500,000 lines of code indicate that it is an effective tool for identifying races in large-scale software systems.

References

[1]

J. Aldrich, C. Chambers, E. G. Sirer, and S. Eggers. Static analyses for eliminating unnecessary synchronization from Java programs. In Proceedings of the Sixth International Static Analysis Symposium, September 1999.]]

Digital Library

[2]

T. Amtoft, F. Nielson, and H. R. Nielson. Type and behaviour reconstruction for higher-order concurrent programs. Journal of Fanctional Programming, 7(3):321347, 1997.]]

Digital Library

[3]

A. D. Birrell. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center, 1989.]]

[4]

B. Blanchet. Escape analysis for object-oriented languages. Application to, Java. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.]]

Digital Library

[5]

J. Bogda and U. HSlzle. Removing unnecessary synchronization in Java. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.]]

Digital Library

[6]

L. Cardelli. Mobile ambient synchronization. Technical Report 1997-013, Digital Systems Research Center, Palo Alto, CA, July 1997.]]

[7]

J. Choi, M. Gupta, M. Serrano, V. Sreedhar, and S. Midkiff. Escape analysis for,Java. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.]]

Digital Library

[8]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238-252 Jan. 1977.]]

Digital Library

[9]

C. Flanagan and M. Abadi. Types for safe locking. In Proceedings of European Symposium on Programming, March 1999.]]

Digital Library

[10]

C. Flanagan and S. N. Freund. Type-based Race Detection for Java. In Proceedings of the Symposium on the Programming Language Design and IrnpIementation, 2000.]]

Digital Library

[11]

C. Flanagan, R. Joshi, and K. R. M. Leino. Annotation inference for modular checkers. Information Processing Letters, 2001. To appear.]]

Digital Library

[12]

C. Flanagan and K. R. M. Leino. Houdini, an Annotation Assistant for ESC/Java. In Formal Methods Europe '01, 2001.]]

Digital Library

[13]

S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, CAV 97: Computer Aided Verification, Lecture Notes in Computer Science 1254, pages 7283. Springer-Verlag, 1997.]]

Digital Library

[14]

P. Jouvelot and D. Gifford. Algebraic reconstruction of types and effects. In Proceedings of the 18th Symposium on Principles of Programming Languages, pages 303-310, 1991.]]

Digital Library

[15]

T. Kistler and J. Marais. WebL a programming language for the web. Computer Networks and ISDN Systems, 30:259-270, April 1998.]]

Digital Library

[16]

K. R. M. Leino, J. B. Saxe, and R. Stata. Checking Java programs via guarded commands. Technical Report 1999-002, Cornpaq Systems Research Center, Palo Alto, CA, May 1999. Also appeared in Formal Techniques for Java Programs, workshop proceedings. Bart Jacobs, Gary T. Leavens, Peter Muller, and Arnd Poetzsch-Heffter, editors. Technical Report 251, Fernuniversitat Hagen, 1999.]]

[17]

J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proceedings of the ACM Conference on Lisp and Fanctional Programming, pages 47-57, 1988.]]

Digital Library

[18]

F. Nielson. Annotated type and effect systems. ACM Computing Surveys, 28(2):344345, 1996. Invited position statement for the Symposium on Models of Programming Languages and Computation.]]

Digital Library

[19]

S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):97-106, 1976.]]

Digital Library

[20]

Standard Performance Evaluation Corporation. SPEC JBB2000. available from http://www.spec.org/osg/jbb2000/, June 2000.]]

[21]

N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97-106, 1993.]]

[22]

J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Fanctional Programming, 2(3):245 271, 1992.]]

[23]

M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value lambda-cMculus using a stack of regions. In Proceedings of the 21st Symposium on Principles of Programming Languages, pages 188201, 1994.]]

Digital Library

[24]

M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109 176, 1997.]]

Digital Library

[25]

M. Wand. Finding the source of type errors. In Conf. Rec. 13th ACM Syrup. on Principles of Prog. Lang., pages 38-43, 1986.]]

Digital Library

[26]

J. Whaley and M. Rinard. CornpositionM pointer and escape analysis for Java programs. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.]]

Digital Library

[27]

World Wide Web Consortium. Jigsaw. available from http://www.w3c.org, January 2001.]]

[28]

J. Yang, G. Michaelson, P. Trinder, and J. B. Wells. Improved Type Error Reporting. In M. Mohnen and P. Koopman, editors, Proceedings of the 12th International Workshop on Irnplementation of Fanctional Languages, number AIB-00-7 in Aachener Informatik Berichte, pages 7186. RWTH Aachen, 2000.]]

[29]

Y. Yu, P. Manolios, and L. Lamport. Model Checking TLA+ Specifications. In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods (CHARME '99), number 1703 in Lecture Notes In Computer Science, pages 5466. Springer-Verlag, September 1999.]]

Digital Library

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
Bai JChen QJiang ZLawall JHu S(2022)Hybrid Static-Dynamic Analysis of Data Races Caused by Inconsistent Locking Discipline in Device DriversIEEE Transactions on Software Engineering10.1109/TSE.2021.3138735(1-1)Online publication date: 2022
https://doi.org/10.1109/TSE.2021.3138735
Almeida DBraganca LTorres FFerreira RNacif J(2021)HAMBug: A Hybrid CPU-FPGA System to Detect Race ConditionsIEEE Transactions on Circuits and Systems II: Express Briefs10.1109/TCSII.2021.309398568:9(3158-3162)Online publication date: Sep-2021
https://doi.org/10.1109/TCSII.2021.3093985
Show More Cited By

Index Terms

Detecting race conditions in large programs
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

What are race conditions?: Some issues and formalizations

In shared-memory parallel programs that use explicit synchronization, race conditions result when accesses to shared memory are not properly synchronized. Race conditions are often considered to be manifestations of bugs, since their presence can cause ...
Detecting Race Conditions in Parallel Programs That Use One Semaphore
Data-Race-Freedom of Concurrent Programs
APSEC '13: Proceedings of the 2013 20th Asia-Pacific Software Engineering Conference (APSEC) - Volume 01

Reasoning about access isolation in a program that uses locks, transactions or both to coordinate accesses to shared memory is complex and error-prone. The programmer must understand when accesses issued to the same memory by distinct threads, under ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PASTE '01: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering

June 2001

103 pages

ISBN:1581134134

DOI:10.1145/379605

Copyright © 2001 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: 01 June 2001

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PASTE01

Sponsor:

PASTE01: SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering 2001

Utah, Snowbird, USA

Acceptance Rates

PASTE '01 Paper Acceptance Rate 13 of 24 submissions, 54%;

Overall Acceptance Rate 57 of 159 submissions, 36%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

63
Total Citations
View Citations
713
Total Downloads

Downloads (Last 12 months)38
Downloads (Last 6 weeks)6

Reflects downloads up to 20 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
Bai JChen QJiang ZLawall JHu S(2022)Hybrid Static-Dynamic Analysis of Data Races Caused by Inconsistent Locking Discipline in Device DriversIEEE Transactions on Software Engineering10.1109/TSE.2021.3138735(1-1)Online publication date: 2022
https://doi.org/10.1109/TSE.2021.3138735
Almeida DBraganca LTorres FFerreira RNacif J(2021)HAMBug: A Hybrid CPU-FPGA System to Detect Race ConditionsIEEE Transactions on Circuits and Systems II: Express Briefs10.1109/TCSII.2021.309398568:9(3158-3162)Online publication date: Sep-2021
https://doi.org/10.1109/TCSII.2021.3093985
Yousaf MSindhu MArif MRehman S(2021)Efficient Identification of Race Condition Vulnerability in C code by Abstract Interpretation and Value Analysis2021 International Conference on Cyber Warfare and Security (ICCWS)10.1109/ICCWS53234.2021.9702954(70-75)Online publication date: 23-Nov-2021
https://doi.org/10.1109/ICCWS53234.2021.9702954
Wu MSong JSharma SDi JHe BWang ZZhang JLin LGreaney EMoon Y(2020)Development of testbed for cyber-manufacturing security issuesInternational Journal of Computer Integrated Manufacturing10.1080/0951192X.2020.173671133:3(302-320)Online publication date: 15-Mar-2020
https://doi.org/10.1080/0951192X.2020.1736711
Juma NDietl WTripunitara M(2020)A Computational Complexity Analysis of Tunable Type Inference for Generic Universe TypesTheoretical Computer Science10.1016/j.tcs.2020.01.035Online publication date: Feb-2020
https://doi.org/10.1016/j.tcs.2020.01.035
Chen QBai JJiang ZLawall JHu S(2019)Detecting Data Races Caused by Inconsistent Lock Protection in Device Drivers2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER.2019.8668017(366-376)Online publication date: Feb-2019
https://doi.org/10.1109/SANER.2019.8668017
Wu MSong JLucas Lin LAurelle NLiu YDing BSong ZMoon Y(2018)Establishment of intrusion detection testbed for CyberManufacturing systemsProcedia Manufacturing10.1016/j.promfg.2018.07.14226(1053-1064)Online publication date: 2018
https://doi.org/10.1016/j.promfg.2018.07.142
Sun QXu LChen LZhang W(2016)Replaying Harmful Data Races in Android Apps2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)10.1109/ISSREW.2016.10(160-166)Online publication date: Oct-2016
https://doi.org/10.1109/ISSREW.2016.10
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
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