Cormac Flanagan
Stephen N. Freund
Skip Abstract Section
Abstract
This paper presents a static race detection analysis for multithreaded Java programs. Our analysis is based on a formal type system that is capable of capturing many common synchronization patterns. These patterns include classes with internal synchronization, classes thatrequire client-side synchronization, and thread-local classes. Experience checking over 40,000 lines of Java code with the type system demonstrates that it is an effective approach for eliminating races conditions. On large examples, fewer than 20 additional type annotations per 1000 lines of code were required by the type checker, and we found a number of races in the standard Java libraries and other test programs.
- ACSE99 Jonathan Aldrich, Craig Chambers, Emin Gun Sirer, and Susan Eggers. Static analyses for eliminating unnecessary synchronization from Java programs. In Proceedings of the Sixth International Static Analysis Symposium, September 1999.]] Google Scholar
Digital Library
- AFM97 Ole Agesen, Stephen N. Freund, and John C. Mitchell. Adding type parameterization to the Java language. In Proceedings of A CM Conference on Object Oriented Languages and Systems, October 1997.]] Google ScholarDigital Library
- AG98 Alexander Aiken and David Gay. Barrier inference. In Proceedings of the 25th Symposium on Principles of Programming Languages, pages 243-354, 1998.]] Google ScholarDigital Library
- ANN97 Torben Amtoft, Flemming Nielsen, and Hanne Riis Nielsen. Type and behaviour reconstruction for higher-order concurrent programs. Journal of Functional Programming, 7(3):321-347, 1997.]] Google ScholarDigital Library
- BH99 Jeff Bogda and Urs HSlzle. Removing unnecessary synchronization in Java. In Proceedings of A CM Conference on Object Oriented Languages and Systems, November 1999.]] Google ScholarDigital Library
- Bir89 Andrew D. Birrell. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center, 1989.]]Google Scholar
- Bla99 Bruno Blanchet. Escape analysis for object-oriented languages. Application to Java. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.]] Google ScholarDigital Library
- BLM96 J. Bank, B. Liskov, and A. Myers. Parameterized Types and Java. Technical Report MIT/LCS/TM- 553, Massachussetts Institute of Technology, 1996.]] Google ScholarDigital Library
- BOSW98 Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Making the future safe for the past: Adding genericity to the Java programming language. In Proceedings of A CM Conference on Object Oriented Languages and Systems, October 1998.]] Google ScholarDigital Library
- Car97 Luca Cardelli. Mobile ambient synchronization. Technical Report 1997-013, Digital Systems Research Center, Pale Alto, CA, July 1997.]]Google Scholar
- CGS+99 J.D. Choi, M. Gupta, M. Serrano, V.C. Sreedhar, and S. Midkiff. Escape analysis for Java. In Proceedings of A CM Conference on Object Oriented Languages and Systems, November 1999.]] Google ScholarDigital Library
- CJ98 Robert Cartwright and Guy L. Steele Jr. Compatible genericity with run-time types for the Java programming language. In Proceedings of A CM Conference on Object Oriented Languages and Systems, October 1998.]] Google ScholarDigital Library
- DE97 S. Drossopoulou and S. Eisenbach. Java is type safe --probably. In European Conference On Object Oriented Programming, pages 389-418, 1997.]]Google ScholarCross Ref
- DLNS98 David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Pale Alto, CA 94301, USA, December 1998.]]Google Scholar
- FA99a Cormac Flanagan and Martfn Abadi. Object types against races. In Proceedings of CONCUR, August 1999.]] Google ScholarDigital Library
- FA99b Cormac Flanagan and Martfn Abadi. Types for safe locking. In Proceedings of European Symposium on Programming, March 1999.]] Google ScholarDigital Library
- FKF98 Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In Prec. 25th A CM Symposium on Principles of Programming Languages, pages 171-183, January 1998.]] Google ScholarDigital Library
- GJS96 James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.]] Google ScholarDigital Library
- IPW99 Atsushi Igarishi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Proceedings of A CM Conference on Object Oriented Languages and Systems, November 1999.]] Google ScholarDigital Library
- Jav98 JavaSoft. Java Developers Kit, version 1.1. http://j ava. sun. corn, 1998.]]Google Scholar
- JG91 Pierre Jouvelot and David Gifford. Algebraic reconstruction of types and effects. In Proceedings of the 18th Symposium on Principles of Programming Languages, pages 303-310, 1991.]] Google ScholarDigital Library
- KM98 Thomas Kistler and Johannes Marais. WebL - a programming language for the web. Computer Networks and ISDN Systems, 30:259-270, April 1998.]] Google ScholarDigital Library
- LG88 John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Proceedings of the A CM Conference on Lisp and Functional Programming, pages 47-57, 1988.]] Google ScholarDigital Library
- LSS99 K. Rustan M. Leino, James B. Saxe, and Raymie Stata. Checking Java programs via guarded commands. Technical Report 1999-002, Compaq Systems Research Center, Palo Alto, CA, May 1999. Also appeared in Formal Techniques for Java Programs, workshop proceedings. Bart Jacobs, Gary T. Leavens, Peter Muller, and Arnd Poetzsch-Heffter, editors. Technical Report 251, Fernuniversitat Hagen, 1999.]]Google Scholar
- Nie96 Flemming Nielson. Annotated type and effect systems. A CM Computing Surveys, 28(2):344-345, 1996. Invited position statement for the Symposium on Models of Programming Languages and Computation.]] Google ScholarDigital Library
- NvO98 Tobias Nipkow and David von Oheimb. Javaligl, t is type-safe- definitely. In Prec. 25th A CM Symposium on Principles of Programming Languages, January 1998.]] Google ScholarDigital Library
- OW97 Martin Odersky and Philip Wadler. Pizza into Java: Translating theory into practice. In Prec. 24th A CM Symposium on Principles of Programming Languages, January 1997.]] Google ScholarDigital Library
- SBN+97 Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas E. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. A CM Transactions on Computer Systems, 15(4):391-411, 1997.]] Google ScholarDigital Library
- Ste93 Nicholas Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97-106, 1993.]]Google Scholar
- Sym97 Don Syme. Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory Technical Report, 1997.]]Google Scholar
- TJ92 Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245-271, 1992.]]Google ScholarCross Ref
- TT94 Mads ToRe and Jean-Pierre Talpin. Implementation of the typed call-by-value }ambda-calculus using a stack of regions. In Proceedings of the 21st Symposium on Principles of Programming Languages, pages 188-201, 1994.]] Google ScholarDigital Library
- TT97 Mads ToRe and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109-176, 1997.]] Google ScholarDigital Library
- WR99 John Whaley and Martin Rinard. Compositional pointer and escape analysis for Java programs. In Proceedings of A CM Conference on Object Oriented Languages and Systems, November 1999.]] Google ScholarDigital Library
Index Terms
- Type-based race detection for Java
Recommendations
Type-based race detection for Java
PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementationThis paper presents a static race detection analysis for multithreaded Java programs. Our analysis is based on a formal type system that is capable of capturing many common synchronization patterns. These patterns include classes with internal ...
Aspect-Oriented Race Detection in Java
In the past, researchers have developed specialized programs to aid programmers in detecting concurrent programming errors such as deadlocks, livelocks, starvation, and data races. In this work, we propose a language extension to the aspect-oriented ...
Comments