skip to main content
research-article
Open access

Types for atomicity: Static checking and inference for Java

Published: 01 August 2008 Publication History

Abstract

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 methods are amenable to sequential reasoning, which significantly facilitates subsequent analysis and verification.
This article presents a type system for specifying and verifying the atomicity of methods in multithreaded Java programs using a synthesis of Lipton's theory of reduction and type systems for race detection. The type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We also present an algorithm for verifying atomicity via type inference.
We have applied our type checker and type inference tools to a number of commonly used Java library classes and programs. These tools were able to verify the vast majority of methods in these benchmarks as atomic, indicating that atomicity is a widespread methodology for multithreaded programming. In addition, reported atomicity violations revealed some subtle errors in the synchronization disciplines of these programs.

Supplementary Material

Flanagan Appendix (a20-flanagan-apndx.pdf)
Online appendix to designing mediation for context-aware applications. The appendix supports the information on article 20.

References

[1]
Abadi, M., Flanagan, C., and Freund, S. N. 2006. Types for safe locking: Static race detection for Java. ACM Trans. Program. Lang. Syst. 28, 2, 207--255.]]
[2]
Agarwal, R. and Stoller, S. D. 2004. Type inference for parameterized race-free Java. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. 149--160.]]
[3]
Aiken, A. and Gay, D. 1998. Barrier inference. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 243--354.]]
[4]
Artho, C., Havelund, K., and Biere, A. 2003. High-level data races. In Proceedings of the First International Workshop on Verification and Validation of Enterprise Information Systems.]]
[5]
Back, R.-J. 1989. A method for refining atomicity in parallel algorithms. In Proceedings of the Parallel Architectures and Languages Europe (PARLE'89). Lecture Notes in Computer Science, vol. 366. Springer-Verlag, 199--216.]]
[6]
Birrell, A. D. 1989. An introduction to programming with threads. Res. rep. 35, Digital Equipment Corporation Systems Research Center.]]
[7]
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.]]
[8]
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.]]
[9]
Bruening, D. 1999. Systematic testing of multithreaded Java programs. M.S. thesis, Massachusetts Institute of Technology.]]
[10]
Bryant, R. 1986. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35, 8, 677--691.]]
[11]
Burrows, M. and Leino, K. R. M. 2002. Finding stale-value errors in concurrent programs. Technical Note 2002-004, Compaq Systems Research Center.]]
[12]
Cardelli, L. 1988. Typechecking dependent types and subtypes. Lecture Notes in Computer Science, Foundations of Logic and Functional Programming. 45--57.]]
[13]
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.]]
[14]
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.]]
[15]
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.]]
[16]
Cohen, E. and Lamport, L. 1998. Reduction in TLA. In Proceedings of the International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1466. Springer-Verlag, 317--331.]]
[17]
Corbett, J. C. 1996. Evaluating deadlock detection methods for concurrent software. IEEE Trans. Softw. Eng. 22, 3, 161--180.]]
[18]
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.]]
[19]
Deng, X., Dwyer, M., Hatcliff, J., and Mizuno, M. 2002. Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In Proceedings of the International Conference on Software Engineering. 442--452.]]
[20]
Detlefs, D. L., Leino, K. R. M., and Nelson, C. G. 1998. Wrestling with rep exposure. Research rep. 156, DEC Systems Research Center.]]
[21]
Doeppner, Jr., T. W. 1977. Parallel program correctness through refinement. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 155--169.]]
[22]
Eppinger, J. L., Mummert, L. B., and Spector, A. Z. 1991. Camelot and Avalon: A Distributed Transaction Facility. Morgan Kaufmann.]]
[23]
Flanagan, C. 2004. Verifying commit-atomicity using model-checking. In Proceedings of the International SPIN Workshop on Model Checking of Software.]]
[24]
Flanagan, C. and Abadi, M. 1999a. Object types against races. In Proceedings of the International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1664. 288--303.]]
[25]
Flanagan, C. and Abadi, M. 1999b. Types for safe locking. In Proceedings of European Symposium on Programming. Lecture Notes in Computer Science, vol. 1576. 91--108.]]
[26]
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.]]
[27]
Flanagan, C. and Freund, S. N. 2004a. Atomizer: A dynamic atomicity checker for multithreaded programs. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 256--267.]]
[28]
Flanagan, C. and Freund, S. N. 2004b. Type inference against races. In Proceedings of the Static Analysis Symposium. 116--132.]]
[29]
Flanagan, C. and Freund, S. N. 2005. Automatic synchronization correction. In Proceedings of the Workshop on Synchronization and Concurrency in Object-Oriented Languages.]]
[30]
Flanagan, C., Freund, S. N., and Lifshin, M. 2005. Type inference for atomicity. In Proceedings of the ACM Workshop on Types in Language Design and Implementation. 47--58.]]
[31]
Flanagan, C., Freund, S. N., and Qadeer, S. 2005. Exploiting purity for atomicity. IEEE Trans. Softw. Eng. 31, 4, 275--291.]]
[32]
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.]]
[33]
Flanagan, C. and Qadeer, S. 2003a. Transactions for software model checking. In Proceedings of the Workshop on Software Model Checking.]]
[34]
Flanagan, C. and Qadeer, S. 2003b. 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. 2003c. 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]
Freund, S. N. and Qadeer, S. 2004. Checking concise specifications for multithreaded software. J. Object Tech. 3, 6, 81--101.]]
[38]
Gharachorloo, K. 1995. Memory consistency models for shared-memory multiprocessors. Ph.D. thesis, Stanford University.]]
[39]
Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., and Lea, D. 2006. Java Concurrency in Practice. Addison-Wesley.]]
[40]
Gosling, J., Joy, B., and Steele, G. 1996. The Java Language Specification. Addison-Wesley.]]
[41]
Grossman, D. 2003. Type-safe multithreading in Cyclone. In Proceedings of the ACM Workshop on Types in Language Design and Implementation. 13--25.]]
[42]
Haack, C. and Wells, J. B. 2003. Type error slicing in implicitly typed higher-order languages. In Proceedings of the European Symposium on Programming. 284--301.]]
[43]
Harris, T. and Fraser, K. 2003. Language support for lightweight transactions. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 388--402.]]
[44]
Hatcliff, J., Robby, and Dwyer, M. B. 2004. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In Proceedings of the International Conference on Verification, Model Checking and Abstract Interpretation. 175--190.]]
[45]
Herlihy, M. P. and Wing, J. M. 1990. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 3, 463--492.]]
[46]
Hicks, M., Foster, J. S., and Pratikakis, P. 2006. Inferring locking for atomic sections. In Proceedings of the Workshop on Languages, Compilers, and Hardware Support for Transactional Computing.]]
[47]
Hoare, C. 1974. Monitors: an operating systems structuring concept. Comm. ACM 17, 10, 549--557.]]
[48]
Hoare, C. A. R. 1972. Towards a theory of parallel programming. In Operating Systems Techniques. A.P.I.C. Studies in Data Processing, vol. 9. 61--71.]]
[49]
Java Grande Forum. 2003. Java Grande benchmark suite. http://www.javagrande.org/.]]
[50]
JavaSoft. 2005. Java Developers Kit, version 1.4.0. http://java.sun.com.]]
[51]
Lamport, L. 1978. Time, clocks, and the ordering of events in a distributed system. Comm. ACM 21, 7, 558--565.]]
[52]
Lamport, L. and Schneider, F. B. 1989. Pretending atomicity. Research rep. 44, DEC Systems Research Center.]]
[53]
Lea, D. 2004. The util.concurrent package, release 1.3.4. http://gee.cs.oswego.edu/dl/.]]
[54]
Lipton, R. J. 1975. Reduction: A method of proving properties of parallel programs. Comm. ACM 18, 12, 717--721.]]
[55]
Liskov, B., Curtis, D., Johnson, P., and Scheifler, R. 1987. Implementation of Argus. In Proceedings of the Symposium on Operating Systems Principles. 111--122.]]
[56]
Lomet, D. B. 1977. Process structuring, synchronization, and recovery using atomic actions. Lang. Design Reliable Softw., 128--137.]]
[57]
Lucassen, J. M. and Gifford, D. K. 1988. Polymorphic effect systems. In Proceedings of the ACM Conference on Lisp and Functional Programming. 47--57.]]
[58]
Manson, J., Pugh, W., and Adve, S. V. 2005. The Java memory model. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 378--391.]]
[59]
McCloskey, B., Zhou, F., Gay, D., and Brewer, E. 2006. Autolocker: synchronization inference for atomic sections. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 346--358.]]
[60]
Misra, J. 2001. A Discipline of Multiprogramming: Programming Theory for Distributed Applications. Springer-Verlag.]]
[61]
Naik, M., Aiken, A., and Whaley, J. 2006. Effective static race detection for Java. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 308--319.]]
[62]
O'Callahan, R. and Choi, J.-D. 2003. Hybrid dynamic data race detection. In Proceedings of the ACM Symposium on Principles and Practice of Parallel Programming. 167--178.]]
[63]
Papadimitriou, C. 1986. The Theory of Database Concurrency Control. Computer Science Press.]]
[64]
Pozniansky, E. and Schuster, A. 2003. Efficient on-the-fly data race detection in multihreaded C++ programs. In Proceedings of the ACM Symposium on Principles and Practice of Parallel Programming. 179--190.]]
[65]
Pratikakis, P., Foster, J. S., and Hicks, M. 2006. Context-sensitive correlation analysis for detecting races. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 320--331.]]
[66]
Qadeer, S., Rajamani, S. K., and Rehof, J. 2004. Summarizing procedures in concurrent programs. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 245--255.]]
[67]
Ringenburg, M. F. and Grossman, D. 2005. AtomCaml: first-class atomicity via rollback. In Proceedings of the ACM International Conference on Functional Programming. 92--104.]]
[68]
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.]]
[69]
Sasturkar, A., Agarwal, R., Wang, L., and Stoller, S. D. 2005. Automated type-based analysis of data races and atomicity. In Proceedings of the ACM Symposium on Principles and Practice of Parallel Programming. 83--94.]]
[70]
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., and Anderson, T. E. 1997. Eraser: A dynamic data race detector for multi-threaded programs. ACM Trans. Comput. Syst. 15, 4, 391--411.]]
[71]
SPEC. 2000. Standard Performance Evaluation Corporation JBB2000 Benchmark. Available from http://www.spec.org/osg/jbb2000/.]]
[72]
Sterling, N. 1993. Warlock: A static data race analysis tool. In Proceedings of the USENIX Winter Technical Conference. 97--106.]]
[73]
Stoller, S. 2006. Personal communication.]]
[74]
Stoller, S. D. 2000. Model-checking multi-threaded distributed Java programs. In Proceedings of the Workshop on Model Checking and Software Verification. Lecture Notes in Computer Science, vol. 1885. Springer-Verlag, 224--244.]]
[75]
Talpin, J.-P. and Jouvelot, P. 1992. Polymorphic type, region and effect inference. J. Funct. Program. 2, 3, 245--271.]]
[76]
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.]]
[77]
Vaziri, M., Tip, F., and Dolby, J. 2006. Associating synchronization constraints with data in an object-oriented language. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 334--345.]]
[78]
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.]]
[79]
von Praun, C. and Gross, T. 2003. Static conflict analysis for multi-threaded object-oriented programs. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 115--128.]]
[80]
Wand, M. 1986. Finding the source of type errors. In Proceedings of the ACM Symposium on the Principles of Programming Languages. 38--43.]]
[81]
Wang, L. and Stoller, S. D. 2003. Runtime analysis for atomicity. In Proceedings of the Workshop on Runtime Verification.]]
[82]
Wang, L. and Stoller, S. D. 2006. Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Softw. Eng. 32, 2, 93--110.]]
[83]
Welc, A., Jagannathan, S., and Hosking, A. L. 2004. Transactional monitors for concurrent objects. In Proceedings of the European Conference on Object-Oriented Programming. 519--542.]]
[84]
Yang, J., Michaelson, G., Trinder, P., and Wells, J. B. 2000. Improved type error reporting. In Proceedings of the International Workshop on Implementation of Functional Languages. 71--86.]]

