AI helps you reading Science
AI generates interpretation videos
AI extracts and analyses the key points of the paper to generate videos automatically
AI parses the academic lineage of this thesis
AI extracts a summary of this paper
Type-based race detection for Java
PLDI '02 Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implement..., no. 5 (2000): 219-232
- Insidious errors in multithreaded programs. A race condition occurs when two threads manipulate a shared data structure simultaneously, without synchronization.
- Race conditions often result in unexpected program behavior, such as program crashes or incorrect results.
- They can be avoided by careful programming discipline: protecting each data structure with a lock and acquiring that lock before manipulating the data structure [Bir89].
- It is easy to write a program that, by mistake, neglects to perform certain crucial synchronization operations
- These synchronization errors are not detected by traditional compile-time checks.
- A single synchronization error in an otherwise correct program may yield a race condition whose cause may take weeks to identify [SBN+97]
- Race conditions are common, insidious errors in multithreaded programs
- Race conditions often result in unexpected program behavior, such as program crashes or incorrect results
- This paper investigates a static analysis system for detecting race conditions in Java programs
- Rccjava was run with the command line flags “-no warn thread local override” and “-constructor holds lock” for these tests. These flags may cause rccjava to miss some potential races, they significantly reduce the number of false alarms reported and provide the most effective way to deal with existing programs that were not written with this type system in mind
- It shows the number of annotations and time required to annotate each program, as well as the number of race conditions found in each program
- We have presented a type system for catching race conditions statically and described rccjava, an implementation of this system for Java
- To test the effectiveness of rccjava as a static race detection tool, the authors used it to check several multithreaded Java programs.
- The authors' test cases include two representative single classes, java.util.Hashtable and java.util.Vector, and several large programs, including java.io, the Java input/output package [Jav98]; Ambit, an implementation of a mobile object calculus [Car97]; and an interpreter and run-time environment for WebL, a language for automating webbased tasks [KM98]
- These five programs use a variety of synchronization patterns, most of which were captured with rccjava annotations.
- The time includes both the time spent by the programmer inserting annotations and the time to run the tool
- Race conditions are difficult to catch using traditional testing techniques.
- They persist even in common, relatively mature Java programs.
- The authors have presented a type system for catching race conditions statically and described rccjava, an implementation of this system for Java.
- Because the type system is modular, it enables race conditions to be detected early in the development cycle, before the entire program has been written.
- The type system does require the programmer to write additional type annotations, but these annotations function as documentation of the locking strategies used by the program
- Table1: Programs analyzed using rccjava
- A number of tools have been developed for detecting race conditions, both statically and dynamically. Warlock [Ste93] is a static race detection system for ANSI C programs. It supports the lock-based synchronization discipline through annotations similar to ours. However, Warlock uses a different analysis mechanism; it works by tracing execution paths through the program, but it fails to trace paths through loops or recursive function calls, and thus may not detect certain races. In addition, Warlock assumes, but does not verify, the thread-local annotations introduced by the programmer. However, these soundness issues have not prevented Warlock from being a practical tool. It has been used to catch races in several programs, including an X-windows library.
- 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.
- Ole Agesen, Stephen N. Freund, and John C. Mitchell. Adding type parameterization to the Java language. In Proceedings of ACM Conference on Object Oriented Languages and Systems, October 1997.
- Alexander Aiken and David Gay. Barrier inference. In Proceedings of the 25th Symposium on Principles of Programming Languages, pages 243–354, 1998.
- Torben Amtoft, Flemming Nielson, and Hanne Riis Nielson. Type and behaviour reconstruction for higher-order concurrent programs. Journal of Functional Programming, 7(3):321–347, 1997.
- Jeff Bogda and Urs Holzle. Removing unnecessary synchronization in Java. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.
- Andrew D. Birrell. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center, 1989.
- Bruno Blanchet. Escape analysis for object-oriented languages. Application to Java. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.
- J. Bank, B. Liskov, and A. Myers. Parameterized Types and Java. Technical Report MIT/LCS/TM553, Massachussetts Institute of Technology, 1996.
- [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 ACM Conference on Object Oriented Languages and Systems, October 1998.
- Luca Cardelli. Mobile ambient synchronization. Technical Report 1997-013, Digital Systems Research Center, Palo Alto, CA, July 1997.
- J.D. Choi, M. Gupta, M. Serrano, V.C. Sreedhar, and S. Midkiff. Escape analysis for Java. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.
- Robert Cartwright and Guy L. Steele Jr. Compatible genericity with run-time types for the Java programming language. In Proceedings of ACM Conference on Object Oriented Languages and Systems, October 1998.
- S. Drossopoulou and S. Eisenbach. Java is type safe — probably. In European Conference On Object Oriented Programming, pages 389–418, 1997.
- 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., Palo Alto, CA 94301, USA, December 1998.
- Cormac Flanagan and Martın Abadi. Object types against races. In Proceedings of CONCUR, August 1999.
- Cormac Flanagan and Martın Abadi. Types for safe locking. In Proceedings of European Symposium on Programming, March 1999.
- Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In Proc. 25th ACM Symposium on Principles of Programming Languages, pages 171–183, January 1998.
- [GJS96] James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.
- Atsushi Igarishi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.
- JavaSoft. Java Developers Kit, version 1.1. http://java.sun.com, 1998.
- 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.
- Thomas Kistler and Johannes Marais. WebL – a programming language for the web. Computer Networks and ISDN Systems, 30:259–270, April 1998.
- John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 47–57, 1988.
- 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.
- Flemming Nielson. Annotated type and effect systems. ACM Computing Surveys, 28(2):344–345, 1996. Invited position statement for the Symposium on Models of Programming Languages and Computation.
- Martin Odersky and Philip Wadler. Pizza into Java: Translating theory into practice. In Proc. 24th ACM Symposium on Principles of Programming Languages, January 1997.
- Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas E. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems, 15(4):391–411, 1997.
- Nicholas Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97–106, 1993.
- Don Syme. Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory Technical Report, 1997.
- Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, 1992.
- Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value lambda-calculus using a stack of regions. In Proceedings of the 21st Symposium on Principles of Programming Languages, pages 188–201, 1994.
- Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.
- John Whaley and Martin Rinard. Compositional pointer and escape analysis for Java programs. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.