research-article

Safe optimisations for shared-memory concurrent programs

Author:

Jaroslav ŠevčíkAuthors Info & Claims

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

Pages 306 - 316

https://doi.org/10.1145/1993498.1993534

Published: 04 June 2011 Publication History

Abstract

Current proposals for concurrent shared-memory languages, including C++ and C, provide sequential consistency only for programs without data races (the DRF guarantee). While the implications of such a contract for hardware optimisations are relatively well-understood, the correctness of compiler optimisations under the DRF guarantee is less clear, and experience with Java shows that this area is error-prone.

In this paper we give a rigorous study of optimisations that involve both reordering and elimination of memory reads and writes, covering many practically important optimisations. We first define powerful classes of transformations semantically, in a language-independent trace semantics. We prove that any composition of these transformations is sound with respect to the DRF guarantee, and moreover that they provide basic security guarantees (no thin-air reads) even for programs with data races. To give a concrete example, we apply our semantic results to a simple imperative language and prove that several syntactic transformations are safe for that language. We also discuss some surprising limitations of the DRF guarantee.

References

[1]

S. V. Adve and M. D. Hill. Weak ordering --- a new definition. In ISCA'90, pages 2--14, 1990.

Digital Library

[2]

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

Digital Library

[3]

J. Alglave, A. Fox, S. Ishtiaq, M. O. Myreen, S. Sarkar, P. Sewell, and F. Zappa Nardelli. The semantics of Power and ARM multiprocessor machine code. In Proc. DAMP 2009, January 2009.

Digital Library

[4]

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T.Weber. Mathematizing C++ concurrency. In Proc. POPL, 2011.

Digital Library

[5]

P. Becker, editor. Programming Languages --- C++. Final Committee Draft. 2010. ISO/IEC JTC1 SC22 WG21 N3092.

[6]

Hans-J. Boehm and Sarita V. Adve. Foundations of the C++ concurrency memory model. In PLDI '08, pages 68--78, New York, NY, USA, 2008. ACM.

Digital Library

[7]

Gérard Boudol and Gustavo Petri. Relaxed memory models: an operational approach. In POPL '09, pages 392--403, 2009.

Digital Library

[8]

S. Burckhardt, M. Musuvathi, and V. Singh. Verifying local transformations on relaxed memory models. In CC '10, pages 104--123, 2010.

Digital Library

[9]

P. Cenciarelli, A. Knapp, and E. Sibilio. The Java memory model: Operationally, denotationally, axiomatically. In 16th ESOP, 2007.

Digital Library

[10]

J. Gosling, B. Joy, G. Steele, and G. Bracha. Java(TM) Language Specification, The (3rd Edition) (Java Series). Addison-Wesley Professional, July 2005.

Digital Library

[11]

Intel. A formal specification of Intel Itanium processor family memory ordering, 2002. Available from http://www.intel.com/design/ itanium/downloads/251429.htm.

[12]

P. Joisha, R. Schreiber, P. Banerjee, H.-J. Boehm, and D. Chakrabarti. A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code. Technical Report HPL-2010-81, HP Laboratories, 2010. To appear in POPL 2011.

Digital Library

[13]

Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558--565, 1978.

Digital Library

[14]

Doug Lea. The JSR-133 cookbook for compiler writers, 2008. http: //g.oswego.edu/dl/jmm/cookbook.html.

[15]

Jaejin Lee, David A. Padua, and Samuel P. Midkiff. Basic compiler algorithms for parallel programs. In PPOPP, pages 1--12. ACM, 1999.

Digital Library

[16]

J. Manson, W. Pugh, and S. Adve. The Java memory model. In POPL '05, pages 378--391, New York, NY, USA, 2005. ACM Press.

Digital Library

[17]

Samuel P. Midkiff and David A. Padua. Issues in the optimization of parallel programs. In ICPP (2), pages 105--113. Pennsylvania State University Press, 1990.

[18]

Vance Morrison. Understand the impact of low-lock techniques in multithreaded apps. MSDN Magazine, Oct 2005.

[19]

V. Saraswat, R. Jagadeesan, M. Michael, and C. von Praun. A theory of memory models. In PPoPP '07. ACM, Mar 2007.

Digital Library

[20]

S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Ridge, T. Braibant, M. Myreen, and J. Alglave. The semantics of x86-CC multiprocessor machine code. In POPL'09, January 2009.

Digital Library

[21]

J. Ševćík. Program Transformations in Weak Memory Models. PhD thesis, University of Edinburgh, Laboratory for Foundations of Computer Science, 2008.

[22]

J. Ševćík. The Sun Hotspot JVM does not conform with the Java memory model. Technical Report EDI-INF-RR-1252, School of Informatics, University of Edinburgh, 2008.

[23]

