Detecting race conditions in large programs

ABSTRACT

The race condition checker \rcc{} statically identifies potential races in concurrent Java programs. This paper describes improvements to \rcc{} that enable it to be used on large, realistic programs. These improvements include not only extensions to the underlying analysis, but also an annotation inference algorithm and a user interface to help programmers understand warnings generated by the tool. Experience with programs containing up to 500,000 lines of code indicate that it is an effective tool for identifying races in large-scale software systems.

REFERENCES

• 1: Jonathan Aldrich , Craig Chambers , Emin Gün Sirer , Susan J. Eggers, Static Analyses for Eliminating Unnecessary Synchronization from Java Programs, Proceedings of the 6th International Symposium on Static Analysis, p.19-38, September 22-24, 1999
• 2: Torben Amtoft , Flemming Nielson , Hanne Riis Nielson, Type and behaviour reconstruction for higher-order concurrent programs, Journal of Functional Programming, v.7 n.3, p.321-347, May 1997 [doi>10.1017/S0956796897002700]
• 3: A. D. Birrell. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center, 1989.
• 4: Bruno Blanchet, Escape analysis for object-oriented languages: application to Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.20-34, November 01-05, 1999, Denver, Colorado, United States
• 5: Jeff Bogda , Urs Hölzle, Removing unnecessary synchronization in Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.35-46, November 01-05, 1999, Denver, Colorado, United States
• 6: L. Cardelli. Mobile ambient synchronization. Technical Report 1997-013, Digital Systems Research Center, Palo Alto, CA, July 1997.
• 7: Jong-Deok Choi , Manish Gupta , Mauricio Serrano , Vugranam C. Sreedhar , Sam Midkiff, Escape analysis for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-19, November 01-05, 1999, Denver, Colorado, United States
• 8: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 9: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 10: 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
• 11: Cormac Flanagan , Rajeev Joshi , K. Rustan M. Leino, Annotation inference for modular checkers, Information Processing Letters, v.77 n.2-4, p.97-108, Feb. 1, 2001 [doi>10.1016/S0020-0190(00)00196-4]
• 12: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 13: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 14: Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
• 15: Thomas Kistler , Hannes Marais, WebL - a programming language for the Web, Computer Networks and ISDN Systems, v.30 n.1-7, p.259-270, April 1, 1998
• 16: K. R. M. Leino, J. B. Saxe, and R. Stata. Checking Java programs via guarded commands. Technical Report 1999-002, Cornpaq 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.
• 17: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 18: Flemming Nielson, Annotated type and effect systems, ACM Computing Surveys (CSUR), v.28 n.2, p.344-345, June 1996 [doi>10.1145/234528.234745]
• 19: S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):97-106, 1976.
• 20: Standard Performance Evaluation Corporation. SPEC JBB2000. available from http://www.spec.org/osg/jbb2000/, June 2000.
• 21: N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97-106, 1993.
• 22: J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Fanctional Programming, 2(3):245 271, 1992.
• 23: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• 24: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 25: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 26: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States
• 27: World Wide Web Consortium. Jigsaw. available from http://www.w3c.org, January 2001.
• 28: J. Yang, G. Michaelson, P. Trinder, and J. B. Wells. Improved Type Error Reporting. In M. Mohnen and P. Koopman, editors, Proceedings of the 12th International Workshop on Irnplementation of Fanctional Languages, number AIB-00-7 in Aachener Informatik Berichte, pages 7186. RWTH Aachen, 2000.
• 29: Yuan Yu , Panagiotis Manolios , Leslie Lamport, Model Checking TLA+ Specifications, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.54-66, September 27-29, 1999

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Java

General Terms:
Algorithms, Languages