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

research-article

Modular data-race-freedom guarantees in the promising semantics

Authors:

Ori LahavAuthors Info & Claims

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 867 - 882

https://doi.org/10.1145/3453483.3454082

Published: 18 June 2021 Publication History

Abstract

Local data-race-freedom guarantees, ensuring strong semantics for locations accessed by non-racy instructions, provide a fruitful methodology for modular reasoning in relaxed memory concurrency. We observe that standard compiler optimizations are in inherent conflict with such guarantees in general fully-relaxed memory models. Nevertheless, for a certain strengthening of the promising model by Lee et al. that only excludes relaxed RMW-store reorderings, we establish multiple useful local data-racefreedom guarantees that enhance the programmability aspect of the model.We also demonstrate that the performance price of forbidding these reorderings is insignificant. To the best of our knowledge, these results are the first to identify a model that includes the standard concurrency constructs, supports the efficient mapping of relaxed reads and writes to plain hardware loads and stores, and yet validates several local data-race-freedom guarantees. To gain confidence, our results are fully mechanized in Coq.

References

[1]

2021. Coq development and supplementary material for this paper. https://sf.snu.ac.kr/promising-ldrf

[2]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018. Optimal Stateless Model Checking Under the Release-acquire Semantics. Proc. ACM Program. Lang., 2, OOPSLA (2018), Article 135, Oct., 29 pages. issn:2475-1421 https://doi.org/10.1145/3276505

Digital Library

[3]

Sarita V. Adve and Mark D. Hill. 1990. Weak Ordering–a New Definition. In ISCA. ACM, New York, NY, USA. 2–14. isbn:0-89791-366-3 https://doi.org/10.1145/325164.325100

Digital Library

[4]

Arm. 2020. Arm A64 Instruction Set Architecture Armv8 (DDI0596 2020-12). https://developer.arm.com/documentation/ddi0596/2020-12

[5]

Mark Batty, Mike Dodds, and Alexey Gotsman. 2013. Library Abstraction for C/C++ Concurrency. In POPL. ACM, New York, NY, USA. 235–248. isbn:9781450318327 https://doi.org/10.1145/2429069.2429099

Digital Library

[6]

Mark Batty, Alastair F. Donaldson, and John Wickerson. 2016. Overhauling SC Atomics in C11 and OpenCL. In POPL. ACM, New York, NY, USA. 634–648. isbn:9781450335492 https://doi.org/10.1145/2837614.2837637

Digital Library

[7]

Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015. The Problem of Programming Language Concurrency Semantics. In ESOP. Springer, Berlin, Heidelberg. 283–307. http://dx.doi.org/10.1007/978-3-662-46669-8_12

[8]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In POPL. ACM, New York, NY, USA. 55–66. isbn:978-1-4503-0490-0 https://doi.org/10.1145/1926385.1926394

Digital Library

[9]

John Bender and Jens Palsberg. 2019. A Formalization of Java’s Concurrent Access Modes. Proc. ACM Program. Lang., 3, OOPSLA (2019), 142:1–142:28. https://doi.org/10.1145/3360568

Digital Library

[10]

Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. 2012. Concurrent Library Correctness on the TSO Memory Model. In ESOP. Springer, Berlin, Heidelberg. 87–107. isbn:978-3-642-28869-2

[11]

2021. http://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html

[12]

Soham Chakraborty and Viktor Vafeiadis. 2019. Grounding Thin-Air Reads with Event Structures. Proc. ACM Program. Lang., 3, POPL (2019), Article 70, Jan., 28 pages. issn:2475-1421 https://doi.org/10.1145/3290383

Digital Library

[13]

Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2019. RustBelt Meets Relaxed Memory. Proc. ACM Program. Lang., 4, POPL (2019), Article 34, Dec., 29 pages. https://doi.org/10.1145/3371102

Digital Library

[14]

Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. 2019. Verifying C11 Programs Operationally. In PPoPP. ACM, New York. 355–365. isbn:978-1-4503-6225-2 https://doi.org/10.1145/3293883.3295702

Digital Library

[15]

Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy. 2018. Bounding Data Races in Space and Time. In PLDI. ACM, New York, NY, USA. 242–255. isbn:9781450356985 https://doi.org/10.1145/3192366.3192421

Digital Library

[16]

Brijesh Dongol, Radha Jagadeesan, and James Riely. 2019. Modular Transactions: Bounding Mixed Races in Space and Time. In PPoPP. ACM, New York, NY, USA. 82–93. isbn:9781450362252 https://doi.org/10.1145/3293883.3295708

Digital Library

[17]

Brijesh Dongol, Radha Jagadeesan, James Riely, and Alasdair Armstrong. 2018. On Abstraction and Compositionality for Weak-Memory Linearisability. In VMCAI. Springer International Publishing, Cham. 183–204. isbn:978-3-319-73721-8

