Dynamic detection of atomic-set-serializability violations

ABSTRACT

Previously 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 correctness criterion for concurrent programs, stating that units of work must be serializable for each atomic set. We showed that a set of problematic data access patterns characterize executions that are not atomic-set serializable. Our criterion subsumes data races (single-location atomic sets) and serializability (all locations in one set).

In this paper, we present a dynamic analysis for detecting violations of atomic-set serializability. The analysis can be implemented efficiently, and does not depend on any specific synchronization mechanism. We implemented the analysis and evaluated it on a suite of real programs and benchmarks. We found a number of known errors as well as several problems not previously reported.

REFERENCES

• 1: T. J. Watson Libraries for Analysis (WALA). http://wala.sourceforge.net/wiki/index.php.
• 2: 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]
• 3: C. Artho, K. Havelund, and A. Biere. High-level data races. Journal on Software Testing, Verification and Reliability (STVR), 13(4):207--227, 2003.
• 4: C. Artho, K. Havelund, and A. Biere. Using block-local atomicity to detect stale-value concurrency errors. In Automated Technology for Verification and Analysis (ATVA'04), 2004.
• 5: Ittai Balaban , Frank Tip , Robert Fuhrer, Refactoring support for class library migration, ACM SIGPLAN Notices, v.40 n.10, October 2005
• 6: Y. Ben-Asher, Y. Eytani, E. Farchi, and S. Ur. Noise makers need to know where to be silent - producing schedules that find bugs. In International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA), 2006.
• 7: Philip A. Bernstein , Vassco Hadzilacos , Nathan Goodman, Concurrency control and recovery in database systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1987
• 8: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 9: Michael Burrows , K. Rustan M. Leino, Finding stale-value errors in concurrent programs: Research Articles, Concurrency and Computation: Practice & Experience, v.16 n.12, p.1161-1172, October 2004 [doi>10.1002/cpe.v16:12]
• 10: Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 11: Yaniv Eytani , Klaus Havelund , Scott D. Stoller , Shmuel Ur, Towards a framework and a benchmark for testing tools for multi-threaded programs: Research Articles, Concurrency and Computation: Practice & Experience, v.19 n.3, p.267-279, March 2007 [doi>10.1002/cpe.v19:3]
• 12: Y. Eytani and S. Ur. Compiling a benchmark of documented multi-threaded bugs. In Proc. IEEE International Parallel & Distributed Processing Symposium (IPDPS'04), 2004.
• 13: Y. Eytani and S. Ur. Compiling a benchmark of documented multi-threaded bugs. In Proc. IEEE International Parallel & Distributed Processing Symposium (IPDPS'04), 2004.
• 14: 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
• 15: 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]
• 16: 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
• 17: Cormac Flanagan , Shaz Qadeer, Types for atomicity, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 18: Jason Gait, A probe effect in concurrent programs, Software—Practice & Experience, v.16 n.3, p.225-233, March 1986 [doi>10.1002/spe.4380160304]
• 19: Tim Peierls , Brian Goetz , Joshua Bloch , Joseph Bowbeer , Doug Lea , David Holmes, Java Concurrency in Practice, Addison-Wesley Professional, 2005
• 20: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 21: 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]
• 22: Shan Lu , Joseph Tucek , Feng Qin , Yuanyuan Zhou, AVIO: detecting atomicity violations via access interleaving invariants, Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, October 21-25, 2006, San Jose, California, USA
• 23: Sang L. Min , Jong-Deok Choi, An efficient cache-based access anomaly detection scheme, Proceedings of the fourth international conference on Architectural support for programming languages and operating systems, p.235-244, April 08-11, 1991, Santa Clara, California, United States
• 24: Mayur Naik , Alex Aiken, Conditional must not aliasing for static race detection, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 25: Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 26: Satish Narayanasamy , Zhenghao Wang , Jordan Tigani , Andrew Edwards , Brad Calder, Automatically classifying benign and harmful data racesallusing replay analysis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 27: Robert H. B. Netzer , Barton P. Miller, What are race conditions?: Some issues and formalizations, ACM Letters on Programming Languages and Systems (LOPLAS), v.1 n.1, p.74-88, March 1992 [doi>10.1145/130616.130623]
• 28: 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
• 29: Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 30: 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]
• 31: 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]
• 32: 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
• 33: Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
• 34: C. von Praun and T. R. Gross. Atomicity violations in object-oriented programs. Journal of Object Technology, 3(6):103--122, June 2004. Special issue: ECOOP 2003 workshop on FTfJP.
• 35: L. Wang and S. D. Stoller. Run-time analysis for atomicity. In Proceedings of the Workshop on Runtime Verification (RV'03), 2003. Volume 89(2) of Electronic Notes in Theoretical Computer Science. Elsevier.
• 36: 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]
• 37: 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]
• 38: 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

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Tracing

General Terms:
Algorithms, Experimentation, Measurement, Reliability

Keywords:
atomicity, concurrent object-oriented programming, data races, dynamic analysis, serializability