What do high-level memory models mean for transactions?

ABSTRACT

Many people have proposed adding transactions, or atomic blocks, to type-safe high-level programming languages. However, researchers have not considered the semantics of transactions with respect to a memory model weaker than sequential consistency. The details of such semantics are more subtle than many people realize, and the interaction between compiler transformations and transactions could produce behaviors that many people find surprising. A language's memory model, which determines these interactions, must clearly indicate which behaviors are legal, and which are not. These design decisions affect both the idioms that are useful for designing concurrent software and the compiler transformations that are legal within the language.Cases where semantics are more subtle than people expect include the actual meaning of both strong and weak atomicity; correct idioms for thread safe lazy initialization; compiler transformations of transactions that touch only thread local memory; and whether there is a well-defined notion for transactions that corresponds to the notion of correct and incorrect use of synchronization in Java. Open questions for a high-level memory-model that includes transactions involve both issues of isolation and ordering.

REFERENCES

• 1: {ACL+a} Eric Allen, David Chase, Victor Luchangco, Jan-Willem Maessen, Sukyoung Ryu, Guy L. Steele Jr., and Sam Tobin-Hochstadt. The Fortress language specification, version 0.903. http://research.sun.com/projects/plrg/fortress0903.pdf.
• 2: {ACL+b} Eric Allen, David Chase, Victor Luchangco, Jan-Willem Maessen, Sukyoung Ryu, Guy L. Steele Jr., and Sam Tobin-Hochstadt. The Fortress language specification, version 1.0α. http://research.sun.com/projects/plrg/fortress.pdf.
• 3: Sarita V. Adve , Kourosh Gharachorloo, Shared Memory Consistency Models: A Tutorial, Computer, v.29 n.12, p.66-76, December 1996 [doi>10.1109/2.546611]
• 4: Sarita V. Adve , Mark D. Hill, Weak ordering—a new definition, Proceedings of the 17th annual international symposium on Computer Architecture, p.2-14, May 28-31, 1990, Seattle, Washington, United States
• 5: S. V. Adve , J. K. Aggarwal, A Unified Formalization of Four Shared-Memory Models, IEEE Transactions on Parallel and Distributed Systems, v.4 n.6, p.613-624, June 1993 [doi>10.1109/71.242161]
• 6: Jan-Willem Maessen , Xiaowei Shen, Improving the Java memory model using CRF, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-12, October 2000, Minneapolis, Minnesota, United States
• 7: 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
• 8: {BBC+} David Bacon Joshua Bloch, Jeff Bogda, Cliff Click, Paul Haahr, Doug Lea, Tom May, Jan-Willem Maessen, John D. Mitchell Kelvin Nilsen, Bill Pugh, and Emin Gun Sirer. The double-checked locking is broken declaration. http://www.cs.umd.edu/pugh/java/memoryModel/DoubleCheckedLocki
• 9: {BLM05} Colin Blundell, E. Christopher Lewis, and Milo M. K. Martin. Deconstructing Transactional Semantics: The Subtleties of Atomicity. In Proceedings of the 2005 Workshop on Duplicating, Deconstructing and Debunking, 2005.
• 10: Hans-J. Boehm, Threads cannot be implemented as a library, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 11: Brian D. Carlstrom , Austen McDonald , Hassan Chafi , JaeWoong Chung , Chi Cao Minh , Christos Kozyrakis , Kunle Olukotun, The Atomos transactional programming language, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 12: 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
• 13: Kourosh Gharachorloo , Daniel Lenoski , James Laudon , Phillip Gibbons , Anoop Gupta , John Hennessy, Memory consistency and event ordering in scalable shared-memory multiprocessors, Proceedings of the 17th annual international symposium on Computer Architecture, p.15-26, May 28-31, 1990, Seattle, Washington, United States
• 14: Lance Hammond , Brian D. Carlstrom , Vicky Wong , Ben Hertzberg , Mike Chen , Christos Kozyrakis , Kunle Olukotun, Programming with transactional coherence and consistency (TCC), Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 15: 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
• 16: Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, 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.1065952]
• 17: C. A. R. Hoare, Towards a theory of parallel programming, The origin of concurrent programming: from semaphores to remote procedure calls, Springer-Verlag New York, Inc., New York, NY, 2002
• 18: Tim Harris , Mark Plesko , Avraham Shinnar , David Tarditi, Optimizing memory transactions, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 19: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 20: 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]
• 21: {LB98} Bil Lewis and Daniel J. Berg. Multithreaded programming with pthreads. 1998.
• 22: {Lea04} Doug Lea. JSR-133 Cookbook, 2004. Available from http://gee.cs.oswego.edu/dl/jmm/cookbook.html.
• 23: Austen McDonald , JaeWoong Chung , Brian D. Carlstrom , Chi Cao Minh , Hassan Chafi , Christos Kozyrakis , Kunle Olukotun, Architectural Semantics for Practical Transactional Memory, Proceedings of the 33rd annual international symposium on Computer Architecture, p.53-65, June 17-21, 2006
• 24: 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
• 25: 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
• 26: {Sco06} Michael L. Scott. Sequential specification of transactional memory semantics. In First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT), June 2006.
• 27: {SH96} Douglas Schmidt and Tim Harrison. Double-Checked Locking: An Optimization Pattern for Efficiently Initializing and Accessing Thread-safe Objects. In Third Annual Pattern Languages of Program Design Conference, 1996.
• 28: {Str97} Bjarne Stroustrup. The C++ Programming Language. Addison-Wesley Longman, Reading Mass. USA, 3rd edition, 1997.
• 29: {VJWH04} Jan Vitek, Suresh Jagannathan, Adam Welc, and Antony L. Hosking. A semantic framework for designer transactions. In 13th European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, pages 249--263, 2004.
• 30: {WJH05} Adam Welc, Suresh Jagannathan, and Antony L. Hosking. Revocation Techniques for Java Concurrency. Concurrency and Computation: Practice and Experience, 2005.
• 31: Yue Yang , Ganesh Gopalakrishnan , Gary Lindstrom, Specifying Java thread semantics using a uniform memory model, Proceedings of the 2002 joint ACM-ISCOPE conference on Java Grande, p.192-201, November 03-05, 2002, Seattle, Washington, USA [doi>10.1145/583810.583832]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Memory management (garbage collection)

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Dynamic storage management
      D.3.4 Processors
          Subjects: Run-time environments; Compilers

General Terms:
Design, Management