J. Ševćík and D. Aspinall. On validity of program transformations in the Java memory model. In ECOOP '08, pages 27--51, 2008.

Digital Library

[24]

Dennis Shasha and Marc Snir. Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst., 10(2):282--312, 1988.

Digital Library

[25]

Sparc International. Sparc architecture manual, version 9, 2000. Available from http://developers.sun.com/solaris/articles/ sparcv9.html.

Digital Library

[26]

Z. Sura, X. Fang, C. Wong, S. Midkiff, J. Lee, and D. Padua. Compiler techniques for high performance sequentially consistent Java programs. In PPoPP '05, pages 2--13, New York, NY, USA, 2005. ACM.

Digital Library

Cited By

Geeson LBrotherston JDijkstra WDonaldson ASmith LSorensen TWickerson J(2024)Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics ImplementationsProceedings of the ACM on Programming Languages10.1145/36897278:OOPSLA2(442-467)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689727
Gouicem RSprokholt DRuehl JRocha RSpink TChakraborty SBhatotia PAamodt TJerger NSwift M(2023)Risotto: A Dynamic Binary Translator for Weak Memory Model ArchitecturesProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3567955.3567962(107-122)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3567955.3567962
Zha JLiang HFeng XJhala RDillig I(2022)Verifying optimizations of concurrent programs in the promising semanticsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523734(903-917)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523734
Show More Cited By

Index Terms

Safe optimisations for shared-memory concurrent programs
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. General programming languages
      1. Language features
        Concurrent programming structures
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Safe optimisations for shared-memory concurrent programs
PLDI '11

Current proposals for concurrent shared-memory languages, including C++ and C, provide sequential consistency only for programs without data races (the DRF guarantee). While the implications of such a contract for hardware optimisations are relatively ...
Safe open-nested transactions through ownership
PPoPP '09

Researchers in transactional memory (TM) have proposed open nesting as a methodology for increasing the concurrency of transactional programs. The idea is to ignore ``low-level'' memory operations of an open-nested transaction when detecting conflicts ...
Safe open-nested transactions through ownership
PPoPP '09: Proceedings of the 14th ACM SIGPLAN symposium on Principles and practice of parallel programming

Researchers in transactional memory (TM) have proposed open nesting as a methodology for increasing the concurrency of transactional programs. The idea is to ignore ``low-level'' memory operations of an open-nested transaction when detecting conflicts ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

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

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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 June 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '11

Sponsor:

SIGPLAN

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

June 4 - 8, 2011

California, San Jose, USA

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

61
Total Citations
View Citations
549
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)1

Reflects downloads up to 05 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Geeson LBrotherston JDijkstra WDonaldson ASmith LSorensen TWickerson J(2024)Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics ImplementationsProceedings of the ACM on Programming Languages10.1145/36897278:OOPSLA2(442-467)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689727
Gouicem RSprokholt DRuehl JRocha RSpink TChakraborty SBhatotia PAamodt TJerger NSwift M(2023)Risotto: A Dynamic Binary Translator for Weak Memory Model ArchitecturesProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3567955.3567962(107-122)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3567955.3567962
Zha JLiang HFeng XJhala RDillig I(2022)Verifying optimizations of concurrent programs in the promising semanticsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523734(903-917)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523734
Rocha RSprokholt DFink MGouicem RSpink TChakraborty SBhatotia PJhala RDillig I(2022)Lasagne: a static binary translator for weak memory model architecturesProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523719(888-902)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523719
Cho MLee SLee DHur CLahav OJhala RDillig I(2022)Sequential reasoning for optimizing compilers under weak memory concurrencyProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523718(213-228)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523718
Gäher LSammler MSpies SJung RDang HKrebbers RKang JDreyer D(2022)Simuliris: a separation logic framework for verifying concurrent program optimizationsProceedings of the ACM on Programming Languages10.1145/34986896:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498689
Gopalakrishnan AVerbrugge C(2022)Reordering Under the ECMAScript Memory Consistency ModelLanguages and Compilers for Parallel Computing10.1007/978-3-030-95953-1_14(198-214)Online publication date: 16-Feb-2022
https://doi.org/10.1007/978-3-030-95953-1_14
Stein BNielsen BChang BMøller A(2019)Static analysis with demand-driven value refinementProceedings of the ACM on Programming Languages10.1145/33605663:OOPSLA(1-29)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360566
Pan RHu QXu GD'Antoni L(2019)Automatic repair of regular expressionsProceedings of the ACM on Programming Languages10.1145/33605653:OOPSLA(1-29)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360565
Vukotic IRahli VEsteves-Veríssimo P(2019)Asphalion: trustworthy shielding against Byzantine faultsProceedings of the ACM on Programming Languages10.1145/33605643:OOPSLA(1-32)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360564
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