skip to main content
10.1145/1040294.1040299acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

Type inference for atomicity

Published: 10 January 2005 Publication History

Abstract

Atomicity is a fundamental correctness property in multithreaded programs. This paper presents an algorithm for verifying atomicity via type inference. The underlying type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We describe an implementation of this algorithm for Java and discuss its performance and usability on benchmarks totaling sixty thousand lines of code.

References

[1]
R. Agarwal and S. D. Stoller. Type inference for parameterized race-free Java. In Proc. Conference on Verification, Model Checking, and Abstract Interpretation, pages 149--160, 2004.
[2]
A. Aiken. Introduction to set constraint-based program analysis. Science of Computer Programming, 35(2):79--111, 1999.
[3]
C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: preventing data races and deadlocks. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 211--230, 2002.
[4]
C. Boyapati and M. Rinard. A parameterized type system for race-free Java programs. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 56--69, 2001.
[5]
D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, Massachusetts Institute of Technology, 1999.
[6]
R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput., C-35(8):677--691, Aug. 1986.
[7]
L. Cardelli. Typechecking dependent types and subtypes. In Lecture notes in computer science on Foundations of logic and functional programming, pages 45--57, 1988.
[8]
X. Deng, M. Dwyer, J. Hatcliff, and M. Mizuno. Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In International Conference on Software Engineering, pages 442--452, 2002.
[9]
J. L. Eppinger, L. B. Mummert, and A. Z. Spector. Camelot and Avalon: A Distributed Transaction Facility. Morgan Kaufmann, 1991.
[10]
C. Flanagan and S. N. Freund. Type-based race detection for Java. In Proc. ACM Conference on Programming Language Design and Implementation, pages 219--232, 2000.
[11]
C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multi-threaded programs. In Proc. ACM Symposium on the Principles of Programming Languages, pages 256--267, 2004.
[12]
C. Flanagan and S. N. Freund. Type inference against races. In Static Analysis Symposium, pages 116--132, 2004.
[13]
C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. In Proc. International Symposium on Software Testing and Analysis, pages 221--231, 2004.
[14]
C. Flanagan and S. Qadeer. Transactions for software model checking. In Proc. Workshop on Software Model Checking, 2003.
[15]
C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proc. ACM Conference on Programming Language Design and Implementation, pages 338--349, 2003.
[16]
C. Flanagan and S. Qadeer. Types for atomicity. In Proc. ACM Workshop on Types in Language Design and Implementation, pages 1--12, 2003.
[17]
M. Flatt, S. Krishnamurthi, and M. Felleisen. Classes and mixins. In Proc. ACM Symposium on the Principles of Programming Languages, pages 171--183, 1998.
[18]
S. N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. In Journal of Object Technology, volume 3(6), pages 81--101, 2004.
[19]
P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Lecture Notes in Computer Science 1032. Springer-Verlag, 1996.
[20]
D. Grossman. Type-safe multithreading in Cyclone. In Proc. ACM Workshop on Types in Language Design and Implementation, pages 13--25, 2003.
[21]
T. L. Harris and K. Fraser. Language support for lightweight transactions. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 388--402, 2003.
[22]
J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In Proc. International Conference on Verification, Model Checking and Abstract Interpretation, 2004.
[23]
M. P. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463--492, 1990.
[24]
Java Grande Forum. Java Grande benchmark suite. Available from http://www.javagrande.org/, 2003.
[25]
D. Lea. util.concurrent package, release 1.3.4, 2004. Available at http://gee.cs.oswego.edu/dl/.
[26]
R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975.
[27]
B. Liskov, D. Curtis, P. Johnson, and R. Scheifler. Implementation of Argus. In Proc. Symposium on Operating Systems Principles, pages 111--122, 1987.
[28]
J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proc. ACM Conference on Lisp and Functional Programming, pages 47--57, 1988.
[29]
R. O'Callahan and J.-D. Choi. Hybrid dynamic data race detection. In ACM Symposium on Principles and Practice of Parallel Programming, pages 167--178, 2003.
[30]
C. Papadimitriou. The theory of database concurrency control. Computer Science Press, 1986.
[31]
S. Qadeer, S. K. Rajamani, and J. Rehof. Summarizing procedures in concurrent programs. In Proc. ACM Symposium on the Principles of Programming Languages, pages 245--255, 2004.
[32]
A. Sasturkar, R. Agarwal, and S. D. Stoller. Extended parameterized Atomic Java, 2004. Submitted for publication.
[33]
Standard Performance Evaluation Corporation. SPEC Benchmarks. Available from http://www.spec.org/, 2004.
[34]
S. D. Stoller. Model-checking multi-threaded distributed Java programs. In Workshop on Model Checking and Software Verification, pages 224--244, 2000.
[35]
J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245--271, 1992.
[36]
M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value lambda-calculus using a stack of regions. In Proc. ACM Symposium on the Principles of Programming Languages, pages 188--201, 1994.
[37]
C. von Praun and T. Gross. Static conflict analysis for multi-threaded object-oriented programs. In Proc. ACM Conference on Programming Language Design and Implementation, pages 115--128, 2003.
[38]
L. Wang and S. D. Stoller. Runtime analysis of atomicity for multi-threaded programs. Technical Report DAR 04-14, Computer Science Department, SUNY Stony Brook, July 2004. A preliminary version appeared in Proc. Workshop on Runtime Verification, 2003.
[39]
A. Welc, S. Jagannathan, and A. L. Hosking. Transactional monitors for concurrent objects. In Proc. European Conference on Object-Oriented Programming, 2004.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
TLDI '05: Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation
January 2005
122 pages
ISBN:1581139993
DOI:10.1145/1040294
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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 January 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. atomicity
  2. concurrency
  3. reduction
  4. type inference

Qualifiers

  • Article

Conference

TLDI05
Sponsor:

Acceptance Rates

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (2023)Error Localization for Sequential Effect SystemsStatic Analysis10.1007/978-3-031-44245-2_16(343-370)Online publication date: 24-Oct-2023
  • (2013)Heap decomposition inference with linear programmingProceedings of the 27th European conference on Object-Oriented Programming10.1007/978-3-642-39038-8_5(104-128)Online publication date: 1-Jul-2013
  • (2011)LOCKSMITHACM Transactions on Programming Languages and Systems10.1145/1889997.189000033:1(1-55)Online publication date: 25-Jan-2011
  • (2010)Effects for cooperable and serializable threadsProceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation10.1145/1708016.1708019(3-14)Online publication date: 23-Jan-2010
  • (2009)LiteRaceACM SIGPLAN Notices10.1145/1543135.154249144:6(134-143)Online publication date: 15-Jun-2009
  • (2009)FastTrackACM SIGPLAN Notices10.1145/1543135.154249044:6(121-133)Online publication date: 15-Jun-2009
  • (2009)A randomized dynamic program analysis technique for detecting real deadlocksACM SIGPLAN Notices10.1145/1543135.154248944:6(110-120)Online publication date: 15-Jun-2009
  • (2009)Lightweight annotations for controlling sharing in concurrent data structuresACM SIGPLAN Notices10.1145/1543135.154248844:6(98-109)Online publication date: 15-Jun-2009
  • (2009)Lightweight annotations for controlling sharing in concurrent data structuresProceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1542476.1542488(98-109)Online publication date: 15-Jun-2009
  • (2008)Keep off the grassProceedings of the Joint European Conferences on Theory and Practice of Software 17th international conference on Compiler construction10.5555/1788374.1788399(276-290)Online publication date: 29-Mar-2008
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media