More Web Proxy on the site http://driver.im/

research-article

Exploiting the commutativity lattice

Authors:

Milind Kulkarni,

Dimitrios Prountzos,

Keshav PingaliAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 6

Pages 542 - 555

https://doi.org/10.1145/1993316.1993562

Published: 04 June 2011 Publication History

Abstract

Speculative execution is a promising approach for exploiting parallelism in many programs, but it requires efficient schemes for detecting conflicts between concurrently executing threads. Prior work has argued that checking semantic commutativity of method invocations is the right way to detect conflicts for complex data structures such as kd-trees. Several ad hoc ways of checking commutativity have been proposed in the literature, but there is no systematic approach for producing implementations.

In this paper, we describe a novel framework for reasoning about commutativity conditions: the commutativity lattice. We show how commutativity specifications from this lattice can be systematically implemented in one of three different schemes: abstract locking, forward gatekeeping and general gatekeeping. We also discuss a disciplined approach to exploiting the lattice to find different implementations that trade off precision in conflict detection for performance. Finally, we show that our novel conflict detection schemes are practical and can deliver speedup on three real-world applications.

References

[1]

Synthetic maximum flow families. http://www.avglab.com/andrew/CATS/maxflow_synthetic.htm.

[2]

A. Bondavalli, N. De Francesco, D. Latella, and G. Vaglini. Shared abstract data type: an algebraic methodology for their specification. In MFDBS 89, 1989.

Digital Library

[3]

J. Burnim, G. Necula, and K. Sen. Specifying and checking semantic atomicity for multithreaded programs. In ASPLOS'11: Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, 2011.

Digital Library

[4]

B. D. Carlstrom, A. McDonald, C. Kozyrakis, and K. Olukotun. Transactional collection classes. In PPoPP, 2007.

Digital Library

[5]

B. Demsky and P. Lam. Views: object-inspired concurrency control. In ICSE, 2010.

Digital Library

[6]

K. P. Eswaran, J. N. Gray, R. A. Lorie, and I. L. Traiger. The notions of consistency and predicate locks in a database system. Commun. ACM, 19(11):624--633, 1976.

Digital Library

[7]

A. V. Goldberg and R. E. Tarjan. A new approach to the maximum-flow problem. J. ACM, 35(4):921--940, 1988.

Digital Library

[8]

J. Gray and A. Reuter. Transaction Processing: Concepts and Techniques. Morgan Kaufmann Publishers Inc., 1992.

Digital Library

[9]

T. Harris and K. Fraser. Language support for lightweight transactions. In OOPSLA. Oct 2003.

Digital Library

[10]

M. Herlihy and E. Koskinen. Transactional boosting: a methodology for highly-concurrent transactional objects. In PPoPP, 2008.

Digital Library

[11]

M. Herlihy, V. Luchangco, and M. Moir. A flexible framework for implementing software transactional memory. In OOPSLA, 2006.

Digital Library

[12]

M. Herlihy and J. E. B. Moss. Transactional memory: architectural support for lock-free data structures. In ISCA, 1993.

Digital Library

[13]

M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. TOPLAS, 12(3):463--492, 1990.

Digital Library

[14]

D. Kim and M. Rinard. Verification of semantic commutativity conditions and inverse operations on linked data structures. In PLDI, 2011.

Digital Library

[15]

E. Koskinen, M. Parkinson, and M. Herlihy. Coarse-grained transactions. In POPL, 2010.

Digital Library

[16]

M. Kulkarni, M. Burtscher, R. Inkulu, K. Pingali, and C. Casçaval. How much parallelism is there in irregular applications? In PPoPP, 2009.

Digital Library

[17]

M. Kulkarni, K. Pingali, G. Ramanarayanan, B. Walter, K. Bala, and L. P. Chew. Optimistic parallelism benefits from data partitioning. In ASPLOS, 2008.

Digital Library

[18]

M. Kulkarni, K. Pingali, B. Walter, G. Ramanarayanan, K. Bala, and L. P. Chew. Optimistic parallelism requires abstractions. In PLDI, 2007.

Digital Library

[19]

J. Larus and R. Rajwar. Transactional Memory (Synthesis Lectures on Computer Architecture). Morgan & Claypool Publishers, 2007.

Digital Library

[20]

Y. Ni, V. Menon, A.-R. Adl-Tabatabai, A. L. Hosking, R. Hudson, J. E. B. Moss, B. Saha, and T. Shpeisman. Open nesting in software transactional memory. In PPoPP, 2007.

Digital Library

[21]

C. H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26(4):631--653, 1979.

Digital Library

