Article

What do high-level memory models mean for transactions?

Authors:

William PughAuthors Info & Claims

MSPC '06: Proceedings of the 2006 workshop on Memory system performance and correctness

Pages 62 - 69

https://doi.org/10.1145/1178597.1178609

Published: 22 October 2006 Publication History

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]

{AG96} Sarita Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66--76, 1996.

Digital Library

[4]

{AH90} Sarita Adve and Mark Hill. Weak ordering---A new definition. In Proc. of the 17th Annual Int'l Symp. on Computer Architecture (ISCA'90), pages 2--14, 1990.

Digital Library

[5]

{AH93} Sarita V. Adve and Mark D. Hill. A unified formalization of four shared-memory models. IEEE Trans. on Parallel and Distributed Systems, 4(6):613--624, June 1993.

Digital Library

[6]

{AMS00} Arvind, Jan-Willem Maessen, and Xiaowei Shen. Improving the Java memory model using CRF. In OOPSLA, pages 1--12, October 2000.

Digital Library

[7]

{ATLM+06} Ali-Reza Adl-Tabatabai, Brian Lewis, Vijay Menon, Brian R. Murphy, Bratin Saha, and Tatiana Shpeisman. Compiler and runtime support for efficient software transactional memory. In ACM Conference on Programming Language Design and Implementation, pages 26--37, 2006.

Digital Library

[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]

{Boe05} Hans-J. Boehm. Threads cannot be implemented as a library. In PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, pages 261--268, New York, NY, USA, 2005. ACM Press.

Digital Library

[11]

{CCM+06} Brian D. Carlstrom, JaeWoong Chung, Austen McDonald, Hassan Chafi, Christos Kozyrakis, and Kunle Olukotun. The Atomos transactional programming language. In ACM Conference on Programming Language Design and Implementation, pages 1--13, 2006.

Digital Library

[12]

{FQ03} Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. In ACM Conference on Programming Language Design and Implementation, pages 338--349, June 2003.

Digital Library

[13]

{GLL+90} Kourosh Gharachorloo, Daniel Lenoski, James Laudon, Phillip Gibbons, Anoop Gupta, and John Hennessy. Memory consistency and event ordering in scalable shared-memory multiprocessors. In Proc. 17th Ann. Intl. Symp. on Computer Architecture, pages 15--26, May 1990.

Digital Library

[14]

{HCW+04} Lance Hammond, Brian D. Carlstrom, Vicky Wong, Ben Hertzberg, Mike Chen, Christos Kozyrakis, and Kunle Olukotun. Programming with transactional coherence and consistency (TCC). In International Conference on Architectural Support for Programming Languages and Operating Systems, pages 1--13, 2004.

Digital Library

[15]

{HF03} Tim Harris and Keir Fraser. Language Support for Lightweight Transactions. In Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '03), pages 388--402, Seattle, Washington, November 2003.

Digital Library

[16]

{HMJH05} Tim Harris, Simon Marlow, Simon Peyton Jones, and Maurice Herlihy. Composable memory transactions. In ACM Symposium on Principles and Practice of Parallel Programming, 2005.

Digital Library

[17]

{Hoa02} C. A. R. Hoare. Towards a Theory of Parallel Programming. The Origin of Concurrent Programming: From Semaphores to Remote Procedure Calls, pages 231--244, 2002.

Digital Library

[18]

{HPST06} Timothy Harris, Mark Plesko, Avraham Shinnar, and David Tarditi. Optimizing memory transactions. In ACM Conference on Programming Language Design and Implementation, pages 14--25, 2006.

Digital Library

[19]

{IPW01} Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396--450, 2001.

Digital Library

[20]

{Lam78} Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558--564, 1978.

Digital Library

[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]

{MCC+06} Austen McDonald, JaeWoong Chung, Brian D. Carlstrom, Chi Cao Minh, Hassan Chafi, Christos Kozyrakis, and Kunle Olukotun. Architectural semantics for practical transactional memory. In 33rd International Symposium on Computer Architecture, June 2006.

Digital Library

[24]

{MPA05} Jeremy Manson, William Pugh, and Sarita V. Adve. The Java Memory Model. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 378--391, New York, NY, USA, 2005. ACM Press.

Digital Library

[25]

{RG05} Michael F. Ringenburg and Dan Grossman. AtomCaml: First-class atomicity via rollback. In 10th ACM International Conference on Functional Programming, pages 92--104, September 2005.

Digital Library

[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]

