research-article

The Push/Pull model of transactions

Authors:

Matthew ParkinsonAuthors Info & Claims

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 186 - 195

https://doi.org/10.1145/2737924.2737995

Published: 03 June 2015 Publication History

Abstract

We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics in which concurrent transactions PUSH their effects into the shared view (or UNPUSH to recall effects) and PULL the effects of potentially uncommitted concurrent transactions into their local view (or UNPULL to detangle). Each operation comes with simple criteria given in terms of commutativity (Lipton's left-movers and right-movers). The benefit of this model is that most of the elaborate reasoning (coinduction, simulation, subtle invariants, etc.) necessary for proving the serializability of a transactional algorithm is already proved within the semantic model. Thus, proving serializability (or opacity) amounts simply to mapping the algorithm on to our rules, and showing that it satisfies the rules' criteria.

References

[1]

A BADI, M., B IRRELL, A., H ARRIS, T., AND I SARD, M. Semantics of transactional memory and automatic mutual exclusion. In The 35th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages (POPL’08) (2008), pp. 63–74.

Digital Library

[2]

B URCKHARDT, S., AND L EIJEN, D. Semantics of concurrent revisions. In Proceedings of the 20th European Symposium on Programming (ESOP’11) (2011), G. Barthe, Ed., vol. 6602, pp. 116–135.

Digital Library

[3]

B USHKOV, V., G UERRAOUI, R., AND K APALKA, M. On the liveness of transactional memory. In Proceedings of the Symposium on Principles of Distributed Computing (DISC’12) (2012), pp. 9–18.

Digital Library

[4]

C HEREM, S., C HILIMBI, T. M., AND G ULWANI, S. Inferring locks for atomic sections. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI’08) (2008), pp. 304–315.

Digital Library

[5]

C OHEN, A., P NUELI, A., AND Z UCK, L. D. Mechanical verification of transactional memories with non-transactional memory accesses. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV’08) (2008), vol. 5123, pp. 121–134.

Digital Library

[6]

D ICE, D., S HALEV, O., AND S HAVIT, N. Transactional Locking II. In Proceedings of the 20th International Symposium on Distributed Computing (DISC’06) (September 2006).

Digital Library

[7]

D IMITROV, D., R AYCHEV, V., V ECHEV, M., AND K OSKINEN, E. Commutativity race detection. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14), Edinburgh, UK (2014).

Digital Library

[8]

F ELBER, P., F ETZER, C., AND R IEGEL, T. Dynamic performance tuning of word-based software transactional memory. In Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP ’08) (2008), pp. 237–246.

Digital Library

[9]

F ELBER, P., K ORLAND, G., AND S HAVIT, N. Deuce: Noninvasive concurrency with a Java STM. In Electronic Proceedings of the workshop on Programmability Issues for Multi-Core Computers (MULTIPROG) (2010).

[10]

G UERRAOUI, R., AND K APALKA, M. On the correctness of transactional memory. In Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’08) (2008), ACM, pp. 175–184.

Digital Library

[11]

H ERLIHY, M., AND K OSKINEN, E. Transactional boosting: A methodology for highly concurrent transactional objects. In Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’08) (2008).

Digital Library

[12]

H ERLIHY, M., AND K OSKINEN, E. Composable transactional objects: A position paper. In Proceedings of the 23rd European Symposium on Programming Languages and Systems (ESOP’14) (2014), vol. 8410, pp. 1–7.

Digital Library

[13]

H ERLIHY, M., L UCHANGCO, V., M OIR, M., AND S CHERER, III, W. N. Software transactional memory for dynamic-sized data structures. In Proceedings of the 22nd annual symposium on Principles of distributed computing (PODC’03) (2003), pp. 92–101.

Digital Library

[14]

H ERLIHY, M., AND M OSS, J. E. B. Transactional memory: Architectural support for lock-free data structures. In Proceedings of the 20th Annual International Symposium on Computer Architecture (ISCA’93) (1993), pp. 289–300.

Digital Library

[15]

IBM. Alphaworks Software Transactional Memory Compiler. http: //ibm.biz/alphaworks-stm-compiler.

[16]

I NTEL. Transactional synchronization in haswell. http: //software.intel.com/en-us/blogs/2012/02/07/ transactional-synchronization-in-haswell.

[17]

K IM, D., AND R INARD, M. C. Verification of semantic commutativity conditions and inverse operations on linked data structures. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’11) (2011), pp. 528– 541.

Digital Library

[18]

K OSKINEN, E., AND H ERLIHY, M. Checkpoints and continuations instead of nested transactions. In Proceedings of the 20th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA’08) (2008), pp. 160–168.

Digital Library

[19]

K OSKINEN, E., AND P ARKINSON, M. The push/pull model of transactions {extended version}. Tech. Rep. RC25529, IBM Research, 2015.

[20]

