skip to main content
10.1145/1375581.1375618acmconferencesArticle/Chapter ViewAbstractPublication PagespldiConference Proceedingsconference-collections
research-article

Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs

Published: 07 June 2008 Publication History

Abstract

Atomicity is a fundamental correctness property in multithreaded programs, both because atomic code blocks are amenable to sequential reasoning (which significantly simplifies correctness arguments), and because atomicity violations often reveal defects in a program's synchronization structure. Unfortunately, all atomicity analyses developed to date are incomplete in that they may yield false alarms on correctly synchronized programs, which limits their usefulness.
We present the first dynamic analysis for atomicity that is both sound and complete. The analysis reasons about the exact dependencies between operations in the observed trace of the target program, and it reports error messages if and only if the observed trace is not conflict-serializable. Despite this significant increase in precision, the performance and coverage of our analysis is competitive with earlier incomplete dynamic analyses for atomicity.

References

[1]
R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized run-time race detection and atomicity checking using partial discovered types. In International Conference on Automated Software Engineering, pages 233--242, 2005.
[2]
R. Agarwal and S. D. Stoller. Type inference for parameterized race-free Java. In Conference on Verification, Model Checking, and Abstract Interpretation, pages 149--160, 2004.
[3]
BCEL. http://jakarta.apache.org/bcel, 2007.
[4]
P. A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.
[5]
CERN. Colt 1.2.0. http://dsd.lbl.gov/~hoschek/colt, 2007.
[6]
X. Deng, M. Dwyer, J. Hatcliff, and M. Mizuno. Invariantbased specification, synthesis, and verification of synchronization in concurrent programs. In International Conference on Software Engineering, pages 442--452, 2002.
[7]
T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: a race and transaction-aware Java runtime. In Conference on Programming Language Design and Implementation, pages 245--255, 2007.
[8]
J. L. Eppinger, L. B. Mummert, and A. Z. Spector. Camelot and Avalon: A Distributed Transaction Facility. 1991.
[9]
K. P. Eswaran, J. Gray, R. A. Lorie, and I. L. Traiger. The notions of consistency and predicate locks in a database system. Communications of the ACM, 19(11):624--633, 1976.
[10]
A. Farzan and P. Madhusudan. Causal atomicity. In Computer Aided Verification, pages 315--328, 2006.
[11]
C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In Symposium on Principles of Programming Languages, pages 256--267, 2004.
[12]
C. Flanagan, S. N. Freund, and M. Lifshin. Type inference for atomicity. In Workshop on Types in Language Design and Implementation, pages 47--58, 2005.
[13]
C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. IEEE Trans. Soft. Eng., 31(4):275--291, 2005.
[14]
C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Conference on Programming Language Design and Implementation, pages 338--349, 2003.
[15]
E. Fleury and G. Sutre. Raja, version 0.4.0-pre4. http://raja.-sourceforge.net/, 2007.
[16]
E. R. Gansner and S. C. North. An open graph visualization system and its applications to software engineering. Software Practice Experience, 30(11):1203--1233, 2000.
[17]
K. Gharachorloo. Memory Consistency Models for Shared-Memory Multiprocessors. PhD thesis, Stanford University, 1995.
[18]
T. Harris and K. Fraser. Language support for lightweight transactions. In Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 388--402, 2003.
[19]
J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In International Conference on Verification, Model Checking and Abstract Interpretation, pages 175--190, 2004.
[20]
K. Havelund. Using runtime analysis to guide model checking of Java programs. In SPIN Model Checking and Software Verification, pages 245--264, 2000.
[21]
M. Hicks, J. S. Foster, and P. Pratikakis. Inferring locking for atomic sections. In Workshop on Languages, Compilers, and Hardware Support for Transactional Computing, 2006.
[22]
C. A. R. Hoare. Towards a theory of parallel programming. In Operating Systems Techniques, volume 9 of A.P.I.C. Studies in Data Processing, pages 61--71, 1972.
[23]
S. Jagannathan, J. Vitek, A.Welc, and A. L. Hosking. A transactional object calculus. Sci. Comput. Program., 57(2):164--186, 2005.
[24]
Java Grande Forum. Java Grande benchmark suite. http://www.javagrande.org/, 2003.
[25]
T. Kistler and J. Marais. WebL ? a programming language for the web. In World Wide Web Conference, pages 259--270, 1998.
[26]
L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558--565, 1978.
[27]
R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975.
[28]
B. Liskov, D. Curtis, P. Johnson, and R. Scheifler. Implementation of Argus. In Symposium on Operating Systems Principles, pages 111--122, 1987.
[29]
D. B. Lomet. Process structuring, synchronization, and recovery using atomic actions. Language Design for Reliable Software, pages 128--137, 1977.
[30]
F. Mattern. Virtual time and global states of distributed systems. In Parallel and Distributed Algorithms: International Workshop on Parallel and Distributed Algorithms. 1988.
[31]
B. McCloskey, F. Zhou, D. Gay, and E. Brewer. Autolocker: synchronization inference for atomic sections. In Symposium on Principles of Programming Languages, pages 346--358, 2006.
[32]
R. O?Callahan and J.-D. Choi. Hybrid dynamic data race detection. In Symposium on Principles and Practice of Parallel Programming, pages 167--178, 2003.
[33]
E. Pozniansky and A. Schuster. Efficient on-the-fly data race detection in multihreaded C++ programs. In Symposium on Principles and Practice of Parallel Programming, pages 179--190, 2003.
[34]
M. Ronsse and K. D. Bosschere. RecPlay: A fully integrated practical record/replay system. ACM Trans. Comput. Syst., 17(2):133--152, 1999.
[35]
A. Sasturkar, R. Agarwal, L. Wang, and S. D. Stoller. Automated type-based analysis of data races and atomicity. In Symposium on Principles and Practice of Parallel Programming, pages 83--94, 2005.
[36]
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, 1997.
[37]
E. Schonberg. On-the-fly detection of access anomalies. In Conference on Programming Language Design and Implementation, pages 285--297, 1989.
[38]
N. Shavit and D. Touitou. Software transactional memory. In Symposium on Principles of Distributed Computing, pages 204--213, 1995.
[39]
Standard Performance Evaluation Corporation. SPEC benchmarks. http://www.spec.org/, 2003.
[40]
M. Vaziri, F. Tip, and J. Dolby. Associating synchronization constraints with data in an object-oriented language. In Symposium on Principles of Programming Languages, pages 334--345, 2006.
[41]
C. von Praun and T. Gross. Static conflict analysis for multi-threaded object-oriented programs. In Conference on Programming Language Design and Implementation, pages 115--128, 2003.
[42]
L. Wang and S. D. Stoller. Static analysis of atomicity for programs with non-blocking synchronization. In Symposium on Principles and Practice of Parallel Programming, pages 61--71, 2005.
[43]
L.Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In Symposium on Principles and Practice of Parallel Programming, pages 137--146, 2006.
[44]
L. Wang and S. D. Stoller. Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Soft. Eng., 32:93--110, Feb. 2006.
[45]
World Wide Web Consortium. Jigsaw. http://www.w3c.org, 2001.
[46]
M. Xu, R. Bodík, and M. D. Hill. A serializability violation detector for shared-memory server programs. In Conference on Programming Language Design and Implementation, pages 1--14, 2005.
[47]
Y. Yu, T. Rodeheffer, and W. Chen. Racetrack: efficient detection of data race conditions via adaptive tracking. In Symposium on Operating System Principles, pages 221--234, 2005.