[18]

Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA. In POPL. ACM, New York, NY, USA. 608–621. isbn:978-1-4503-3549-2 https://doi.org/10.1145/2837614.2837615

Digital Library

[19]

Radha Jagadeesan, Alan Jeffrey, and James Riely. 2020. Pomsets with Preconditions: A Simple Model of Relaxed Memory. Proc. ACM Program. Lang., 4, OOPSLA (2020), Article 194, Nov., 30 pages. https://doi.org/10.1145/3428262

Digital Library

[20]

Alan Jeffrey and James Riely. 2019. On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory. Logical Methods in Computer Science, 15, 1 (2019), https://doi.org/10.23638/LMCS-15(1:33)2019

[21]

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 17:1–17:29. isbn:978-3-95977-035-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ECOOP.2017.17

[22]

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxed-Memory Concurrency. In POPL. ACM, New York, NY, USA. 175–189. isbn:978-1-4503-4660-3 https://doi.org/10.1145/3009837.3009850

Digital Library

[23]

Max Khiszinsky. 2020. CDS C++ Library. https://github.com/khizmax/libcds

[24]

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2017. Effective Stateless Model Checking for C/C++ Concurrency. Proc. ACM Program. Lang., 2, POPL (2017), Article 17, Dec., 32 pages. issn:2475-1421 https://doi.org/10.1145/3158105

Digital Library

[25]

Ori Lahav. 2019. Verification under Causally Consistent Shared Memory. ACM SIGLOG News, 6, 2 (2019), April, 43–56. https://doi.org/10.1145/3326938.3326942

Digital Library

[26]

Ori Lahav and Udi Boker. 2020. Decidable Verification under a Causally Consistent Shared Memory. In PLDI. ACM, New York, NY, USA. 211–226. isbn:9781450376136 https://doi.org/10.1145/3385412.3385966

Digital Library

[27]

Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016. Taming Release-acquire Consistency. In POPL. ACM, New York, NY, USA. 649–662. isbn:978-1-4503-3549-2 https://doi.org/10.1145/2837614.2837643

Digital Library

[28]

Ori Lahav and Roy Margalit. 2019. Robustness Against Release/Acquire Semantics. In PLDI. ACM, New York, NY, USA. 126–141. isbn:978-1-4503-6712-7 https://doi.org/10.1145/3314221.3314604

Digital Library

[29]

Ori Lahav and Viktor Vafeiadis. 2015. Owicki-Gries Reasoning for Weak Memory Models. In ICALP. Springer, Berlin, Heidelberg. 311–323. https://doi.org/10.1007/978-3-662-47666-6_25

Digital Library

[30]

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing Sequential Consistency in C/C++11. In PLDI. ACM, New York, NY, USA. 618–632. isbn:978-1-4503-4988-8 https://doi.org/10.1145/3062341.3062352

Digital Library

[31]

Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, and Viktor Vafeiadis. 2020. Promising 2.0: Global Optimizations in Relaxed Memory Concurrency. In PLDI. ACM, New York, NY, USA. 362–376. isbn:9781450376136 https://doi.org/10.1145/3385412.3386010

Digital Library

[32]

Jeremy Manson, William Pugh, and Sarita V. Adve. 2005. The Java Memory Model. In POPL. ACM, New York, NY, USA. 378–391. isbn:158113830X https://doi.org/10.1145/1040305.1040336

Digital Library

[33]

Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, and Satish Narayanasamy. 2016. DRFx: An Understandable, High Performance, and Flexible Memory Model for Concurrent Languages. ACM Trans. Program. Lang. Syst., 38, 4 (2016), Article 16, Sept., 40 pages. issn:0164-0925 https://doi.org/10.1145/2925988

Digital Library

[34]

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. 2020. Reconciling Event Structures with Modern Multiprocessors. In ECOOP. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 5:1–5:26. isbn:978-3-95977-154-2 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ECOOP.2020.5

[35]

Peizhao Ou and Brian Demsky. 2018. Towards Understanding the Costs of Avoiding Out-of-Thin-Air Results. Proc. ACM Program. Lang., 2, OOPSLA (2018), Article 136, Oct., 29 pages. https://doi.org/10.1145/3276506

Digital Library

[36]

Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A Better x86 Memory Model: x86-TSO. In TPHOLs. Springer, Berlin, Heidelberg. 391–407. isbn:978-3-642-03358-2 https://doi.org/10.1007/978-3-642-03359-9_27

Digital Library

[37]

Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, and Mark Batty. 2020. Modular Relaxed Dependencies in Weak Memory Concurrency. In ESOP. Springer, Cham. 599–625. https://doi.org/10.1007/978-3-030-44914-8_22

Digital Library

[38]

Jean Pichon-Pharabod and Peter Sewell. 2016. A Concurrency Semantics for Relaxed Atomics That Permits Optimisation and Avoids Thin-air Executions. In POPL. ACM, New York, NY, USA. 622–633. isbn:978-1-4503-3549-2 https://doi.org/10.1145/2837614.2837616

