Types for atomicity: Static checking and inference for Java

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.

REFERENCES

• 1: Martin Abadi , Cormac Flanagan , Stephen N. Freund, Types for safe locking: Static race detection for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.207-255, March 2006 [doi>10.1145/1119479.1119480]
• 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: Alexander Aiken , David Gay, Barrier inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.342-354, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268974]
• 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: Ralph-Johan Back, A Method for Refining Atomicity in Parallel Algorithms, Proceedings of the Parallel Architectures and Languages Europe, Volume II: Parallel Languages, p.199-216, June 12-16, 1989
• 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: 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
• 9: Bruening, D. 1999. Systematic testing of multithreaded Java programs. M.S. thesis, Massachusetts Institute of Technology.
• 10: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 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: 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
• 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: Jong-Deok Choi , Manish Gupta , Mauricio Serrano , Vugranam C. Sreedhar , Sam Midkiff, Escape analysis for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-19, November 01-05, 1999, Denver, Colorado, United States
• 15: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 16: Ernie Cohen , Leslie Lamport, Reduction in TLA, Proceedings of the 9th International Conference on Concurrency Theory, p.317-331, September 08-11, 1998
• 17: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 18: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 19: 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]
• 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: Thomas W. Doeppner, Jr., Parallel program correctness through refinement, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.155-169, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512965]
• 22: Jeffrey L. Eppinger , Lily B. Mummert , Alfred Z. Spector, Camelot and Avalon: a distributed transaction facility, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1991
• 23: Flanagan, C. 2004. Verifying commit-atomicity using model-checking. In Proceedings of the International SPIN Workshop on Model Checking of Software.
• 24: Cormac Flanagan , Martín Abadi, Object Types against Races, Proceedings of the 10th International Conference on Concurrency Theory, p.288-303, August 24-27, 1999
• 25: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 26: 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
• 27: 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
• 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: Cormac Flanagan , Stephen N. Freund , Marina Lifshin, Type inference for atomicity, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.47-58, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040299]
• 31: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting Purity for Atomicity, IEEE Transactions on Software Engineering, v.31 n.4, p.275-291, April 2005 [doi>10.1109/TSE.2005.47]
• 32: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 33: Flanagan, C. and Qadeer, S. 2003a. Transactions for software model checking. In Proceedings of the Workshop on Software Model Checking.
• 34: 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
• 35: 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
• 36: 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]
• 37: Freund, S. N. and Qadeer, S. 2004. Checking concise specifications for multithreaded software. J. Object Tech. 3, 6, 81--101.
• 38: Kourosh Gharachorloo, Memory consistency models for shared-memory multiprocessors, Stanford University, Stanford, CA, 1996
• 39: Tim Peierls , Brian Goetz , Joshua Bloch , Joseph Bowbeer , Doug Lea , David Holmes, Java Concurrency in Practice, Addison-Wesley Professional, 2005
• 40: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 41: 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
• 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: 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
• 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: 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]
• 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: C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
• 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: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 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: 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]
• 55: 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
• 56: D. B. Lomet, Process structuring, synchronization, and recovery using atomic actions, Proceedings of an ACM conference on Language design for reliable software, p.128-137, March 28-30, 1977, Raleigh, North Carolina
• 57: 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]
• 58: Jeremy Manson , William Pugh , Sarita V. Adve, The Java memory model, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.378-391, January 12-14, 2005, Long Beach, California, USA
• 59: Bill McCloskey , Feng Zhou , David Gay , Eric Brewer, Autolocker: synchronization inference for atomic sections, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.346-358, January 11-13, 2006, Charleston, South Carolina, USA
• 60: Jayadev Misra, A discipline of multiprogramming: programming theory for distributed applications, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 61: Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 62: 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
• 63: Christos Papadimitriou, The theory of database concurrency control, Computer Science Press, Inc., New York, NY, 1986
• 64: Eli Pozniansky , Assaf Schuster, Efficient on-the-fly data race detection in multithreaded C++ programs, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 65: Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 66: 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
• 67: Michael F. Ringenburg , Dan Grossman, AtomCaml: first-class atomicity via rollback, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 68: Alexandru Salcianu , Martin Rinard, Pointer and escape analysis for multithreaded programs, Proceedings of the eighth ACM SIGPLAN symposium on Principles and practices of parallel programming, p.12-23, June 2001, Snowbird, Utah, United States
• 69: Amit Sasturkar , Rahul Agarwal , Liqiang Wang , Scott D. Stoller, Automated type-based analysis of data races and atomicity, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065956]
• 70: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 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: 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
• 75: Talpin, J.-P. and Jouvelot, P. 1992. Polymorphic type, region and effect inference. J. Funct. Program. 2, 3, 245--271.
• 76: 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]
• 77: Mandana Vaziri , Frank Tip , Julian Dolby, Associating synchronization constraints with data in an object-oriented language, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.334-345, January 11-13, 2006, Charleston, South Carolina, USA
• 78: Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
• 79: 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
• 80: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 81: Wang, L. and Stoller, S. D. 2003. Runtime analysis for atomicity. In Proceedings of the Workshop on Runtime Verification.
• 82: Liqiang Wang , Scott D. Stoller, Runtime Analysis of Atomicity for Multithreaded Programs, IEEE Transactions on Software Engineering, v.32 n.2, p.93-110, February 2006 [doi>10.1109/TSE.2006.1599419]
• 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.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics
      D.3.2 Language Classifications
          Subjects: Concurrent, distributed, and parallel languages

General Terms:
Languages, Reliability, Verification

Keywords:
Atomicity, concurrent programs, type inference, type systems