[22]

L. Rauchwerger and D. Padua. The LRPD test: Speculative run-time parallelization of loops with privatization and reduction parallelization. In PLDI, 1995.

Digital Library

[23]

P. M. Schwarz and A. Z. Spector. Synchronizing shared abstract types. ACM Trans. Comput. Syst., 2(3):223--250, 1984.

Digital Library

[24]

B. Walter, K. Bala, M. Kulkarni, and K. Pingali. Fast agglomerative clustering for rendering. In Interactive Ray Tracing, 2008.

[25]

W. Weihl. Commutativity-based concurrency control for abstract data types. IEEE Transactions on Computers, 37(12), 1988.

Digital Library

Cited By

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
Shun J(2017)Priority Updates: A Contention-Reducing Primitive for Deterministic ProgrammingShared-Memory Parallelism Can Be Simple, Fast, and Scalable10.1145/3018787.3018794Online publication date: 9-Jun-2017
https://dl.acm.org/doi/10.1145/3018787.3018794
Show More Cited By

Index Terms

Exploiting the commutativity lattice
1. Computing methodologies
  1. Concurrent computing methodologies
    1. Concurrent programming languages
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Concurrent programming structures
      2. Language types
        Concurrent programming languages

Recommendations

Exploiting the commutativity lattice
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

Speculative execution is a promising approach for exploiting parallelism in many programs, but it requires efficient schemes for detecting conflicts between concurrently executing threads. Prior work has argued that checking semantic commutativity of ...
Exploiting semantic commutativity in hardware speculation
MICRO-49: The 49th Annual IEEE/ACM International Symposium on Microarchitecture

Hardware speculative execution schemes such as hardware transactional memory (HTM) enjoy low run-time overheads but suffer from limited concurrency because they rely on reads and writes to detect conflicts. By contrast, software speculation schemes can ...
Contract-based return-value commutativity: safely exploiting contract-based commutativity for faster serializable transactions
AGERE 2021: Proceedings of the 11th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control

A key challenge of designing distributed software systems is maintaining data consistency. We can define data consistency and data isolation guarantees --e.g. serializability-- in terms of schedules of atomic reads and writes, but this excludes ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 6

PLDI '11

June 2011

652 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1993316

Issue’s Table of Contents

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2011
668 pages
ISBN:9781450306638
DOI:10.1145/1993498
General Chair:
Mary Hall
University of Utah
,
Program Chair:
David Padua
University of Illinois at Urbana-Champaign

Copyright © 2011 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: 04 June 2011

Published in SIGPLAN Volume 46, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

58
Total Citations
View Citations
437
Total Downloads

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

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

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
Shun J(2017)Priority Updates: A Contention-Reducing Primitive for Deterministic ProgrammingShared-Memory Parallelism Can Be Simple, Fast, and Scalable10.1145/3018787.3018794Online publication date: 9-Jun-2017
https://dl.acm.org/doi/10.1145/3018787.3018794
Shun J(2017)Shared-Memory Parallelism Can Be Simple, Fast, and Scalable10.1145/3018787Online publication date: 9-Jun-2017
https://doi.org/10.1145/3018787
Chen YHong CSinha NWang B(2015)Commutativity of ReducersProceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 903510.1007/978-3-662-46681-0_9(131-146)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46681-0_9
Gehr TDimitrov DVechev M(2015)Learning Commutativity SpecificationsComputer Aided Verification10.1007/978-3-319-21690-4_18(307-323)Online publication date: 16-Jul-2015
https://doi.org/10.1007/978-3-319-21690-4_18
Gramoli VGuerraoui R(2014)Reusable Concurrent Data TypesProceedings of the 28th European Conference on ECOOP 2014 --- Object-Oriented Programming - Volume 858610.1007/978-3-662-44202-9_8(182-206)Online publication date: 1-Aug-2014
https://dl.acm.org/doi/10.1007/978-3-662-44202-9_8
Zakhour GWeisenburger PSalvaneschi G(2024)Automated Verification of Fundamental Algebraic LawsProceedings of the ACM on Programming Languages10.1145/36564088:PLDI(766-789)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656408
Chen AFathololumi PKoskinen EPincus J(2022)Veracity: declarative multicore programming with commutativityProceedings of the ACM on Programming Languages10.1145/35633496:OOPSLA2(1726-1756)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563349
De Porre KFerreira CPreguiça NGonzalez Boix E(2021)ECROs: building global scale systems from sequential codeProceedings of the ACM on Programming Languages10.1145/34854845:OOPSLA(1-30)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485484
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 Issue’s Table of Contents