Verifying correct usage of atomic blocks and typestate

ABSTRACT

The atomic block, a synchronization primitive provided to programmers in transactional memory systems, has the potential to greatly ease the development of concurrent software. However, atomic blocks can still be used incorrectly, and race conditions can still occur at the level of application logic. In this paper, we present a intraprocedural static analysis, formalized as a type system and proven sound, that helps programmers use atomic blocks correctly. Using access permissions, which describe how objects are aliased and modified, our system statically prevents race conditions and enforces typestate properties in concurrent programs. We have implemented a prototype static analysis for the Java language based on our system and have used it to verify several realistic examples.

REFERENCES

• 1: Ali-Reza Adl-Tabatabai , Brian T. Lewis , Vijay Menon , Brian R. Murphy , Bratin Saha , Tatiana Shpeisman, Compiler and runtime support for efficient software transactional memory, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 2: Cyrille Artho, Klaus Havelund, and Armin Biere. High level data races. In VVEIS '03: Proceedings of the Workshop on Verification and Validation of Enterprise Information Systems, pages 82--93, April 2003.
• 3: Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology Special Issue: ECOOP 2003 workshop on Formal Techniques for Javalike Programs, 3(6):27--56, June 2004.
• 4: Nels E. Beckman and Jonathan Aldrich. Verifying correct usage of atomic blocks and typestate: Technical companion. Technical Report CMU-ISR-08-126, Carnegie Mellon University, 2008. http://reports-archive.adm.cs.cmu.edu/anon/isr2008/CMU-ISR-08-126.pdf.
• 5: Kevin Bierhoff , Jonathan Aldrich, Modular typestate checking of aliased objects, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 6: Kevin Bierhoff , Jonathan Aldrich, PLURAL: checking protocol compliance under aliasing, Companion of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany [doi>10.1145/1370175.1370213]
• 7: 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
• 8: John Boyland. Checking interference with fractional permissions. In R. Cousot, editor, Static Analysis: 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 55--72, Berlin, Heidelberg, New York, 2003. Springer.
• 9: Robert DeLine and Manuel Fähndrich. Typestates for objects. In ECOOP '04: European Conference on Object-Oriented Programming, pages 465--490. Springer, 2004.
• 10: Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 11: 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
• 12: Stephen Freund and Shaz Qadeer. Checking concise specifications for multithreaded software. In Workshop on Formal Techniques for Java-like Programs, 2003.
• 13: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 14: Aaron Greenhouse , William L. Scherlis, Assuring and evolving concurrent programs: annotations and policy, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581395]
• 15: 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
• 16: Dan Grossman, The transactional memory / garbage collection analogy, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 17: Tim Harris and Simon Peyton Jones. Transactional memory with data invariants. In TRANSACT '06: First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing, 2006.
• 18: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Race checking by context inference, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 19: Michael Hicks, Jeffrey S. Foster, and Polyvios Pratikakis. Lock inference for atomic sections. In TRANSACT '06: First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing, 2006.
• 20: Benjamin Hindman , Dan Grossman, Atomicity via source-to-source translation, Proceedings of the 2006 workshop on Memory system performance and correctness, October 22-22, 2006, San Jose, California [doi>10.1145/1178597.1178611]
• 21: Bart Jacobs , Frank Piessens , K. Rustan M. Leino , Wolfram Schulte, Safe Concurrency for Aggregate Objects with Invariants, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.137-147, September 07-09, 2005 [doi>10.1109/SEFM.2005.39]
• 22: Cliff B. Jones. Specification and design of (parallel) programs. In Proceedings of IFIP'83, pages 321--332. North-Holland, 1983.
• 23: P. Lincoln , A. Scedrov, First-order linear logic without modalities is NEXPTIME-hard, Theoretical Computer Science, v.135 n.1, p.139-153, Dec. 5, 1994
• 24: 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]
• 25: Katherine F. Moore , Dan Grossman, High-level small-step operational semantics for transactions, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 26: Peter W. OHearn, Resources, concurrency, and local reasoning, Theoretical Computer Science, v.375 n.1-3, p.271-307, May, 2007 [doi>10.1016/j.tcs.2006.12.035]
• 27: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 28: 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
• 29: Edwin Rodriguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, and Robby. Extending JML for modular specification and verification of multi-threaded programs. In ECOOP '05: Object-Oriented Programming 19th European Conference, pages 551--576, 2005.
• 30: 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]
• 31: 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]
• 32: 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]
• 33: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 34: 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
• 35: Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, pages 347--359. North Holland, 1990.
• 36: Yuan Yu , Tom Rodeheffer , Wei Chen, RaceTrack: efficient detection of data race conditions via adaptive tracking, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom
• 37: Yang Zhao. Checking Interference with Fractional Permissions. PhD thesis, University of Wisconsin-Milwaukee, August 2007.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Concurrent, distributed, and parallel languages

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

General Terms:
Languages, Verification

Keywords:
permissions, transactional memory, typestate