Associating synchronization constraints with data in an object-oriented language

ABSTRACT

Concurrency-related bugs may happen when multiple threads access shared data and interleave in ways that do not correspond to any sequential execution. Their absence is not guaranteed by the traditional notion of "data race" freedom. We present a new definition of data races in terms of 11 problematic interleaving scenarios, and prove that it is complete by showing that any execution not exhibiting these scenarios is serializable for a chosen set of locations. Our definition subsumes the traditional definition of a data race as well as high-level data races such as stale-value errors and inconsistent views. We also propose a language feature called atomic sets of locations, which lets programmers specify the existence of consistency properties between fields in objects, without specifying the properties themselves. We use static analysis to automatically infer those points in the code where synchronization is needed to avoid data races under our new definition. An important benefit of this approach is that, in general, far fewer annotations are required than is the case with existing approaches such as synchronized blocks or atomic sections. Our implementation successfully inferred the appropriate synchronization for a significant subset of Java's Standard Collections framework.

REFERENCES

• 1: Gul Agha, An overview of actor languages, Proceedings of the 1986 SIGPLAN workshop on Object-oriented programming, p.58-67, June 09-13, 1986, Yorktown Heights, New York, United States
• 2: C. S. Ananian and M. Rinard. Language-level transactions. In High-Performance Embedded Computing (HPEC), 2004.
• 3: C. Artho, K. Havelund, and A. Biere. High-level data races. In Proc. NDDL/VVEIS'03, pages 82--93, 2003.
• 4: C. Artho, K. Havelund, and A. Biere. Using block-local atomicity to detect stale-value concurrency errors. In ATVA'04, pages 150--164, 2004.
• 5: David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
• 6: D. Bäumer, E. Gamma, and Adam Kieÿ zun. Integrating refactoring support into a Java development tool. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) Companion, October 2001.
• 7: Hal Berenson , Phil Bernstein , Jim Gray , Jim Melton , Elizabeth O'Neil , Patrick O'Neil, A critique of ANSI SQL isolation levels, Proceedings of the 1995 ACM SIGMOD international conference on Management of data, p.1-10, May 22-25, 1995, San Jose, California, United States
• 8: Philip A. Bernstein , Vassco Hadzilacos , Nathan Goodman, Concurrency control and recovery in database systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1987
• 9: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 10: M. Burrows and K. R. M. Leino. Finding stale-value errors in concurrent programs. Technical Report 2002-004, SRC, May 2002.
• 11: Philippe Charles , Christian Grothoff , Vijay Saraswat , Christopher Donawa , Allan Kielstra , Kemal Ebcioglu , Christoph von Praun , Vivek Sarkar, X10: an object-oriented approach to non-uniform cluster computing, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 12: Andrew A. Chien , Uday S. Reddy , John Plevyak , Julian Dolby, ICC++-AC++ Dialect for High Performance Parallel Computing, Proceedings of the Second JSSST International Symposium on Object Technologies for Advanced Software, p.76-95, March 11-15, 1996
• 13: Andrew A. Chien , Willaim J. Dally, Concurrent aggregates (CA), Proceedings of the second ACM SIGPLAN symposium on Principles & practice of parallel programming, p.187-196, March 14-16, 1990, Seattle, Washington, United States
• 14: 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]
• 15: 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
• 16: S. Fink, J. Dolby, , and L. Colby. Semi-automatic J2EE transaction configuration. Technical Report RC23326, IBM T.J. Watson Research Center, March 2004.
• 17: C. Flanagan. Verifying commit-atomicity using model checking. In Proc. SPIN'04, pages 252--266, 2004.
• 18: 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]
• 19: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 20: 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
• 21: 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
• 22: 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
• 23: 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
• 24: Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, 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.1065952]
• 25: J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model checking. In Proc. VMCAI'04, pages 175--190, 2004.
• 26: Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
• 27: K. Rustan M. Leino, Data groups: specifying the modification of extended state, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.144-153, October 18-22, 1998, Vancouver, British Columbia, Canada
• 28: K. R. M. Leino, J. B. Saxe, and R. Stata. Checking Java programs via guarded commands. Technical Report 002, Compaq SRC, 1999.
• 29: 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]
• 30: 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
• 31: Java Community Process. JSR 166: Concurrency utilities. See http://gee.cs.oswego.edu/dl/concurrency-interest/index.html., September 2004.
• 32: 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]
• 33: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multi-threaded programs, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.27-37, October 05-08, 1997, Saint Malo, France
• 34: C. von Praun and T. Gross. Static detection of atomicity violations in object-oriented programs. Journal of Object Technology, 3(2), 2004.
• 35: Liqiang Wang and Scott D. Stoller. Runtime analysis for atomicity for multi-threaded programs. Technical Report DAR-04-14, State University of New York At Stony Brook, May 2005.
• 36: A. Welc, S. Jagannathan, and A. Hosking. Transactional monitors for concurrent objects. In Proc. ECOOP'04, pages 519--542, 2004.
• 37: ANSI X3.135-1992. In American National Standard for Information Systems -- Database Language -- SQL, November 1992.
• 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:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming

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

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

General Terms:
Languages, Theory

Keywords:
concurrent object-oriented programming, data races, programming model, serializability