article

Open access

Types for safe locking: Static race detection for Java

Authors:

Cormac Flanagan,

Stephen N. FreundAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 28, Issue 2

Pages 207 - 255

https://doi.org/10.1145/1119479.1119480

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.]]

Digital Library

[2]

Aiken, A. and Gay, D. 1998. Barrier inference. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 243--354.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[18]

Corbett, J. C. 1996. Evaluating deadlock detection methods for concurrent software. IEEE Trans. Softw. Eng. 22, 3, 161--180.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[31]

Flanagan, C., Joshi, R., and Leino, K. R. M. 2001. Annotation inference for modular checkers. Information Processing Letters 77, 2--4, 91--108.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[37]

Gosling, J., Joy, B., and Steele, G. 1996. The Java Language Specification. Addison-Wesley.]]

Digital Library

[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.]]

Digital Library

[39]

Grossman, D. 2003. Type-safe multithreading in Cyclone. In Proceedings of the ACM Workshop on Types in Language Design and Implementation. 13--25.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[45]

Kobayashi, N. 1998. A partially deadlock-free typed process calculus. ACM Trans. Prog. Lang. Syst. 20, 2, 436--482.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[61]

Tofte, M. and Talpin, J.-P. 1997. Region-based memory management. Information and Computation 132, 2, 109--176.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

Cited By

Arrial VGuerrieri GKesner D(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
https://dl.acm.org/doi/10.1145/3571244
Farzan AKlumpp DPodelski A(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
https://dl.acm.org/doi/10.1145/3571242
Zhou LZhou YOliveira B(2023)Recursive Subtyping for AllProceedings of the ACM on Programming Languages10.1145/35712417:POPL(1396-1425)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571241
Show More Cited By

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 programming

Concurrent 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 Systems

A 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

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

Copyright © 2006 ACM.

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.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

197
Total Citations
View Citations
1,401
Total Downloads

Downloads (Last 12 months)87
Downloads (Last 6 weeks)17

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Arrial VGuerrieri GKesner D(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
https://dl.acm.org/doi/10.1145/3571244
Farzan AKlumpp DPodelski A(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
https://dl.acm.org/doi/10.1145/3571242
Zhou LZhou YOliveira B(2023)Recursive Subtyping for AllProceedings of the ACM on Programming Languages10.1145/35712417:POPL(1396-1425)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571241
Chen ZLafont AO'Connor LKeller GMcLaughlin CJackson VRizkallah C(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
https://dl.acm.org/doi/10.1145/3571240
Thokair MZhang MMathur UViswanathan M(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
https://dl.acm.org/doi/10.1145/3571238
Bembenek AGreenberg MChong S(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
https://dl.acm.org/doi/10.1145/3571200
Kellogg MDaskiewicz DNgo LNguyen DAhmed MErnst MBissyandé TKlein JBird CSarro F(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
https://dl.acm.org/doi/10.1109/ASE56229.2023.00186
Wolf F(2023)Fahrzeugarchitektur und InfrastrukturSoftware im Automobil10.1007/978-3-662-67156-6_1(1-49)Online publication date: 13-Jun-2023
https://doi.org/10.1007/978-3-662-67156-6_1
Gordon CYun C(2023)Error Localization for Sequential Effect SystemsStatic Analysis10.1007/978-3-031-44245-2_16(343-370)Online publication date: 24-Oct-2023
https://doi.org/10.1007/978-3-031-44245-2_16
Young MHu ALemieux G(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
https://dl.acm.org/doi/10.1145/3535457
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents