Cormac Flanagan
Stephen N. Freund
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.
- 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.Google Scholar
Cross Ref
- A. Aiken. Introduction to set constraint-based program analysis. Science of Computer Programming, 35(2):79--111, 1999. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, Massachusetts Institute of Technology, 1999.Google Scholar
- R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput., C-35(8):677--691, Aug. 1986. Google ScholarDigital Library
- L. Cardelli. Typechecking dependent types and subtypes. In Lecture notes in computer science on Foundations of logic and functional programming, pages 45--57, 1988. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. L. Eppinger, L. B. Mummert, and A. Z. Spector. Camelot and Avalon: A Distributed Transaction Facility. Morgan Kaufmann, 1991. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Type inference against races. In Static Analysis Symposium, pages 116--132, 2004.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Transactions for software model checking. In Proc. Workshop on Software Model Checking, 2003.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Types for atomicity. In Proc. ACM Workshop on Types in Language Design and Implementation, pages 1--12, 2003. Google ScholarDigital Library
- M. Flatt, S. Krishnamurthi, and M. Felleisen. Classes and mixins. In Proc. ACM Symposium on the Principles of Programming Languages, pages 171--183, 1998. Google ScholarDigital Library
- S. N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. In Journal of Object Technology, volume 3(6), pages 81--101, 2004.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- D. Grossman. Type-safe multithreading in Cyclone. In Proc. ACM Workshop on Types in Language Design and Implementation, pages 13--25, 2003. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Java Grande Forum. Java Grande benchmark suite. Available from http://www.javagrande.org/, 2003.Google Scholar
- D. Lea. util.concurrent package, release 1.3.4, 2004. Available at http://gee.cs.oswego.edu/dl/.Google Scholar
- R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975. Google ScholarDigital Library
- B. Liskov, D. Curtis, P. Johnson, and R. Scheifler. Implementation of Argus. In Proc. Symposium on Operating Systems Principles, pages 111--122, 1987. Google ScholarDigital Library
- J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proc. ACM Conference on Lisp and Functional Programming, pages 47--57, 1988. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- C. Papadimitriou. The theory of database concurrency control. Computer Science Press, 1986. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Sasturkar, R. Agarwal, and S. D. Stoller. Extended parameterized Atomic Java, 2004. Submitted for publication.Google Scholar
- Standard Performance Evaluation Corporation. SPEC Benchmarks. Available from http://www.spec.org/, 2004.Google Scholar
- S. D. Stoller. Model-checking multi-threaded distributed Java programs. In Workshop on Model Checking and Software Verification, pages 224--244, 2000. Google ScholarDigital Library
- J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245--271, 1992.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- A. Welc, S. Jagannathan, and A. L. Hosking. Transactional monitors for concurrent objects. In Proc. European Conference on Object-Oriented Programming, 2004.Google ScholarCross Ref
Index Terms
- Type inference for atomicity
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 ...
Atomizer: A dynamic atomicity checker for multithreaded programs
Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected interactions between concurrent threads. Much previous work has focused on detecting race conditions, but the absence of race conditions does not by ...
Comments