{YGL01} Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom. Specifying Java thread semantics using a uniform memory model. In ACM Java Grande Conference, November 2001.

Digital Library

Cited By

Dongol BJagadeesan RRiely JHollingsworth JKeidar I(2019)Modular transactionsProceedings of the 24th Symposium on Principles and Practice of Parallel Programming10.1145/3293883.3295708(82-93)Online publication date: 16-Feb-2019
https://dl.acm.org/doi/10.1145/3293883.3295708
Chong NSorensen TWickerson J(2018)The semantics of transactions and weak memory in x86, Power, ARM, and C++ACM SIGPLAN Notices10.1145/3296979.319237353:4(211-225)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192373
Chong NSorensen TWickerson JFoster JGrossman D(2018)The semantics of transactions and weak memory in x86, Power, ARM, and C++Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192373(211-225)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192373
Show More Cited By

Index Terms

What do high-level memory models mean for transactions?
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Dynamic compilers
      2. Runtime environments
  2. Software organization and properties
    1. Contextual software domains
      1. Operating systems
        Memory management
        Garbage collection

Recommendations

Versioned boxes as the basis for memory transactions
Special issue: Synchronization and concurrency in object-oriented languages

In this paper, we propose the use of Versioned Boxes, which keep a history of values, as the basis for language-level memory transactions. Unlike previous work on software transactional memory, in our proposal read-only transactions never conflict with ...
Invalidating transactions: optimizations, theory, guarantees, and unification
Scheduling memory transactions in distributed systems

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

MSPC '06: Proceedings of the 2006 workshop on Memory system performance and correctness

October 2006

114 pages

ISBN:1595935789

DOI:10.1145/1178597

General Chair:
Antony Hosking
Purdue U
,
Program Chair:
Ali-Reza Adl-Tabatabai
Intel

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 October 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

MSPC '06

Sponsor:

SIGPLAN

MSPC '06: ACM SIGPLAN Workshop on Memory Systems Performance and Correctness 2006

October 22, 2006

California, San Jose

Acceptance Rates

Overall Acceptance Rate 6 of 20 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

66
Total Citations
View Citations
590
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Dongol BJagadeesan RRiely JHollingsworth JKeidar I(2019)Modular transactionsProceedings of the 24th Symposium on Principles and Practice of Parallel Programming10.1145/3293883.3295708(82-93)Online publication date: 16-Feb-2019
https://dl.acm.org/doi/10.1145/3293883.3295708
Chong NSorensen TWickerson J(2018)The semantics of transactions and weak memory in x86, Power, ARM, and C++ACM SIGPLAN Notices10.1145/3296979.319237353:4(211-225)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192373
Chong NSorensen TWickerson JFoster JGrossman D(2018)The semantics of transactions and weak memory in x86, Power, ARM, and C++Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192373(211-225)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192373
Dongol BJagadeesan RRiely J(2017)Transactions in relaxed memory architecturesProceedings of the ACM on Programming Languages10.1145/31581062:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158106
Marino DSingh AMillstein TMusuvathi MNarayanasamy S(2016)DRFxACM Transactions on Programming Languages and Systems10.1145/292598838:4(1-40)Online publication date: 15-Sep-2016
https://dl.acm.org/doi/10.1145/2925988
Bao WKrishnamoorthy SPouchet LRastello FSadayappan P(2016)PolyCheck: dynamic verification of iteration space transformations on affine programsACM SIGPLAN Notices10.1145/2914770.283765651:1(539-554)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837656
Swamy NHriţcu CKeller CRastogi ADelignat-Lavaud AForest SBhargavan KFournet CStrub PKohlweiss MZinzindohoue JZanella-Béguelin S(2016)Dependent types and multi-monadic effects in F*ACM SIGPLAN Notices10.1145/2914770.283765551:1(256-270)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837655
Drăgoi CHenzinger TZufferey D(2016)PSync: a partially synchronous language for fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/2914770.283765051:1(400-415)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837650
Kestor GUnsal OCristal ATasiran S(2015)TRADEACM Transactions on Parallel Computing10.1145/27860212:2(1-23)Online publication date: 8-Jul-2015
https://dl.acm.org/doi/10.1145/2786021
Cristal AOzkan BCohen EKestor GKuru IUnsal OTasiran SMutluergil SElmas T(2015)Verification Tools for Transactional ProgramsTransactional Memory. Foundations, Algorithms, Tools, and Applications10.1007/978-3-319-14720-8_14(283-306)Online publication date: 2015
https://doi.org/10.1007/978-3-319-14720-8_14
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten