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.
- Gul Agha. An overview of actor languages. In Proceedings of the 1986 SIGPLAN workshop on Object-oriented programming, pages 58--67, New York, NY, USA, 1986. Google ScholarDigital Library
- C. S. Ananian and M. Rinard. Language-level transactions. In High-Performance Embedded Computing (HPEC), 2004.Google Scholar
- C. Artho, K. Havelund, and A. Biere. High-level data races. In Proc. NDDL/VVEIS'03, pages 82--93, 2003.Google ScholarCross Ref
- C. Artho, K. Havelund, and A. Biere. Using block-local atomicity to detect stale-value concurrency errors. In ATVA'04, pages 150--164, 2004.Google ScholarCross Ref
- D. F. Bacon, R. E. Strom, and A. Tarafdar. Guava: A dialect of Java without data races. In Proc. OOPSLA'00, pages 382--400, 2000. Google ScholarDigital Library
- 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.Google Scholar
- H. Berenson, P. Bernstein, J. Gray, J. Melton, E. O'Neil, and P. O'Neil. A critique of ANSI SQL isolation levels. In Proc. ACM SIGMOD Conf., pages 1--10, 1995. Google ScholarDigital Library
- P. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987. Google ScholarDigital Library
- C. Boyapati and M. Rinard. A parameterized type system for race-free Java programs. In Proc. OOPSLA'01, October 2001. Google ScholarDigital Library
- M. Burrows and K. R. M. Leino. Finding stale-value errors in concurrent programs. Technical Report 2002-004, SRC, May 2002.Google Scholar
- Philippe Charles, Christopher Donawa, Kemal Ebcioglu, Christian Grothoff, Allan Kielstra, Vijay Saraswat, Vivek Sarkar, and Christoph von Praun. X10: An object-oriented approach to non-uniform cluster computing. In Proc. OOPSLA'05, San Diego, CA, 2005. To appear. Google ScholarDigital Library
- A. Chien, U. Reddy, J. Plevyak, and J. Dolby. ICC++ - A C++ dialect for high performance parallel computing. Lecture Notes in Computer Science, 1049:76--95, 1996. Google ScholarDigital Library
- Andrew A. Chien and William J. Dally. Concurrent aggregates (ca). In Proc. PPoPP '90, pages 187--196, 1990. Google ScholarDigital Library
- X. Deng, M. Dwyer, J. Hatcliff, and M. Mizuno. Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In Proc. ICSE'02, May 2002. Google ScholarDigital Library
- D. Engler and K. Ashcraft. Racerx: Effective, static detection of race conditions and deadlocks. In Proc. SOSP'03, pages 237--252, October 2003. Google ScholarDigital Library
- S. Fink, J. Dolby, , and L. Colby. Semi-automatic J2EE transaction configuration. Technical Report RC23326, IBM T.J. Watson Research Center, March 2004.Google Scholar
- C. Flanagan. Verifying commit-atomicity using model checking. In Proc. SPIN'04, pages 252--266, 2004.Google ScholarCross Ref
- C. Flanagan, S. Freund, and M. Lifshin. Type inference for atomicity. In Proc. TLDI'05, pages 47--58, 2005. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Type-based race detection for Java. In Proc. PLDI'00, pages 219--232, 2000. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In Proc. POPL'04, pages 256--267, 2004. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proc. PLDI'03, pages 338--349, 2003. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Types for atomicity. In Proc. TLDI'03, pages 1--12, 2003. Google ScholarDigital Library
- T. Harris and K. Fraser. Language support for lightweight transactions. In Proc. OOPSLA'03, pages 388--402, 2003. Google ScholarDigital Library
- T. Harris, S. Marlow, S. Peyton-Jones, and M. Herlihy. Composable memory transactions. In Proc. PPoPP'05, 2005. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Gary A. Kildall. A unified approach to global program optimization. In Proc. POPL'73, pages 194--206, 1973. Google ScholarDigital Library
- K. R. M. Leino. Data groups: Specifying the modification of extended state. In Proc. OOPSLA'98, pages 144--153, 1998. Google ScholarDigital Library
- K. R. M. Leino, J. B. Saxe, and R. Stata. Checking Java programs via guarded commands. Technical Report 002, Compaq SRC, 1999.Google Scholar
- R. J. Lipton. Reduction: A method of proving properties of parallel programs. CACM, 18(12), 1975. Google ScholarDigital Library
- R. O'Callahan and J.-D. Choi. Hybrid dynamic data race detection. In Proc. PPoPP'03, pages 167--178, 2003. Google ScholarDigital Library
- Java Community Process. JSR 166: Concurrency utilities. See http://gee.cs.oswego.edu/dl/concurrency-interest/index.html., September 2004.Google Scholar
- A. Sasturkar, R. Agarwal, L. Wang, and S. Stoller. Automated type-based analysis of data races and atomicity. In Proc. PPoPP'05, 2005. Google ScholarDigital Library
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multi-threaded programs. In Proc. SOSP'97, pages 27--37, October 1997. Google ScholarDigital Library
- C. von Praun and T. Gross. Static detection of atomicity violations in object-oriented programs. Journal of Object Technology, 3(2), 2004.Google Scholar
- 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.Google Scholar
- A. Welc, S. Jagannathan, and A. Hosking. Transactional monitors for concurrent objects. In Proc. ECOOP'04, pages 519--542, 2004.Google ScholarCross Ref
- ANSI X3.135-1992. In American National Standard for Information Systems -- Database Language -- SQL, November 1992.Google Scholar
- M. Xu, R. Bodik, and M. Hill. A serializability violation detector for shared-memory server programs. In Proc. PLDI'05, pages 1--14, 2005. Google ScholarDigital Library
Index Terms
- Associating synchronization constraints with data in an object-oriented language
Recommendations
Associating synchronization constraints with data in an object-oriented language
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesConcurrency-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 ...
A data-centric approach to synchronization
Concurrency-related errors, such as data races, are frustratingly difficult to track down and eliminate in large object-oriented programs. Traditional approaches to preventing data races rely on protecting instruction sequences with synchronization ...
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 ...
Comments