Aditya Kulkarni
ABSTRACT
Atomic regions are an important concept in correct concurrent programming: since atomic regions can be viewed as having executed in a single step, atomicity greatly reduces the number of possible interleavings the programmer needs to consider. This paper describes a method for building atomicity into a programming language in an organic fashion. We take the view that atomicity holds for whole threads by default, and a division into smaller atomic regions occurs only at points where an explicit need for sharing is needed and declared. A corollary of this view is every line of code is part of some atomic region. We define a polymorphic type system, Task Types, to enforce most of the desired atomicity properties statically. We show the reasonableness of our type system by proving that type soundness, isolation invariance, and atomicity enforcement properties hold at run time. We also present initial results of a Task Types implementation built on Java
- }}Martin Abadi, Andrew Birrell, Tim Harris, and Michael Isard. Semantics of transactional memory and automatic mutual exclusion. In POPL '08, pages 63--74, 2008. Google Scholar
Digital Library
- }}Ole Agesen. Concrete type inference: delivering object-oriented applications. PhD thesis, Stanford University, Stanford, CA, USA, 1996. Google ScholarDigital Library
- }}Gul Agha. ACTORS : A model of Concurrent computations in Distributed Systems. MITP, Cambridge, Mass., 1990. Google ScholarDigital Library
- }}J. Armstrong. Erlang - a Survey of the Language and its Industrial Applications. In INAP'96 - The 9th Exhibitions and Symposium on Industrial Applications of Prolog, pages 16--18, Hino, Tokyo, Japan, 1996.Google Scholar
- }}Robert L. Bocchino, Jr., Vikram S. Adve, Danny Dig, Sarita V. Adve, Stephen Heumann, Rakesh Komuravelli, Jeffrey Overbey, Patrick Simmons, Hyojin Sung, and Mohsen Vakilian. A type and effect system for deterministic parallel java. In OOPSLA '09, pages 97--116, 2009. Google ScholarDigital Library
- }}Bruno Blanchet. Escape analysis for object-oriented languages: application to java. SIGPLAN Not., 34(10):20--34, 1999. Google ScholarDigital Library
- }}Marc Berndl, Ondrej Lhoták, Feng Qian, Laurie Hendren, and Navindra Umanee. Points-to analysis using bdds. In PLDI '03, pages 103--114, 2003. Google ScholarDigital Library
- }}Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership types for safe programming: preventing data races and deadlocks. In OOPSLA '02, pages 211--230, 2002. Google ScholarDigital Library
- }}Stephen Brookes. A semantics for concurrent separation logic. Theoretical Computer Science, 375(1-3):227 -- 270, 2007. Google ScholarDigital Library
- }}Sigmund Cherem, Trishul Chilimbi, and Sumit Gulwani. Inferring locks for atomic sections. In PLDI'08, pages 304--315, 2008. Google ScholarDigital Library
- }}Wei-Ngan Chin, Florin Craciun, Shengchao Qin, and Martin Rinard. Region inference for an object-oriented language. In PLDI '04, pages 243--254, 2004. Google ScholarDigital Library
- }}Jong-deok Choi, Manish Gupta, Mauricio Serrano, Vugranam C. Sreedhar, and Sam Midkiff. Escape analysis for java. In OOPSLA'99, pages 1--19, 1999. Google ScholarDigital Library
- }}Dave Clarke. Object Ownership and Containment. PhD thesis, University of New South Wales, July 2001. Google ScholarDigital Library
- }}B. CarlStrom, A. McDonald, H. Chafi, J. Chung, C. Minh, C. Kozyrakis, and K. Olukotun. The atomos transactional programming language. In PLDI'06, June 2006. Google ScholarDigital Library
- }}David G. Clarke, John M. Potter, and James Noble. Ownership types for flexible alias protection. In In OOPSLA'98, pages 48--64. ACM Press, 1998. Google ScholarDigital Library
- }}Jeffrey Dean and Sanjay Ghemawat. MapReduce: Simplified data processing on large clusters. In OSDI'04, 2004. Google ScholarDigital Library
- }}W. Dietl and P. Müller. Runtime universe type inference. In IWACO'07, 2007.Google Scholar
- }}Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, and Rupak Majumdar. Lock allocation. In POPL '07, pages 291--296, 2007. Google ScholarDigital Library
- }}Maryam Emami, Rakesh Ghiya, and Laurie J. Hendren. Context-sensitive interprocedural points-to analysis in the presence of function pointers. In PLDI'94, pages 242--256, 1994. Google ScholarDigital Library
- }}Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. In PLDI'03, pages 338--349, 2003. Google ScholarDigital Library
- }}William D. Gropp, Ewing Lusk, and Anthony Skjellum. Using MPI - Portable Parallel Programming with the Message Passing Interface. MIT Press, Cambridge, MA, 1994. Google ScholarDigital Library
- }}Dan Grossman. Type-safe multithreading in cyclone. In TLDI '03, pages 13--25, 2003. Google ScholarDigital Library
- }}Tim Harris and Keir Fraser. Language support for lightweight transactions. In OOPSLA'03, pages 388--402, 2003. Google ScholarDigital Library
- }}Michael Hicks, Jeffrey S. Foster, and Polyvios Prattikakis. Lock inference for atomic sections. In TRANSACT'06, June 2006.Google Scholar
- }}Tim Harris, Simon Marlow, Simon Peyton-Jones, and Maurice Herlihy. Composable memory transactions. In PPoPP '05, pages 48--60, 2005. Google ScholarDigital Library
- }}Michael Isard and Andrew Birrell. Automatic mutual exclusion. In HOTOS'07: Proceedings of the 11th USENIX workshop on Hot topics in operating systems, pages 1--6, Berkeley, CA, USA, 2007. USENIX Association. Google ScholarDigital Library
- }}Atsushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight java - a minimal core calculus for java and gj. In ACM Transactions on Programming Languages and Systems, pages 132--146, 1999. Google ScholarDigital Library
- }}Sheng Liang and Gilad Bracha. Dynamic class loading in the java virtual machine. In In OOPSLA'98, pages 36--44. ACM Press, 1998. 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
- }}Yu David Liu, Xiaoqi Lu, and Scott F. Smith. Coqa: Concurrent objects with quantized atomicity. In CC'08, March 2008. Google ScholarDigital Library
- }}Yu David Liu and Scott Smith. Pedigree types. In 4th International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), pages 63--71, July 2008.Google Scholar
- }}Ana Milanova, Atanas Rountev, and Barbara G. Ryder. Parameterized object sensitivity for points-to analysis for java. ACM Trans. Softw. Eng. Methodol., 14(1):1--41, 2005. Google ScholarDigital Library
- }}Bill McCloskey, Feng Zhou, David Gay, and Eric Brewer. Autolocker: synchronization inference for atomic sections. In POPL'06, pages 346--358, 2006. Google ScholarDigital Library
- }}Nathaniel Nystrom, Michael R. Clarkson, and Andrew C. Myers. Polyglot: An extensible compiler framework for java. In CC'03, volume 2622, pages 138--152, NY, April 2003. Springer-Verlag. Google ScholarDigital Library
- }}Peter W. OHearn. Resources, concurrency, and local reasoning. Theoretical Computer Science, 375(1-3):271--307, 2007. Google ScholarDigital Library
- }}Matthew Parkinson and Gavin Bierman. Separation logic and abstraction. In POPL'05, pages 247--258, 2005. Google ScholarDigital Library
- }}Matthew J. Parkinson and Gavin M. Bierman. Separation logic, abstraction and inheritance. In POPL '08, pages 75--86, New York, NY, USA, 2008. ACM. Google ScholarDigital Library
- }}L. A. Smith, J. M. Bull, and J. Obdrzálek. A parallel java grande benchmark suite. In Supercomputing '01: Proceedings of the 2001 ACM/IEEE conference on Supercomputing, 2001. Google ScholarDigital Library
- }}Sriram Srinivasan and Alan Mycroft. Kilim: Isolation-typed actors for java. In ECOOP'08, 2008. Google ScholarDigital Library
- }}Tatiana Shpeisman, Vijay Menon, Ali-Reza Adl-Tabatabai, Steven Balensiefer, Dan Grossman, Richard L. Hudson, Katherine F. Moore, and Bratin Saha. Enforcing isolation and ordering in stm. In PLDI'07, pages 78--88, 2007. Google ScholarDigital Library
- }}http://www.cs.binghamton.edu/~davidL/tasktypes.Google Scholar
- }}Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 1997. Google ScholarDigital Library
- }}Mandana Vaziri, Frank Tip, and Julian Dolby. Associating synchronization constraints with data in an object-oriented language. In POPL '06, pages 334--345, 2006. Google ScholarDigital Library
- }}Adam Welc, Suresh Jagannathan, and Antony L. Hosking. Transactional monitors for concurrent objects. In ECOOP'04, pages 519--542, 2004.Google ScholarCross Ref
- }}John Whaley and Monica S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI'04, pages 131--144, 2004. Google ScholarDigital Library
- }}John Whaley and Martin Rinard. Compositional pointer and escape analysis for java programs. In OOPSLA, pages 187--206, 1999. Google ScholarDigital Library
- }}Alisdair Wren. Ownership type inference. Master's thesis, Imperial College, 2003.Google Scholar
- }}Tiejun Wang and Scott F. Smith. Precise constraint-based type inference for Java. In ECOOP'01, pages 99--117, 2001. Google ScholarDigital Library
Index Terms
- Task types for pervasive atomicity
Recommendations
Task types for pervasive atomicity
OOPSLA '10Atomic regions are an important concept in correct concurrent programming: since atomic regions can be viewed as having executed in a single step, atomicity greatly reduces the number of possible interleavings the programmer needs to consider. This ...
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 ...
Types for atomicity
Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions, between threads. Previous work addressed this problem by devising tools for detecting race conditions, a situation ...
Comments