K OSKINEN, E., P ARKINSON, M. J., AND H ERLIHY, M. Coarsegrained transactions. In Proceedings of the 37th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL’10) (2010), ACM, pp. 19–30.

Digital Library

[21]

K ULKARNI, M., P INGALI, K., W ALTER, B., R AMANARAYANAN, G., B ALA, K., AND C HEW, L. P. Optimistic parallelism requires abstractions. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI’07) (2007), pp. 211–222.

Digital Library

[22]

L ESANI, M., L UCHANGCO, V., AND M OIR, M. A framework for formally verifying software transactional memory algorithms. In Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR’12) (2012), vol. 7454, pp. 516–530.

Digital Library

[23]

L ESANI, M., AND P ALSBERG, J. Communicating memory transactions. In Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’11) (2011), pp. 157–168.

Digital Library

[24]

L ESANI, M., AND P ALSBERG, J. Decomposing opacity. In Proceedings of the 28th International Symposium on Distributed Computing (DISC’14) (2014), pp. 391–405.

[25]

L IPTON, R. J. Reduction: a method of proving properties of parallel programs. Commun. ACM 18, 12 (1975), 717–721.

Digital Library

[26]

L YNCH, N. A., AND T UTTLE, M. R. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing (PODC’87) (1987), pp. 137–151.

Digital Library

[27]

M ATVEEV, A., AND S HAVIT, N. Towards a fully pessimistic STM model. In Proceedings of the 2012 Workshop on Transactional Memory (TRANSACT12) (2012).

[28]

M OORE, K. F., AND G ROSSMAN, D. High-level small-step operational semantics for transactions. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL’08) (2008), pp. 51–62.

Digital Library

[29]

M ORAVAN, M. J., B OBBA, J., M OORE, K. E., Y EN, L., H ILL, M. D., L IBLIT, B., S WIFT, M. M., AND W OOD, D. A. Supporting nested transactional memory in logTM. SIGOPS Operating Systems Review 40, 5 (2006), 359–370.

Digital Library

[30]

N I, Y., M ENON, V. S., A DL -T ABATABAI, A.-R., H OSKING, A. L., H UDSON, R. L., M OSS, J. E. B., S AHA, B., AND S HPEISMAN, T. Open nesting in software transactional memory. In Proceedings of the 12th ACM SIGPLAN symposium on Principles and Practice of Parallel Programming (PPoPP’07) (2007), pp. 68–78.

Digital Library

[31]

P APADIMITRIOU, C. The serializability of concurrent database updates. Journal of the ACM (JACM) 26, 4 (1979), 631–653.

Digital Library

[32]

R AMADAN, H. E., R OY, I., H ERLIHY, M., AND W ITCHEL, E. Committing conflicting transactions in an stm. In Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP ’09) (2009), pp. 163–172.

Digital Library

[33]

R IEGEL, T., F ETZER, C., AND F ELBER, P. Time-based transactional memory with scalable time bases. In Proceedings of the 19th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA’07) (2007), pp. 221–228.

Digital Library

[34]

S AHA, B., A DL -T ABATABAI, A.-R., H UDSON, R. L., M INH, C. C., AND H ERTZBERG, B. McRT-STM: a high performance software transactional memory system for a multi-core runtime. In Proceedings of the 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’06) (2006), pp. 187–197.

Digital Library

[35]

S PEAR, M., D ALESSANDRO, L., M ARATHE, V., AND S COTT, M. A comprehensive strategy for contention management in software transactional memory. In Proceedings of the 14th ACM SIGPLAN Symposium on Principles and practice of parallel programming (PPoPP’09) (2009).

Digital Library

[36]

S PEAR, M. F., M ARATHE, V. J., D ALESSANDRO, L., AND S COTT, M. L. Privatization techniques for software transactional memory. In Proceedings of the 26th Annual ACM Symposium on Principles of Distributed Computing (PODC’07) (2007), pp. 338–339.

Digital Library

[37]

W ANG, A., G AUDET, M., W U, P., A MARAL, J. N., O HMACHT, M., B ARTON, C., S ILVERA, R., AND M ICHAEL, M. Evaluation of blue gene/q hardware support for transactional memories. In Proceedings of the 21st International Conference on Parallel Architectures and Compilation Techniques (2012), pp. 127–136.

Digital Library

[38]

W EIHL, W. E. Data-dependent concurrency control and recovery (extended abstract). In Proceedings of the 2nd annual ACM symposium on Principles of Distributed Computing (PODC’83) (1983), ACM Press, pp. 63–75.

Digital Library

[39]

W ELC, A., S AHA, B., AND A DL -T ABATABAI, A.-R. Irrevocable transactions and their applications. In Proceedings of the 20th Annual Symposium on Parallelism in Algorithms and Architectures (SPAA’08) (2008), ACM, pp. 285–296. Introduction Overview Language and Atomic Semantics The Push/Pull Model Serializability Implementations Implementations That Are Yet to Come Related Work Conclusions and Future Work

