research-article

High-level small-step operational semantics for transactions

Authors:

Katherine F. Moore,

Dan GrossmanAuthors Info & Claims

ACM SIGPLAN Notices, Volume 43, Issue 1

Pages 51 - 62

https://doi.org/10.1145/1328897.1328448

Published: 07 January 2008 Publication History

Abstract

Software transactions have received significant attention as a way to simplify shared-memory concurrent programming, but insufficient focus has been given to the precise meaning of software transactions or their interaction with other language features. This work begins to rectify that situation by presenting a family of formal languages that model a wide variety of behaviors for software transactions. These languages abstract away implementation details of transactional memory, providing high-level definitions suitable for programming languages. We use small-step semantics in order to represent explicitly the interleaved execution of threads that is necessary to investigate pertinent issues.

We demonstrate the value of our core approach to modeling transactions by investigating two issues in depth. First, we consider parallel nesting, in which parallelism and transactions can nest arbitrarily. Second, we present multiple models for weak isolation, in which nontransactional code can violate the isolation of a transaction. For both, type-and-effect systems let us soundly and statically restrict what computation can occur inside or outside a transaction. We prove some key language-equivalence theorems to confirm that under sufficient static restrictions, in particular that each mutable memory location is used outside transactions or inside transactions (but not both), no program can determine whether the language implementation uses weak isolation or strong isolation.

References

[1]

Mart1n Abadi, Andrew Birrell, Tim Harris, and Michael Isard. Semantics of transactional memory and automatic mutual exclusion. In 35th ACM Symposium on Principles of Programming Languages, 2008.

Digital Library

[2]

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, 2006.

Digital Library

[3]

Kunal Agrawal, Charles E. Leiserson, and Jim Sukha. Memory models for open-nested transactions. In ACM SIGPLAN Workshop on Memory Systems Performance & Correctness, 2006.

Digital Library

[4]

Eric Allen, David Chase, Joe Hallet, Victor Luchangco, Jan-Willem Maessen, Sukyoung Ryu, Guy L. Steele Jr., and Sam Tobin-Hochstadt. The Fortress language specification, version 1.0beta, 2007. http://research.sun.com/projects/plrg/Publications/fortress1.0beta.pdf.

[5]

Colin Blundell, E Christopher Lewis, and Milo M. K. Martin. Subtleties of transactional memory atomicity semantics. Computer Architecture Letters, 5(2), 2006.

Digital Library

[6]

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, 2006.

Digital Library

[7]

Peter Damron, Alexandra Fedorova, Yossi Lev, Victor Luchangco, Mark Moir, and Daniel Nussbaum. Hybrid transactional memory. In International Conference on Architectural Support for Programming Languages and Operating Systems, 2006.

Digital Library

[8]

Cormac Flanagan and Martín Abadi. Types for safe locking. In European Symposium on Programming, volume 1576 of Lecture Notes in Computer Science, 1999.

Digital Library

[9]

Matteo Frigo and Victor Luchangco. Computation-centric memory models. In ACM Symposium on Parallel Algorithms and Architectures, 1998.

Digital Library

[10]

Dan Grossman, Jeremy Manson, and William Pugh. What do high-level memory models mean for transactions? In ACM SIGPLAN Workshop on Memory Systems Performance & Correctness, 2006.

Digital Library

[11]

Nicholas Haines, Darrell Kindred, J. Gregory Morrisett, Scott M. Nettles, and Jeannette M. Wing. Composing first-class transactions. ACM Trans. on Programming Languages and Systems, 16(6):1719--1736, 1994.

Digital Library

[12]

Tim Harris. Exceptions and side-effects in atomic blocks. In PODC Workshop on Concurrency and Synchronization in Java Programs, 2004.

[13]

Tim Harris and Keir Fraser. Language support for lightweight transactions. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2003.

Digital Library

[14]

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

[15]

Tim Harris, Mark Plesko, Avraham Shinnar, and David Tarditi. Optimizing memory transactions. In ACM Conference on Programming Language Design and Implementation, 2006.

Digital Library

[16]

Maurice Herlihy, Victor Luchangco, and Mark Moir. A flexible framework for implementing software transactional memory. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2006.

Digital Library

[17]

