Types for safe locking: Static race detection for Java

ABSTRACT

This article presents a static race-detection analysis for multithreaded shared-memory programs, focusing on the Java programming language. The analysis is based on a type system that captures many common synchronization patterns. It supports classes with internal synchronization, classes that require client-side synchronization, and thread-local classes. In order to demonstrate the effectiveness of the type system, we have implemented it in a checker and applied it to over 40,000 lines of hand-annotated Java code. We found a number of race conditions in the standard Java libraries and other test programs. The checker required fewer than 20 additional type annotations per 1,000 lines of code. This article also describes two improvements that facilitate checking much larger programs: an algorithm for annotation inference and a user interface that clarifies warnings generated by the checker. These extensions have enabled us to use the checker for identifying race conditions in large-scale software systems with up to 500,000 lines of code.

REFERENCES

• 1: Ole Agesen , Stephen N. Freund , John C. Mitchell, Adding type parameterization to the Java language, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.49-65, October 05-09, 1997, Atlanta, Georgia, United States
• 2: Alexander Aiken , David Gay, Barrier inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.342-354, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268974]
• 3: 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
• 4: 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]
• 5: David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
• 6: Birrell, A. D. 1989. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center.
• 7: 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
• 8: 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
• 9: Boyapati, C., Lee, R., and Rinard, M. 2002. A type system for preventing data races and deadlocks in Java programs. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 211--230.
• 10: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 11: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• 12: L. Cardelli, Typechecking dependent types and subtypes, Lecture notes in computer science on Foundations of logic and functional programming, p.45-57, June 1988, Trento, Italy
• 13: Cardelli, L. 1997. Mobile ambient synchronization. Tech. Rep. 1997-013, Digital Systems Research Center, Palo Alto, CA.
• 14: Robert Cartwright , Guy L. Steele, Jr., Compatible genericity with run-time types for the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.201-215, October 18-22, 1998, Vancouver, British Columbia, Canada
• 15: A. T. Chamillard , L. A. Clarke , G. S. Avrunin, Experimental Design for Comparing Static Concurrency Analysis, University of Massachusetts, Amherst, MA, 1996
• 16: 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
• 17: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 18: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 19: 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]
• 20: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 21: Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998. Extended static checking. Research Report 159, Compaq Systems Research Center.
• 22: Drossopoulou, S. and Eisenbach, S. 1997. Java is type safe---Probably. In European Conference On Object Oriented Programming. 389--418.
• 23: Matthew B. Dwyer , Lori A. Clarke, Data Flow Analysis for Verifying Properties of Concurrent Programs, University of Massachusetts, Amherst, MA, 1994
• 24: Lisbeth Fajstrup , Eric Goubault , Martin Raußen, Detecting Deadlocks in Concurrent Systems, Proceedings of the 9th International Conference on Concurrency Theory, p.332-347, September 08-11, 1998
• 25: Cormac Flanagan , Martín Abadi, Object Types against Races, Proceedings of the 10th International Conference on Concurrency Theory, p.288-303, August 24-27, 1999
• 26: 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
• 27: 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
• 28: Cormac Flanagan , Stephen N. Freund, Detecting race conditions in large programs, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.90-96, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379687]
• 29: Flanagan, C. and Freund, S. N. 2004. Type inference against races. In Proceedings of the Static Analysis Symposium. 116--132.
• 30: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting purity for atomicity, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 31: 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]
• 32: 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
• 33: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 34: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 35: Cormac Flanagan , Shaz Qadeer, Types for atomicity, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 36: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268961]
• 37: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 38: 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
• 39: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 40: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 41: JavaSoft. 1998. Java Developers Kit, version 1.1. available from http://java.sun.com.
• 42: JavaSoft. 2004. Java Developer's Kit, version 1.5. available from http://java.sun.com.
• 43: 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]
• 44: Thomas Kistler , Hannes Marais, WebL - a programming language for the Web, Proceedings of the seventh international conference on World Wide Web 7, p.259-270, April 1998, Brisbane, Australia
• 45: Naoki Kobayashi, A partially deadlock-free typed process calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.2, p.436-482, March 1998 [doi>10.1145/276393.278524]
• 46: Naoki Kobayashi , Shin Saito , Eijiro Sumii, An Implicitly-Typed Deadlock-Free Process Calculus, Proceedings of the 11th International Conference on Concurrency Theory, p.489-503, August 22-25, 2000
• 47: Leino, K. R. M., Saxe, J. B., and Stata, R. 1999. Checking Java programs via guarded commands. Tech. Rep. 1999-002, Compaq Systems Research Center, Palo Alto, CA.
• 48: 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]
• 49: Joseph A. Bank , Andrew C. Myers , Barbara Liskov, Parameterized types for Java, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.132-145, January 15-17, 1997, Paris, France [doi>10.1145/263699.263714]
• 50: 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]
• 51: Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
• 52: Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
• 53: Alexandru Salcianu , Martin Rinard, Pointer and escape analysis for multithreaded programs, Proceedings of the eighth ACM SIGPLAN symposium on Principles and practices of parallel programming, p.12-23, June 2001, Snowbird, Utah, United States
• 54: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 55: Douglas C. Schmidt , Tim Harrison, Double-checked locking, Pattern languages of program design 3, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1997
• 56: Standard Performance Evaluation Corporation. 2000. SPEC JBB2000. Available from http://www.spec.org/osg/jbb2000/.
• 57: Sterling, N. 1993. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference. 97--106.
• 58: Syme, D. 1997. Proving Java type soundness. Tech. Rep. 427, University of Cambridge Computer Laboratory Technical Report.
• 59: Talpin, J.-P. and Jouvelot, P. 1992. Polymorphic type, region and effect inference. J. Funct. Prog. 2, 3, 245--271.
• 60: 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]
• 61: 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]
• 62: Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
• 63: 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
• 64: World Wide Web Consortium. 2001. Jigsaw. Available from http://www.w3c.org.
• 65: Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-40, January 2001, London, United Kingdom
• 66: 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.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics

General Terms:
Languages, Reliability, Verification

Keywords:
Concurrent programs, race conditions, type inference, type system