Digital Library

Cited By

Popovic MPopovic MKordic BZhu H(2023)Complete formal verification of the PSTM transaction SchedulerComputer Science and Information Systems10.2298/CSIS210908058P20:1(307-327)Online publication date: 2023
https://doi.org/10.2298/CSIS210908058P
Sharma NSharma SSharma VUtkarsh ABharadwaj G(2021)An Algorithm for Concurrency control in Transactions for E-WalletInternational Journal of Innovative Technology and Exploring Engineering10.35940/ijitee.E8677.041062110:6(1-4)Online publication date: 30-Apr-2021
https://doi.org/10.35940/ijitee.E8677.0410621
Honoré WKim JShin JShao Z(2021)Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systemsProceedings of the ACM on Programming Languages10.1145/34854745:OOPSLA(1-31)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485474
Show More Cited By

Index Terms

The Push/Pull model of transactions

Recommendations

The Push/Pull model of transactions
PLDI '15

We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics in which concurrent transactions PUSH their effects into the shared view ...
Coarse-grained transactions
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Traditional transactional memory systems suffer from overly conservative conflict detection, yielding so-called false conflicts, because they are based on fine-grained, low-level read/write conflicts. In response, the recent trend has been toward ...
Coarse-grained transactions
POPL '10

Traditional transactional memory systems suffer from overly conservative conflict detection, yielding so-called false conflicts, because they are based on fine-grained, low-level read/write conflicts. In response, the recent trend has been toward ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2015

630 pages

ISBN:9781450334686

DOI:10.1145/2737924

General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

ACM SIGPLAN Notices Volume 50, Issue 6
PLDI '15
June 2015
630 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2813885
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 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: 03 June 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NSF CCF

Conference

PLDI '15

Sponsor:

SIGPLAN

PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 13 - 17, 2015

OR, Portland, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
341
Total Downloads

Downloads (Last 12 months)30
Downloads (Last 6 weeks)9

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Popovic MPopovic MKordic BZhu H(2023)Complete formal verification of the PSTM transaction SchedulerComputer Science and Information Systems10.2298/CSIS210908058P20:1(307-327)Online publication date: 2023
https://doi.org/10.2298/CSIS210908058P
Sharma NSharma SSharma VUtkarsh ABharadwaj G(2021)An Algorithm for Concurrency control in Transactions for E-WalletInternational Journal of Innovative Technology and Exploring Engineering10.35940/ijitee.E8677.041062110:6(1-4)Online publication date: 30-Apr-2021
https://doi.org/10.35940/ijitee.E8677.0410621
Honoré WKim JShin JShao Z(2021)Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systemsProceedings of the ACM on Programming Languages10.1145/34854745:OOPSLA(1-31)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485474
Popovic MPopovic MKordic BZhu H(2021)PSTM Transaction Scheduler Verification Based on CSP and Testing7th Conference on the Engineering of Computer Based Systems10.1145/3459960.3459962(1-10)Online publication date: 26-May-2021
https://dl.acm.org/doi/10.1145/3459960.3459962
Koskinen EBansal K(2021)Decomposing Data Structure Commutativity Proofs with $$m\!n$$-DifferencingVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_5(81-103)Online publication date: 12-Jan-2021
https://doi.org/10.1007/978-3-030-67067-2_5
Bansal KKoskinen ETripp O(2020)Synthesizing Precise and Useful Commutativity ConditionsJournal of Automated Reasoning10.1007/s10817-020-09573-wOnline publication date: 29-Aug-2020
https://doi.org/10.1007/s10817-020-09573-w
Popovic MPopovic MGhilezan SKordic B(2019)Formal Verification of Python Software Transactional Memory Serializability Based on the Push/Pull Semantic ModelProceedings of the 6th Conference on the Engineering of Computer Based Systems10.1145/3352700.3352706(1-8)Online publication date: 2-Sep-2019
https://dl.acm.org/doi/10.1145/3352700.3352706
Dickerson TGazzillo PHerlihy MKoskinen E(2019)Adding concurrency to smart contractsDistributed Computing10.1007/s00446-019-00357-zOnline publication date: 6-Jul-2019
https://doi.org/10.1007/s00446-019-00357-z
Dickerson TKoskinen EGazzillo PHerlihy M(2019)Conflict Abstractions and Shadow Speculation for Optimistic Transactional ObjectsProgramming Languages and Systems10.1007/978-3-030-34175-6_16(313-331)Online publication date: 18-Nov-2019
https://doi.org/10.1007/978-3-030-34175-6_16
Banerjee KChouksey RKarfa CKalita PChaudron MCrnkovic IChechik MHarman M(2018)Automatic detection of inverse operations while avoiding loop unrollingProceedings of the 40th International Conference on Software Engineering: Companion Proceeedings10.1145/3183440.3195083(175-176)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3183440.3195083
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.

Media

Figures

Other

Tables

View Table of Contents