Richard Hudson, Bratin Saha, Ali-Reza Adl-Tabatabai, and Benjamin Hertzberg. McRT-Malloc: A scalable transactional memory allocator. In International Symposium on Memory Management, 2006.

Digital Library

[18]

Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. on Programming Languages and Systems, 23(3), 2001.

Digital Library

[19]

Suresh Jagannathan, Jan Vitek, Adam Welc, and Antony L. Hosking. A transactional object calculus. Science of Computer Programming, 57(2), 2005.

Digital Library

[20]

Aaron Kimball and Dan Grossman. Software transactions meet first-class continuations. In 8th Annual Workshop on Scheme and Functional Programming, 2007.

[21]

Sanjeev Kumar, Michael Chu, Christopher J. Hughes, Partha Kundu, and Anthony Nguyen. Hybrid transactional memory. In ACM Symposium on Principles and Practice of Parallel Programming, 2006.

Digital Library

[22]

James R. Larus and Ravi Rajwar. Transactional Memory. Morgan & Claypool Publishers, 2006.

[23]

Ben Liblit. An operational semantics for LogTM. Technical Report 1571, University of Wisconsin-Madison, 2006.

[24]

Jeremy Manson, William Pugh, and Sarita V. Adve. The Java memory model. In 32nd ACM Symposium on Principles of Programming Languages, 2005.

Digital Library

[25]

Virendra J. Marathe, William N. Scherer, and Michael L. Scott. Adaptive software transactional memory. In International Symposium on Distributed Computing, 2005.

Digital Library

[26]

Katherine F. Moore and Dan Grossman. High-level small-step operational semantics for transactions (technical companion). Technical report, Univ. of Wash. Dept. of Computer Science & Engineering, 2007. http://www.cs.washington.edu/homes/kfm/atomsfamily proofs.pdf.

[27]

Michelle J. Moravan, Jayaram Bobba, Kevin E. Moore, Luke Yen, Mark D. Hill, Ben Liblit, Michael M. Swift, and David A. Wood. Supporting nested transactional memory in LogTM. In 12th International Conference on Architectural Support for Programming Languages and Operating Systems, 2006.

Digital Library

[28]

J. Eliot B. Moss. Nested Transactions: An Approach to Reliable Distributed Computing. The MIT Press, 1985.

Digital Library

[29]

J. Eliot B. Moss and Antony L. Hosking. Nested transactional memory: Model and preliminary architecture sketches. In Synchronization and Concurrency in Object-Oriented Languages (SCOOL), 2005.

[30]

Michael F. Ringenburg and Dan Grossman. AtomCaml: First-class atomicity via rollback. In 10th ACM International Conference on Functional Programming, 2005.

Digital Library

[31]

Michael L. Scott. Sequential specification of transactional memory semantics. In Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT), 2006.

[32]

Tatiana Shpeisman, Vijay Menon, Ali-Reza Adl-Tabatabai, Steve Balensiefer, Dan Grossman, Richard Hudson, Katherine F. Moore, and Bratin Saha. Enforcing isolation and ordering in STM. In ACM Conference on Programming Language Design and Implementation, 2007.

Digital Library

[33]

Michael F. Spear, Virendra J. Marathe, Luke Dalessandro, and Michael L. Scott. Privatization techniques for software transactional memory. Technical Report 915, Computer Science Department, University of Rochester, 2007.

Digital Library

[34]

Jan Vitek, Suresh Jagannathan, Adam Welc, and Antony L. Hosking. A semantic framework for designer transactions. In European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, 2004.

[35]

Philip Wadler. The marriage of effects and monads. In 3rd ACM International Conference on Functional Programming, 1999.

Digital Library

[36]

Pawel T. Wojciechowski. Isolation-only transactions by typing and versioning. In ACM International Conference on Principles and Practice of Declarative Programming, 2005.

Digital Library

Cited By

