Type inference for atomicity

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: Alexander Aiken, Introduction to set constraint-based program analysis, Science of Computer Programming, v.35 n.2-3, p.79-111, Nov.1.1999 [doi>10.1016/S0167-6423(99)00007-6]
• 3: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 4: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 5: D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, Massachusetts Institute of Technology, 1999.
• 6: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 7: L. Cardelli, Typechecking dependent types and subtypes, Lecture notes in computer science on Foundations of logic and functional programming, p.45-57, June 1988, Trento, Italy
• 8: Xianghua Deng , Matthew B. Dwyer , John Hatcliff , Masaaki Mizuno, Invariant-based specification, synthesis, and verification of synchronization in concurrent programs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581394]
• 9: Jeffrey L. Eppinger , Lily B. Mummert , Alfred Z. Spector, Camelot and Avalon: a distributed transaction facility, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1991
• 10: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 12: C. Flanagan and S. N. Freund. Type inference against races. In Static Analysis Symposium, pages 116--132, 2004.
• 13: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting purity for atomicity, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 14: C. Flanagan and S. Qadeer. Transactions for software model checking. In Proc. Workshop on Software Model Checking, 2003.
• 15: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 16: Cormac Flanagan , Shaz Qadeer, Types for atomicity, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 17: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268961]
• 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: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 20: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 21: Tim Harris , Keir Fraser, Language support for lightweight transactions, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 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: Maurice P. Herlihy , Jeannette M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.463-492, July 1990 [doi>10.1145/78969.78972]
• 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: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 27: B. Liskov , D. Curtis , P. Johnson , R. Scheifer, Implementation of Argus, Proceedings of the eleventh ACM Symposium on Operating systems principles, p.111-122, November 08-11, 1987, Austin, Texas, United States
• 28: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 29: Robert O'Callahan , Jong-Deok Choi, Hybrid dynamic data race detection, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 30: Christos Papadimitriou, The theory of database concurrency control, Computer Science Press, Inc., New York, NY, 1986
• 31: Shaz Qadeer , Sriram K. Rajamani , Jakob Rehof, Summarizing procedures in concurrent programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-255, January 14-16, 2004, Venice, Italy
• 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: Scott D. Stoller, Model-Checking Multi-threaded Distributed Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.224-244, August 30-September 01, 2000
• 35: J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245--271, 1992.
• 36: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• 37: Christoph von Praun , Thomas R. Gross, Static conflict analysis for multi-threaded object-oriented programs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Reliability, Verification

Keywords:
atomicity, concurrency, reduction, type inference