Digital Library

[39]

Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2019. Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. Proc. ACM Program. Lang., 3, POPL (2019), Article 69, Jan., 31 pages. issn:2475-1421 https://doi.org/10.1145/3290382

Digital Library

[40]

Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. 2019. On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models. Proc. ACM Program. Lang., 3, POPL (2019), Article 68, Jan., 31 pages. https://doi.org/10.1145/3290381

Digital Library

[41]

Matthew D. Sinclair, Johnathan Alsop, and Sarita V. Adve. 2017. Chasing Away RAts: Semantics and Evaluation for Relaxed Atomics on Heterogeneous Systems. In ISCA. ACM, New York, NY, USA. 161–174. isbn:9781450348928 https://doi.org/10.1145/3079856.3080206

Digital Library

[42]

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. 2015. Common Compiler Optimisations Are Invalid in the C11 Memory Model and What We Can Do About It. In POPL. ACM, New York, NY, USA. 209–220. isbn:978-1-4503-3300-9 https://doi.org/10.1145/2676726.2676995

Digital Library

[43]

Jaroslav Ševčík and David Aspinall. 2008. On Validity of Program Transformations in the Java Memory Model. In ECOOP. Springer-Verlag, Berlin, Heidelberg. 27–51. https://doi.org/10.1007/978-3-540-70592-5_3

Digital Library

[44]

Yang Zhang and Xinyu Feng. 2016. An Operational Happens-before Memory Model. Front. Comput. Sci., 10, 1 (2016), Feb., 54–81. issn:2095-2228 https://doi.org/10.1007/s11704-015-4492-4

Digital Library

Cited By

Chappe NHenrio LZakowski YStark KTimany ABlazy STabareau N(2025)Monadic Interpreters for Concurrent Memory ModelsProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705890(283-298)Online publication date: 10-Jan-2025
https://dl.acm.org/doi/10.1145/3703595.3705890
Lee SCho MMargalit RHur CLahav O(2023)Putting Weak Memory in Order via a Promising Intermediate RepresentationProceedings of the ACM on Programming Languages10.1145/35912977:PLDI(1872-1895)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591297
Singh ALahav O(2023)An Operational Approach to Library Abstraction under Relaxed Memory ConcurrencyProceedings of the ACM on Programming Languages10.1145/35712467:POPL(1542-1572)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571246
Show More Cited By

Index Terms

Modular data-race-freedom guarantees in the promising semantics
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Models of computation
    1. Concurrency
  2. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Putting Weak Memory in Order via a Promising Intermediate Representation

We investigate the problem of developing an "in-order" shared-memory concurrency model for languages like C and C++, which executes instructions following their program order, and is thus more amenable to reasoning and verification compared to recent ...
A promising semantics for relaxed-memory concurrency
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Despite many years of research, it has proven very difficult to develop a memory model for concurrent programming languages that adequately balances the conflicting desiderata of programmers, compilers, and hardware. In this paper, we propose the first ...
Sequential reasoning for optimizing compilers under weak memory concurrency
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

We formally show that sequential reasoning is adequate and sufficient for establishing soundness of various compiler optimizations under weakly consistent shared-memory concurrency. Concretely, we introduce a sequential model and show that behavioral ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2021

1341 pages

ISBN:9781450383912

DOI:10.1145/3453483

General Chair:
Stephen N. Freund
Williams College, USA
,
Program Chair:
Eran Yahav
Technion, Israel

Copyright © 2021 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: 18 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Alon fellowship
Israel Science Foundation

Conference

PLDI '21

Sponsor:

SIGPLAN

PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 20 - 25, 2021

Virtual, Canada

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
199
Total Downloads

Downloads (Last 12 months)33
Downloads (Last 6 weeks)2

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Chappe NHenrio LZakowski YStark KTimany ABlazy STabareau N(2025)Monadic Interpreters for Concurrent Memory ModelsProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705890(283-298)Online publication date: 10-Jan-2025
https://dl.acm.org/doi/10.1145/3703595.3705890
Lee SCho MMargalit RHur CLahav O(2023)Putting Weak Memory in Order via a Promising Intermediate RepresentationProceedings of the ACM on Programming Languages10.1145/35912977:PLDI(1872-1895)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591297
Singh ALahav O(2023)An Operational Approach to Library Abstraction under Relaxed Memory ConcurrencyProceedings of the ACM on Programming Languages10.1145/35712467:POPL(1542-1572)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571246
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
Jeffrey ARiely JBatty MCooksey SKaysin IPodkopaev A(2022)The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrencyProceedings of the ACM on Programming Languages10.1145/34987166:POPL(1-30)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498716
Moiseenko EPodkopaev AKoznov D(2021)A Survey of Programming Language Memory ModelsProgramming and Computing Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
https://dl.acm.org/doi/10.1134/S0361768821060050

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