Kallas KZhang HAlur RAngel SLiu V(2023)Executing Microservice Applications on Serverless, CorrectlyProceedings of the ACM on Programming Languages10.1145/35712067:POPL(367-395)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571206
Abe THiraishi T(2021)An Extensionally Equivalence-ensured Language for Task Parallel Processing with Backtracking-based Load BalancingJournal of Information Processing10.2197/ipsjjip.29.43429(434-448)Online publication date: 2021
https://doi.org/10.2197/ipsjjip.29.434
Zhang MHuang JCao MBond M(2015)Low-overhead software transactional memory with progress guarantees and strong semanticsACM SIGPLAN Notices10.1145/2858788.268851050:8(97-108)Online publication date: 24-Jan-2015
https://dl.acm.org/doi/10.1145/2858788.2688510
Show More Cited By

Index Terms

High-level small-step operational semantics for transactions

Recommendations

High-level small-step operational semantics for transactions
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Software transactions have received significant attention as a way to simplify shared-memory concurrent programming, but insufficient focus has been given to the precise meaning of software transactions or their interaction with other language features. ...
Enforcing isolation and ordering in STM
Proceedings of the 2007 PLDI conference

Transactional memory provides a new concurrency control mechanism that avoids many of the pitfalls of lock-based synchronization. High-performance software transactional memory (STM) implementations thus far provide weak atomicity: Accessing shared data ...
Enforcing isolation and ordering in STM
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

Transactional memory provides a new concurrency control mechanism that avoids many of the pitfalls of lock-based synchronization. High-performance software transactional memory (STM) implementations thus far provide weak atomicity: Accessing shared data ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 43, Issue 1

POPL '08

January 2008

420 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1328897

Issue’s Table of Contents

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2008
448 pages
ISBN:9781595936899
DOI:10.1145/1328438
General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

Copyright © 2008 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Published in SIGPLAN Volume 43, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

95
Total Citations
View Citations
944
Total Downloads

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

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kallas KZhang HAlur RAngel SLiu V(2023)Executing Microservice Applications on Serverless, CorrectlyProceedings of the ACM on Programming Languages10.1145/35712067:POPL(367-395)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571206
Abe THiraishi T(2021)An Extensionally Equivalence-ensured Language for Task Parallel Processing with Backtracking-based Load BalancingJournal of Information Processing10.2197/ipsjjip.29.43429(434-448)Online publication date: 2021
https://doi.org/10.2197/ipsjjip.29.434
Zhang MHuang JCao MBond M(2015)Low-overhead software transactional memory with progress guarantees and strong semanticsACM SIGPLAN Notices10.1145/2858788.268851050:8(97-108)Online publication date: 24-Jan-2015
https://dl.acm.org/doi/10.1145/2858788.2688510
Zhang MHuang JCao MBond MCohen AGrove D(2015)Low-overhead software transactional memory with progress guarantees and strong semanticsProceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/2688500.2688510(97-108)Online publication date: 24-Jan-2015
https://dl.acm.org/doi/10.1145/2688500.2688510
Dabrowski FLoulergue FPinsard T(2015)A formal semantics of nested atomic sections with thread escapeComputer Languages, Systems and Structures10.1016/j.cl.2015.04.00142:C(2-21)Online publication date: 1-Jul-2015
https://dl.acm.org/doi/10.1016/j.cl.2015.04.001
Bushkov VGuerraoui R(2015)Liveness in Transactional MemoryTransactional Memory. Foundations, Algorithms, Tools, and Applications10.1007/978-3-319-14720-8_2(32-49)Online publication date: 2015
https://doi.org/10.1007/978-3-319-14720-8_2
Lesani MPalsberg J(2013)Proving Non-opacityProceedings of the 27th International Symposium on Distributed Computing - Volume 820510.1007/978-3-642-41527-2_8(106-120)Online publication date: 14-Oct-2013
https://dl.acm.org/doi/10.1007/978-3-642-41527-2_8
Cheeseman LParkinson MClebsch SKogias MDrossopoulou SChisnall DWrigstad TLiétar P(2023)When Concurrency Matters: Behaviour-Oriented ConcurrencyProceedings of the ACM on Programming Languages10.1145/36228527:OOPSLA2(1531-1560)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622852
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
DiLorenzo JMancini KFisher KFoster N(2019)TxForest: A DSL for Concurrent FilestoresProgramming Languages and Systems10.1007/978-3-030-34175-6_17(332-354)Online publication date: 18-Nov-2019
https://doi.org/10.1007/978-3-030-34175-6_17
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 Issue’s Table of Contents