Cited By

View all
  • (2024)Predictive Monitoring against Pattern Regular LanguagesProceedings of the ACM on Programming Languages10.1145/36329158:POPL(2191-2225)Online publication date: 5-Jan-2024
  • (2023)Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-TriggeringProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616276(1153-1164)Online publication date: 30-Nov-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
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 30, Issue 4
July 2008
358 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/1377492
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 August 2008
Accepted: 01 April 2007
Revised: 01 April 2007
Received: 01 July 2006
Published in TOPLAS Volume 30, Issue 4

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Atomicity
  2. concurrent programs
  3. type inference
  4. type systems

Qualifiers

  • Research-article
  • Research
  • Refereed

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)160
  • Downloads (Last 6 weeks)22
Reflects downloads up to 23 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Predictive Monitoring against Pattern Regular LanguagesProceedings of the ACM on Programming Languages10.1145/36329158:POPL(2191-2225)Online publication date: 5-Jan-2024
  • (2023)Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-TriggeringProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616276(1153-1164)Online publication date: 30-Nov-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)Error Localization for Sequential Effect SystemsStatic Analysis10.1007/978-3-031-44245-2_16(343-370)Online publication date: 22-Oct-2023
  • (2021)Corpse reviver: sound and efficient gradual typing via contract verificationProceedings of the ACM on Programming Languages10.1145/34343345:POPL(1-28)Online publication date: 4-Jan-2021
  • (2021)A graded dependent type system with a usage-aware semanticsProceedings of the ACM on Programming Languages10.1145/34343315:POPL(1-32)Online publication date: 4-Jan-2021
  • (2021)Provably space-efficient parallel functional programmingProceedings of the ACM on Programming Languages10.1145/34342995:POPL(1-33)Online publication date: 4-Jan-2021
  • (2021)Verifying correct usage of context-free API protocolsProceedings of the ACM on Programming Languages10.1145/34342985:POPL(1-30)Online publication date: 4-Jan-2021
  • (2020)DynamiTe: dynamic termination and non-termination proofsProceedings of the ACM on Programming Languages10.1145/34282574:OOPSLA(1-30)Online publication date: 13-Nov-2020
  • (2020)Rethinking safe consistency in distributed object-oriented programmingProceedings of the ACM on Programming Languages10.1145/34282564:OOPSLA(1-30)Online publication date: 13-Nov-2020
  • 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

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media