Martin Abadi
Cormac Flanagan
Skip Abstract Section
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.
- Agesen, O., Freund, S. N., and Mitchell, J. C. 1997. Adding type parameterization to the Java language. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 49--65.]] Google Scholar
Digital Library
- Aiken, A. and Gay, D. 1998. Barrier inference. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 243--354.]] Google ScholarDigital Library
- Aldrich, J., Chambers, C., Sirer, E. G., and Eggers, S. 1999. Static analyses for eliminating unnecessary synchronization from Java programs. In Proceedings of the Static Analysis Symposium, A. Cortesi and G. Filé, Eds. Lecture Notes in Computer Science, vol. 1694. Springer-Verlag, 19--38.]] Google ScholarDigital Library
- Amtoft, T., Nielson, F., and Nielson, H. R. 1997. Type and behaviour reconstruction for higher-order concurrent programs. J. Functional Prog. 7, 3, 321--347.]] Google ScholarDigital Library
- Bacon, D. F., Strom, R. E., and Tarafdar, A. 2001. Guava: A dialect of Java without data races. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 382--400.]] Google ScholarDigital Library
- Birrell, A. D. 1989. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center.]]Google Scholar
- Blanchet, B. 1999. Escape analysis for object-oriented languages. Application to Java. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 20--34.]] Google ScholarDigital Library
- Bogda, J. and Hölzle, U. 1999. Removing unnecessary synchronization in Java. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 35--46.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Boyapati, C. and Rinard, M. 2001. A parameterized type system for race-free Java programs. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 56--69.]] Google ScholarDigital Library
- Bracha, G., Odersky, M., Stoutamire, D., and Wadler, P. 1998. Making the future safe for the past: Adding genericity to the Java programming language. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 183--200.]] Google ScholarDigital Library
- Cardelli, L. 1988. Typechecking dependent types and subtypes. In Lecture Notes in Computer Science on Foundations of Logic and Functional Programming. Springer-Verlag, New York, Inc., 45--57.]] Google ScholarDigital Library
- Cardelli, L. 1997. Mobile ambient synchronization. Tech. Rep. 1997-013, Digital Systems Research Center, Palo Alto, CA.]]Google Scholar
- Cartwright, R. and Steele Jr., G. L. 1998. Compatible genericity with run-time types for the Java programming language. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 201--215.]] Google ScholarDigital Library
- Chamillard, A. T., Clarke, L. A., and Avrunin, G. S. 1996. An empirical comparison of static concurrency analysis techniques. Tech. Rep. 96-084, Department of Computer Science, University of Massachusetts at Amherst.]] Google ScholarDigital Library
- Choi, J.-D., Gupta, M., Serrano, M. J., Sreedhar, V. C., and Midkiff, S. P. 1999. Escape analysis for Java. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 1--19.]] Google ScholarDigital Library
- Choi, J.-D., Lee, K., Loginov, A., O'Callahan, R., Sarkar, V., and Sridhara, M. 2002. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 258--269.]] Google ScholarDigital Library
- Corbett, J. C. 1996. Evaluating deadlock detection methods for concurrent software. IEEE Trans. Softw. Eng. 22, 3, 161--180.]] Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 238--252.]] Google ScholarDigital Library
- DeLine, R. and Fähndrich, M. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 59--69.]] Google ScholarDigital Library
- Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998. Extended static checking. Research Report 159, Compaq Systems Research Center.]]Google Scholar
- Drossopoulou, S. and Eisenbach, S. 1997. Java is type safe---Probably. In European Conference On Object Oriented Programming. 389--418.]]Google Scholar
- Dwyer, M. B. and Clarke, L. A. 1994. Data flow analysis for verifying properties of concurrent programs. Tech. Rep. 94-045, Department of Computer Science, University of Massachusetts at Amherst.]] Google ScholarDigital Library
- Fajstrup, L., Goubault, E., and Raussen, M. 1998. Detecting deadlocks in concurrent systems. In Proceedings of the International Conference on Concurrency Theory, D. Sangiorgi and R. de Simone, Eds. Lecture Notes in Computer Science, vol. 1466. Springer-Verlag, 332--347.]] Google ScholarDigital Library
- Flanagan, C. and Abadi, M. 1999a. Object types against races. In Proceedings of the International Conference on Concurrency Theory, J. C. M. Baeten and S. Mauw, Eds. Lecture Notes in Computer Science, vol. 1664. Springer-Verlag, 288--303.]] Google ScholarDigital Library
- Flanagan, C. and Abadi, M. 1999b. Types for safe locking. In Proceedings of the European Symposium on Programming, S. D. Swierstra, Ed. Lecture Notes in Computer Science, vol. 1576. Springer-Verlag, 91--108.]] Google ScholarDigital Library
- Flanagan, C. and Freund, S. N. 2000. Type-based race detection for Java. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 219--232.]] Google ScholarDigital Library
- Flanagan, C. and Freund, S. N. 2001. Detecting race conditions in large programs. In Proceedings of the ACM Workshop on Program Analysis for Software Tools and Engineering. 90--96.]] Google ScholarDigital Library
- Flanagan, C. and Freund, S. N. 2004. Type inference against races. In Proceedings of the Static Analysis Symposium. 116--132.]]Google Scholar
- Flanagan, C., Freund, S. N., and Qadeer, S. 2004. Exploiting purity for atomicity. In Proceedings of the ACM International Symposium on Software Testing and Analysis. 221--231.]] Google ScholarDigital Library
- Flanagan, C., Joshi, R., and Leino, K. R. M. 2001. Annotation inference for modular checkers. Information Processing Letters 77, 2--4, 91--108.]] Google ScholarDigital Library
- Flanagan, C. and Leino, K. R. M. 2001. Houdini, an annotation assistant for ESC/Java. In Formal Methods Europe, J. N. Oliveira and P. Zave, Eds. Lecture Notes in Computer Science, vol. 2021. Springer-Verlag, 500--517.]] Google ScholarDigital Library
- Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for Java. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 234--245.]] Google ScholarDigital Library
- Flanagan, C. and Qadeer, S. 2003a. A type and effect system for atomicity. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 338--349.]] Google ScholarDigital Library
- Flanagan, C. and Qadeer, S. 2003b. Types for atomicity. In Proceedings of the ACM Workshop on Types in Language Design and Implementation. 1--12.]] Google ScholarDigital Library
- Flatt, M., Krishnamurthi, S., and Felleisen, M. 1998. Classes and mixins. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 171--183.]] Google ScholarDigital Library
- Gosling, J., Joy, B., and Steele, G. 1996. The Java Language Specification. Addison-Wesley.]] Google ScholarDigital Library
- Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the IEEE Conference on Computer Aided Verification. 72--83.]] Google ScholarDigital Library
- Grossman, D. 2003. Type-safe multithreading in Cyclone. In Proceedings of the ACM Workshop on Types in Language Design and Implementation. 13--25.]] Google ScholarDigital Library
- Igarashi, A., Pierce, B., and Wadler, P. 2001. Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Prog. Lang. Syst. 23, 3, 396--450.]] Google ScholarDigital Library
- JavaSoft. 1998. Java Developers Kit, version 1.1. available from http://java.sun.com.]]Google Scholar
- JavaSoft. 2004. Java Developer's Kit, version 1.5. available from http://java.sun.com.]]Google Scholar
- Jouvelot, P. and Gifford, D. 1991. Algebraic reconstruction of types and effects. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 303--310.]] Google ScholarDigital Library
- Kistler, T. and Marais, J. 1998. WebL---A programming language for the web. In Proceedings of the International World Wide Web Conference. Computer Networks and ISDN Systems, vol. 30. Elsevier, 259--270.]] Google ScholarDigital Library
- Kobayashi, N. 1998. A partially deadlock-free typed process calculus. ACM Trans. Prog. Lang. Syst. 20, 2, 436--482.]] Google ScholarDigital Library
- Kobayashi, N., Saito, S., and Sumii, E. 2000. An implicitly-typed deadlock-free process calculus. In Proceedings of the International Conference on Concurrency Theory, C. Palamidessi, Ed. Lecture Notes in Computer Science, vol. 1877. Springer-Verlag, 489--503.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Lucassen, J. M. and Gifford, D. K. 1988. Polymorphic effect systems. In Proceedings of the ACM Conference on Lisp and Functional Programming. 47--57.]] Google ScholarDigital Library
- Myers, A. C., Bank, J. A., and Liskov, B. 1997. Parameterized types and Java. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 132--145.]] Google ScholarDigital Library
- Nielson, F. 1996. Annotated type and effect systems. ACM Comput. Surv. 28, 2, 344--345. Invited position statement for the Symposium on Models of Programming Languages and Computation.]] Google ScholarDigital Library
- Nipkow, T. and von Oheimb, D. 1998. Javalight is type-safe---definitely. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 161--170.]] Google ScholarDigital Library
- Odersky, M. and Wadler, P. 1997. Pizza into Java: Translating theory into practice. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 146--159.]] Google ScholarDigital Library
- Salcianu, A. and Rinard, M. 2001. Pointer and escape analysis for multithreaded programs. In Proceedings of the Symposium on Principles and Practice of Parallel Programming. 12--23.]] Google ScholarDigital Library
- Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., and Anderson, T. E. 1997. Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems 15, 4, 391--411.]] Google ScholarDigital Library
- Schmidt, D. C. and Harrison, T. H. 1997. Double-checked locking---A optimization pattern for efficiently initializing and accessing thread-safe objects. In Pattern Languages of Program Design 3, R. Martin, F. Buschmann, and D. Riehle, Eds. Addison-Wesley.]] Google ScholarDigital Library
- Standard Performance Evaluation Corporation. 2000. SPEC JBB2000. Available from http://www.spec.org/osg/jbb2000/.]]Google Scholar
- Sterling, N. 1993. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference. 97--106.]]Google Scholar
- Syme, D. 1997. Proving Java type soundness. Tech. Rep. 427, University of Cambridge Computer Laboratory Technical Report.]]Google Scholar
- Talpin, J.-P. and Jouvelot, P. 1992. Polymorphic type, region and effect inference. J. Funct. Prog. 2, 3, 245--271.]]Google ScholarCross Ref
- Tofte, M. and Talpin, J.-P. 1994. Implementation of the typed call-by-value lambda-calculus using a stack of regions. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 188--201.]] Google ScholarDigital Library
- Tofte, M. and Talpin, J.-P. 1997. Region-based memory management. Information and Computation 132, 2, 109--176.]] Google ScholarDigital Library
- von Praun, C. and Gross, T. 2001. Object race detection. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 70--82.]] Google ScholarDigital Library
- Whaley, J. and Rinard, M. 1999. Compositional pointer and escape analysis for Java programs. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 187--206.]] Google ScholarDigital Library
- World Wide Web Consortium. 2001. Jigsaw. Available from http://www.w3c.org.]]Google Scholar
- Yahav, E. 2001. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 27--40.]] Google ScholarDigital Library
- Yu, Y., Manolios, P., and Lamport, L. 1999. Model checking TLA+ specifications. In Correct Hardware Design and Verification Methods, L. Pierre and T. Kropf, Eds. Lecture Notes in Computer Science, vol. 1703. Springer-Verlag, 54--66.]] Google ScholarDigital Library
Index Terms
- Types for safe locking: Static race detection for Java
Recommendations
Types for atomicity: Static checking and inference for Java
Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads. Atomic ...
Automated type-based analysis of data races and atomicity
PPoPP '05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programmingConcurrent programs are notorious for containing errors that are difficult to reproduce and diagnose at run-time. This motivated the development of type systems that statically ensure the absence of some common kinds of concurrent programming errors ...
Types for Safe Locking
ESOP '99: Proceedings of the 8th European Symposium on Programming Languages and SystemsA race condition is a situation where two threads manipulate a data structure simultaneously, without synchronization. Race conditions are common errors in multithreaded programming. They often lead to unintended nondeterminism and wrong results. ...
Comments