Nels E. Beckman
Jonathan Aldrich
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.
- Ali-Reza Adl-Tabatabai, Brian T. Lewis, Vijay Menon, Brian R. Murphy, Bratin Saha, and Tatiana Shpeisman. Compiler and runtime support for efficient software transactional memory. In PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, pages 26--37. ACM Press, 2006. Google Scholar
Digital Library
- 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.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 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.Google Scholar
- Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. In OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, pages 301--320. ACM Press, 2007. Google ScholarDigital Library
- Kevin Bierhoff and Jonathan Aldrich. Plural: Checking protocol compliance under aliasing. In Companion Proceedings of ICSE-30, pages 971--972. ACM Press, May 2008. Google ScholarDigital Library
- Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership types for safe programming: preventing data races and deadlocks. In OOPSLA '02: Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pages 211--230. ACM Press, 2002. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Robert DeLine and Manuel Fähndrich. Typestates for objects. In ECOOP '04: European Conference on Object-Oriented Programming, pages 465--490. Springer, 2004.Google ScholarCross Ref
- Dawson Engler and Ken Ashcraft. RacerX: effective, static detection of race conditions and deadlocks. In SOSP '03: Proceedings of the nineteenth ACM symposium on Operating systems principles, pages 237--252. ACM Press, 2003. Google ScholarDigital Library
- Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. In PLDI '03: Proceedings of the ACMSIGPLAN 2003 conference on Programming language design and implementation, pages 338--349. ACM Press, 2003. Google ScholarDigital Library
- Stephen Freund and Shaz Qadeer. Checking concise specifications for multithreaded software. In Workshop on Formal Techniques for Java-like Programs, 2003.Google Scholar
- Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50(1):1--102, 1987. Google ScholarDigital Library
- Aaron Greenhouse and William L. Scherlis. Assuring and evolving concurrent programs: annotations and policy. In ICSE '02: Proceedings of the 24th International Conference on Software Engineering, pages 453--463. ACM Press, 2002. Google ScholarDigital Library
- Dan Grossman. Type-safe multithreading in cyclone. In TLDI '03: Proceedings of the 2003 ACMSIGPLAN international workshop on Types in languages design and implementation, pages 13--25. ACM Press, 2003. Google ScholarDigital Library
- Dan Grossman. The transactional memory / garbage collection analogy. In OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, pages 695--706. ACM Press, 2007. Google ScholarDigital Library
- 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.Google Scholar
- Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Race checking by context inference. In PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pages 1--13. ACM Press, 2004. Google ScholarDigital Library
- 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.Google Scholar
- Benjamin Hindman and Dan Grossman. Atomicity via source-tosource translation. In MSPC '06: Proceedings of the 2006 workshop on Memory system performance and correctness, pages 82--91. ACM Press, 2006. Google ScholarDigital Library
- Bart Jacobs, Frank Piessens, K. Rustan M. Leino, and Wolfram Schulte. Safe concurrency for aggregate objects with invariants. In SEFM '05: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, pages 137--147, Washington, DC, USA, 2005. IEEE Computer Society. Google ScholarDigital Library
- Cliff B. Jones. Specification and design of (parallel) programs. In Proceedings of IFIP'83, pages 321--332. North-Holland, 1983.Google Scholar
- Patrick Lincoln and Andre Scedrov. First-order linear logic without modalities is NEXPTIME-hard. Theor. Comput. Sci., 135(1): 139--153, 1994. Google ScholarDigital Library
- Richard J. Lipton. Reduction: a method of proving properties of parallel programs. Commun. ACM, 18(12):717--721, 1975. Google ScholarDigital Library
- Katherine F. Moore and Dan Grossman. High-level small-step operational semantics for transactions. In POPL '08: Proceedings of the 35th annual ACMSIGPLAN-SIGACT symposium on Principles of programming languages, pages 51--62. ACM Press, 2008. Google ScholarDigital Library
- Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271--307, 2007. Google ScholarDigital Library
- Susan Owicki and David Gries. Verifying properties of parallel programs: an axiomatic approach. Commun. ACM, 19(5):279--285, 1976. Google ScholarDigital Library
- Polyvios Pratikakis, Jeffrey S. Foster, and Michael Hicks. Locksmith: context-sensitive correlation analysis for race detection. In PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, pages 320--331. ACM Press, 2006. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Amit Sasturkar, Rahul Agarwal, Liqiang Wang, and Scott D. Stoller. Automated type-based analysis of data races and atomicity. In PPoPP '05: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 83--94. ACM Press, 2005. Google ScholarDigital Library
- Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst., 15(4): 391--411, 1997. Google ScholarDigital Library
- Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst., 15(4): 391--411, 1997. Google ScholarDigital Library
- Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng., 12(1):157--171, 1986. Google ScholarDigital Library
- Mandana Vaziri, Frank Tip, and Julian Dolby. Associating synchronization constraints with data in an object-oriented language. In POPL '06: Conference record of the 33rd ACM SIGPLANSIGACT symposium on Principles of programming languages, pages 334--345. ACM, 2006. Google ScholarDigital Library
- 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.Google Scholar
- Yuan Yu, Tom Rodeheffer, and Wei Chen. Racetrack: efficient detection of data race conditions via adaptive tracking. In SOSP'05: Proceedings of the twentieth ACMsymposium on Operating systems principles, pages 221--234. ACM Press, 2005. Google ScholarDigital Library
- Yang Zhao. Checking Interference with Fractional Permissions. PhD thesis, University of Wisconsin-Milwaukee, August 2007.Google Scholar
Index Terms
- Verifying correct usage of atomic blocks and typestate
Recommendations
Typestate-like analysis of multiple interacting objects
OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applicationsThis paper presents a static analysis of typestate-like temporal specifications of groups of interacting objects, which are expressed using tracematches. Whereas typestate expresses a temporal specification of one object, a tracematch state may change ...
Verifying correct usage of atomic blocks and typestate
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 ...
The Clara framework for hybrid typestate analysis
A typestate property describes which operations are available on an object or a group of inter-related objects, depending on this object's or group's internal state, the typestate. Researchers in the field of static analysis have devised static program ...
Comments