Cormac Flanagan
Stephen N. Freund
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.
- 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. Google Scholar
Digital Library
- 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.Google ScholarCross Ref
- BCEL. http://jakarta.apache.org/bcel, 2007.Google Scholar
- P. A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987. Google ScholarDigital Library
- CERN. Colt 1.2.0. http://dsd.lbl.gov/~hoschek/colt, 2007.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. L. Eppinger, L. B. Mummert, and A. Z. Spector. Camelot and Avalon: A Distributed Transaction Facility. 1991. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Farzan and P. Madhusudan. Causal atomicity. In Computer Aided Verification, pages 315--328, 2006. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. IEEE Trans. Soft. Eng., 31(4):275--291, 2005. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Conference on Programming Language Design and Implementation, pages 338--349, 2003. Google ScholarDigital Library
- E. Fleury and G. Sutre. Raja, version 0.4.0-pre4. http://raja.-sourceforge.net/, 2007.Google Scholar
- 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. Google ScholarDigital Library
- K. Gharachorloo. Memory Consistency Models for Shared-Memory Multiprocessors. PhD thesis, Stanford University, 1995. Google ScholarDigital Library
- T. Harris and K. Fraser. Language support for lightweight transactions. In Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 388--402, 2003. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- K. Havelund. Using runtime analysis to guide model checking of Java programs. In SPIN Model Checking and Software Verification, pages 245--264, 2000. Google ScholarCross Ref
- 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.Google Scholar
- 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.Google Scholar
- S. Jagannathan, J. Vitek, A.Welc, and A. L. Hosking. A transactional object calculus. Sci. Comput. Program., 57(2):164--186, 2005. Google ScholarDigital Library
- Java Grande Forum. Java Grande benchmark suite. http://www.javagrande.org/, 2003.Google Scholar
- T. Kistler and J. Marais. WebL ? a programming language for the web. In World Wide Web Conference, pages 259--270, 1998. Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558--565, 1978. Google ScholarDigital Library
- R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975. Google ScholarDigital Library
- B. Liskov, D. Curtis, P. Johnson, and R. Scheifler. Implementation of Argus. In Symposium on Operating Systems Principles, pages 111--122, 1987. Google ScholarDigital Library
- D. B. Lomet. Process structuring, synchronization, and recovery using atomic actions. Language Design for Reliable Software, pages 128--137, 1977. Google ScholarDigital Library
- F. Mattern. Virtual time and global states of distributed systems. In Parallel and Distributed Algorithms: International Workshop on Parallel and Distributed Algorithms. 1988.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- M. Ronsse and K. D. Bosschere. RecPlay: A fully integrated practical record/replay system. ACM Trans. Comput. Syst., 17(2):133--152, 1999. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- E. Schonberg. On-the-fly detection of access anomalies. In Conference on Programming Language Design and Implementation, pages 285--297, 1989. Google ScholarDigital Library
- N. Shavit and D. Touitou. Software transactional memory. In Symposium on Principles of Distributed Computing, pages 204--213, 1995. Google ScholarDigital Library
- Standard Performance Evaluation Corporation. SPEC benchmarks. http://www.spec.org/, 2003.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- L. Wang and S. D. Stoller. Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Soft. Eng., 32:93--110, Feb. 2006. Google ScholarDigital Library
- World Wide Web Consortium. Jigsaw. http://www.w3c.org, 2001.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs
Recommendations
Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs
PLDI '08Atomicity 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 ...
Dynamic detection of atomic-set-serializability violations
ICSE '08: Proceedings of the 30th international conference on Software engineeringPreviously we presented atomic sets, memory locations that share some consistency property, and units of work, code fragments that preserve consistency of atomic sets on which they are declared. We also proposed atomic-set serializability as a ...
Towards transactional memory semantics for C++
SPAA '09: Proceedings of the twenty-first annual symposium on Parallelism in algorithms and architecturesTransactional memory (TM) eliminates many problems associated with lock-based synchronization. Over recent years, much progress has been made in software and hardware implementation techniques for TM. However, before transactional memory can be ...
Comments