AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
We have presented a type system for catching race conditions statically and described rccjava, an implementation of this system for Java

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

Cited by: 508|Views191
EI

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. Expe...More

Code:

Data:

Introduction
  • 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]
Highlights
  • 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
Results
  • 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
Conclusion
  • 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
Tables
  • Table1: Programs analyzed using rccjava
Download tables as Excel
Related work
  • 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.
Reference
  • 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 ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Alexander Aiken and David Gay. Barrier inference. In Proceedings of the 25th Symposium on Principles of Programming Languages, pages 243–354, 1998.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Jeff Bogda and Urs Holzle. Removing unnecessary synchronization in Java. In Proceedings of ACM Conference on Object Oriented Languages and Systems, November 1999.
    Google ScholarLocate open access versionFindings
  • Andrew D. Birrell. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center, 1989.
    Google ScholarLocate open access versionFindings
  • 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 ScholarLocate open access versionFindings
  • J. Bank, B. Liskov, and A. Myers. Parameterized Types and Java. Technical Report MIT/LCS/TM553, Massachussetts Institute of Technology, 1996.
    Google ScholarFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • Luca Cardelli. Mobile ambient synchronization. Technical Report 1997-013, Digital Systems Research Center, Palo Alto, CA, July 1997.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • S. Drossopoulou and S. Eisenbach. Java is type safe — probably. In European Conference On Object Oriented Programming, pages 389–418, 1997.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • Cormac Flanagan and Martın Abadi. Object types against races. In Proceedings of CONCUR, August 1999.
    Google ScholarLocate open access versionFindings
  • Cormac Flanagan and Martın Abadi. Types for safe locking. In Proceedings of European Symposium on Programming, March 1999.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • [GJS96] James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • JavaSoft. Java Developers Kit, version 1.1. http://java.sun.com, 1998.
    Findings
  • 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 ScholarLocate open access versionFindings
  • Thomas Kistler and Johannes Marais. WebL – a programming language for the web. Computer Networks and ISDN Systems, 30:259–270, April 1998.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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 ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Martin Odersky and Philip Wadler. Pizza into Java: Translating theory into practice. In Proc. 24th ACM Symposium on Principles of Programming Languages, January 1997.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Nicholas Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97–106, 1993.
    Google ScholarLocate open access versionFindings
  • Don Syme. Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory Technical Report, 1997.
    Google ScholarFindings
  • Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, 1992.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科