[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
article
Open access

Types for safe locking: Static race detection for Java

Published: 01 March 2006 Publication History

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]
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.]]
[2]
Aiken, A. and Gay, D. 1998. Barrier inference. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 243--354.]]
[3]
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.]]
[4]
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.]]
[5]
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.]]
[6]
Birrell, A. D. 1989. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center.]]
[7]
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.]]
[8]
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.]]
[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]
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.]]
[11]
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.]]
[12]
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.]]
[13]
Cardelli, L. 1997. Mobile ambient synchronization. Tech. Rep. 1997-013, Digital Systems Research Center, Palo Alto, CA.]]
[14]
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.]]
[15]
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.]]
[16]
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.]]
[17]
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.]]
[18]
Corbett, J. C. 1996. Evaluating deadlock detection methods for concurrent software. IEEE Trans. Softw. Eng. 22, 3, 161--180.]]
[19]
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.]]
[20]
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.]]
[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]
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.]]
[24]
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.]]
[25]
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.]]
[26]
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.]]
[27]
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.]]
[28]
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.]]
[29]
Flanagan, C. and Freund, S. N. 2004. Type inference against races. In Proceedings of the Static Analysis Symposium. 116--132.]]
[30]
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.]]
[31]
Flanagan, C., Joshi, R., and Leino, K. R. M. 2001. Annotation inference for modular checkers. Information Processing Letters 77, 2--4, 91--108.]]
[32]
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.]]
[33]
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.]]
[34]
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.]]
[35]
Flanagan, C. and Qadeer, S. 2003b. Types for atomicity. In Proceedings of the ACM Workshop on Types in Language Design and Implementation. 1--12.]]
[36]
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.]]
[37]
Gosling, J., Joy, B., and Steele, G. 1996. The Java Language Specification. Addison-Wesley.]]
[38]
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.]]
[39]
Grossman, D. 2003. Type-safe multithreading in Cyclone. In Proceedings of the ACM Workshop on Types in Language Design and Implementation. 13--25.]]
[40]
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.]]
[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]
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.]]
[44]
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.]]
[45]
Kobayashi, N. 1998. A partially deadlock-free typed process calculus. ACM Trans. Prog. Lang. Syst. 20, 2, 436--482.]]
[46]
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.]]
[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]
Lucassen, J. M. and Gifford, D. K. 1988. Polymorphic effect systems. In Proceedings of the ACM Conference on Lisp and Functional Programming. 47--57.]]
[49]
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.]]
[50]
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.]]
[51]
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.]]
[52]
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.]]
[53]
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.]]
[54]
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.]]
[55]
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.]]
[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]
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.]]
[61]
Tofte, M. and Talpin, J.-P. 1997. Region-based memory management. Information and Computation 132, 2, 109--176.]]
[62]
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.]]
[63]
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.]]
[64]
World Wide Web Consortium. 2001. Jigsaw. Available from http://www.w3c.org.]]
[65]
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.]]
[66]
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.]]

Cited By

View all
  • (2023)Quantitative Inhabitation for Different Lambda Calculi in a Unifying FrameworkProceedings of the ACM on Programming Languages10.1145/35712447:POPL(1483-1513)Online publication date: 11-Jan-2023
  • (2023)Stratified Commutativity in Verification Algorithms for Concurrent ProgramsProceedings of the ACM on Programming Languages10.1145/35712427:POPL(1426-1453)Online publication date: 11-Jan-2023
  • (2023)Recursive Subtyping for AllProceedings of the ACM on Programming Languages10.1145/35712417:POPL(1396-1425)Online publication date: 11-Jan-2023
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 28, Issue 2
March 2006
182 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/1119479
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 2006
Published in TOPLAS Volume 28, Issue 2

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Concurrent programs
  2. race conditions
  3. type inference
  4. type system

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)105
  • Downloads (Last 6 weeks)14
Reflects downloads up to 11 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2023)Quantitative Inhabitation for Different Lambda Calculi in a Unifying FrameworkProceedings of the ACM on Programming Languages10.1145/35712447:POPL(1483-1513)Online publication date: 11-Jan-2023
  • (2023)Stratified Commutativity in Verification Algorithms for Concurrent ProgramsProceedings of the ACM on Programming Languages10.1145/35712427:POPL(1426-1453)Online publication date: 11-Jan-2023
  • (2023)Recursive Subtyping for AllProceedings of the ACM on Programming Languages10.1145/35712417:POPL(1396-1425)Online publication date: 11-Jan-2023
  • (2023)Dargent: A Silver Bullet for Verified Data Layout RefinementProceedings of the ACM on Programming Languages10.1145/35712407:POPL(1369-1395)Online publication date: 11-Jan-2023
  • (2023)Dynamic Race Detection with O(1) SamplesProceedings of the ACM on Programming Languages10.1145/35712387:POPL(1308-1337)Online publication date: 11-Jan-2023
  • (2023)From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection ProblemsProceedings of the ACM on Programming Languages10.1145/35712007:POPL(185-217)Online publication date: 11-Jan-2023
  • (2023)Pluggable Type Inference for FreeProceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE56229.2023.00186(1542-1554)Online publication date: 11-Nov-2023
  • (2023)Fahrzeugarchitektur und InfrastrukturSoftware im Automobil10.1007/978-3-662-67156-6_1(1-49)Online publication date: 13-Jun-2023
  • (2023)Error Localization for Sequential Effect SystemsStatic Analysis10.1007/978-3-031-44245-2_16(343-370)Online publication date: 24-Oct-2023
  • (2022)Cache Abstraction for Data Race Detection in Heterogeneous Systems with Non-coherent AcceleratorsACM Transactions on Embedded Computing Systems10.1145/353545722:1(1-25)Online publication date: 13-Dec-2022
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media