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

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: Rahul Agarwal , Amit Sasturkar , Liqiang Wang , Scott D. Stoller, Optimized run-time race detection and atomicity checking using partial discovered types, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101944]
• 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: Philip A. Bernstein , Vassco Hadzilacos , Nathan Goodman, Concurrency control and recovery in database systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1987
• 5: CERN. Colt 1.2.0. http://dsd.lbl.gov/~hoschek/colt, 2007.
• 6: Xianghua Deng , Matthew B. Dwyer , John Hatcliff , Masaaki Mizuno, Invariant-based specification, synthesis, and verification of synchronization in concurrent programs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581394]
• 7: Tayfun Elmas , Shaz Qadeer , Serdar Tasiran, Goldilocks: a race and transaction-aware java runtime, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 8: Jeffrey L. Eppinger , Lily B. Mummert , Alfred Z. Spector, Camelot and Avalon: a distributed transaction facility, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1991
• 9: K. P. Eswaran , J. N. Gray , R. A. Lorie , I. L. Traiger, The notions of consistency and predicate locks in a database system, Communications of the ACM, v.19 n.11, p.624-633, Nov. 1976 [doi>10.1145/360363.360369]
• 10: A. Farzan and P. Madhusudan. Causal atomicity. In Computer Aided Verification, pages 315--328, 2006.
• 11: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 12: Cormac Flanagan , Stephen N. Freund , Marina Lifshin, Type inference for atomicity, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.47-58, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040299]
• 13: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting Purity for Atomicity, IEEE Transactions on Software Engineering, v.31 n.4, p.275-291, April 2005 [doi>10.1109/TSE.2005.47]
• 14: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 15: E. Fleury and G. Sutre. Raja, version 0.4.0-pre4. http://raja.-sourceforge.net/, 2007.
• 16: Emden R. Gansner , Stephen C. North, An open graph visualization system and its applications to software engineering, Software—Practice & Experience, v.30 n.11, p.1203-1233, Sept. 2000 [doi>10.1002/1097-024X(200009)30:11<1203::AID-SPE338>3.3.CO;2-E]
• 17: Kourosh Gharachorloo, Memory consistency models for shared-memory multiprocessors, Stanford University, Stanford, CA, 1996
• 18: Tim Harris , Keir Fraser, Language support for lightweight transactions, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 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: Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.245-264, August 30-September 01, 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: Suresh Jagannathan , Jan Vitek , Adam Welc , Antony Hosking, A transactional object calculus, Science of Computer Programming, v.57 n.2, p.164-186, August 2005 [doi>10.1016/j.scico.2005.03.001]
• 24: Java Grande Forum. Java Grande benchmark suite. http://www.javagrande.org/, 2003.
• 25: Thomas Kistler , Hannes Marais, WebL - a programming language for the Web, Proceedings of the seventh international conference on World Wide Web 7, p.259-270, April 1998, Brisbane, Australia
• 26: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 27: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 28: B. Liskov , D. Curtis , P. Johnson , R. Scheifer, Implementation of Argus, Proceedings of the eleventh ACM Symposium on Operating systems principles, p.111-122, November 08-11, 1987, Austin, Texas, United States
• 29: D. B. Lomet, Process structuring, synchronization, and recovery using atomic actions, Proceedings of an ACM conference on Language design for reliable software, p.128-137, March 28-30, 1977, Raleigh, North Carolina
• 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: Bill McCloskey , Feng Zhou , David Gay , Eric Brewer, Autolocker: synchronization inference for atomic sections, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.346-358, January 11-13, 2006, Charleston, South Carolina, USA
• 32: Robert O'Callahan , Jong-Deok Choi, Hybrid dynamic data race detection, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 33: Eli Pozniansky , Assaf Schuster, Efficient on-the-fly data race detection in multithreaded C++ programs, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 34: Michiel Ronsse , Koen De Bosschere, RecPlay: a fully integrated practical record/replay system, ACM Transactions on Computer Systems (TOCS), v.17 n.2, p.133-152, May 1999 [doi>10.1145/312203.312214]
• 35: Amit Sasturkar , Rahul Agarwal , Liqiang Wang , Scott D. Stoller, Automated type-based analysis of data races and atomicity, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065956]
• 36: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 37: D. Schonberg, On-the-fly detection of access anomalies, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.285-297, June 19-23, 1989, Portland, Oregon, United States
• 38: Nir Shavit , Dan Touitou, Software transactional memory, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.204-213, August 20-23, 1995, Ottowa, Ontario, Canada [doi>10.1145/224964.224987]
• 39: Standard Performance Evaluation Corporation. SPEC benchmarks. http://www.spec.org/, 2003.
• 40: Mandana Vaziri , Frank Tip , Julian Dolby, Associating synchronization constraints with data in an object-oriented language, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.334-345, January 11-13, 2006, Charleston, South Carolina, USA
• 41: Christoph von Praun , Thomas R. Gross, Static conflict analysis for multi-threaded object-oriented programs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 42: Liqiang Wang , Scott D. Stoller, Static analysis of atomicity for programs with non-blocking synchronization, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065953]
• 43: Liqiang Wang , Scott D. Stoller, Accurate and efficient runtime detection of atomicity errors in concurrent programs, Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming, March 29-31, 2006, New York, New York, USA [doi>10.1145/1122971.1122993]
• 44: Liqiang Wang , Scott D. Stoller, Runtime Analysis of Atomicity for Multithreaded Programs, IEEE Transactions on Software Engineering, v.32 n.2, p.93-110, February 2006 [doi>10.1109/TSE.2006.1599419]
• 45: World Wide Web Consortium. Jigsaw. http://www.w3c.org, 2001.
• 46: Min Xu , Rastislav Bodík , Mark D. Hill, A serializability violation detector for shared-memory server programs, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 47: Yuan Yu , Tom Rodeheffer , Wei Chen, RaceTrack: efficient detection of data race conditions via adaptive tracking, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing); Monitors

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Languages, Verification

Keywords:
atomicity, dynamic analysis, serializability