Cited By

View all
  • (2024)Predictive Monitoring against Pattern Regular LanguagesProceedings of the ACM on Programming Languages10.1145/36329158:POPL(2191-2225)Online publication date: 5-Jan-2024
  • (2024)Coarser Equivalences for Causal ConcurrencyProceedings of the ACM on Programming Languages10.1145/36328738:POPL(911-941)Online publication date: 5-Jan-2024
  • (2024)CSSTs: A Dynamic Data Structure for Partial Orders in Concurrent Execution AnalysisProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651358(223-238)Online publication date: 27-Apr-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2008
396 pages
ISBN:9781595938602
DOI:10.1145/1375581
  • General Chair:
  • Rajiv Gupta,
  • Program Chair:
  • Saman Amarasinghe
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 43, Issue 6
    PLDI '08
    June 2008
    382 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/1379022
    Issue’s Table of Contents
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 June 2008

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. atomicity
  2. dynamic analysis
  3. serializability

Qualifiers

  • Research-article

Conference

PLDI '08
Sponsor:

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)60
  • Downloads (Last 6 weeks)6
Reflects downloads up to 23 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Predictive Monitoring against Pattern Regular LanguagesProceedings of the ACM on Programming Languages10.1145/36329158:POPL(2191-2225)Online publication date: 5-Jan-2024
  • (2024)Coarser Equivalences for Causal ConcurrencyProceedings of the ACM on Programming Languages10.1145/36328738:POPL(911-941)Online publication date: 5-Jan-2024
  • (2024)CSSTs: A Dynamic Data Structure for Partial Orders in Concurrent Execution AnalysisProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651358(223-238)Online publication date: 27-Apr-2024
  • (2023)Sound Dynamic Deadlock Prediction in Linear TimeProceedings of the ACM on Programming Languages10.1145/35912917:PLDI(1733-1758)Online publication date: 6-Jun-2023
  • (2023)Asynchronous Wait-Free Runtime Verification and Enforcement of LinearizabilityProceedings of the 2023 ACM Symposium on Principles of Distributed Computing10.1145/3583668.3594563(90-101)Online publication date: 19-Jun-2023
  • (2023)Davida: A Decentralization Approach to Localizing Transaction Sequences for Debugging Transactional Atomicity ViolationsIEEE Transactions on Reliability10.1109/TR.2022.317668072:2(808-826)Online publication date: Jun-2023
  • (2023)When Memory Corruption Met Concurrency: Vulnerabilities in Concurrent ProgramsIEEE Access10.1109/ACCESS.2023.327283311(44725-44740)Online publication date: 2023
  • (2023)Static Deadlock Detection in Low-Level C CodeComputer Aided Systems Theory – EUROCAST 202210.1007/978-3-031-25312-6_31(267-276)Online publication date: 10-Feb-2023
  • (2023)Software Fault Localization: an Overview of Research, Techniques, and ToolsHandbook of Software Fault Localization10.1002/9781119880929.ch1(1-117)Online publication date: 21-Apr-2023
  • (2022)A tree clock data structure for causal orderings in concurrent executionsProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3503222.3507734(710-725)Online publication date: 28-Feb-2022
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media