skip to main content
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
  • (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)Precise and efficient atomicity violation detection for interrupt-driven programs via staged path pruningProceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3533767.3534412(506-518)Online publication date: 18-Jul-2022
  • (2021)On interleaving space exploration of multi-threaded programsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-020-9501-615:4Online publication date: 1-Aug-2021
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 June 2008
Published in SIGPLAN Volume 43, Issue 6

Check for updates

Author Tags

  1. atomicity
  2. dynamic analysis
  3. serializability

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)56
  • Downloads (Last 6 weeks)2
Reflects downloads up to 22 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (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)Precise and efficient atomicity violation detection for interrupt-driven programs via staged path pruningProceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3533767.3534412(506-518)Online publication date: 18-Jul-2022
  • (2021)On interleaving space exploration of multi-threaded programsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-020-9501-615:4Online publication date: 1-Aug-2021
  • (2021)Concurrent Correctness in Vector SpaceVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_8(151-173)Online publication date: 12-Jan-2021
  • (2019)Efficient transaction-based deterministic replay for multi-threaded programsProceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2019.00076(760-771)Online publication date: 10-Nov-2019
  • (2018)A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniquesSoftware Quality Journal10.1007/s11219-017-9385-326:3(855-889)Online publication date: 1-Sep-2018
  • (2018)Discovering Concurrency ErrorsLectures on Runtime Verification10.1007/978-3-319-75632-5_2(34-60)Online publication date: 11-Feb-2018
  • (2017)Verifying Concurrent Programs Using Contracts2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2017.25(196-206)Online publication date: Mar-2017
  • (2017)Boosted decision trees for behaviour mining of concurrent programmesConcurrency and Computation: Practice and Experience10.1002/cpe.426829:21Online publication date: 31-Aug-2017
  • (2016)Race-driven active random testing of null-pointer dereferencesProceedings of the 8th Asia-Pacific Symposium on Internetware10.1145/2993717.2993722(63-70)Online publication date: 18-Sep-2016
  • 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