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

research-article

Repairing sequential consistency in C/C++11

Authors:

Viktor Vafeiadis,

Derek DreyerAuthors Info & Claims

PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 618 - 632

https://doi.org/10.1145/3062341.3062352

Published: 14 June 2017 Publication History

Abstract

The C/C++11 memory model defines the semantics of concurrent memory accesses in C/C++, and in particular supports racy "atomic" accesses at a range of different consistency levels, from very weak consistency ("relaxed") to strong, sequential consistency ("SC"). Unfortunately, as we observe in this paper, the semantics of SC atomic accesses in C/C++11, as well as in all proposed strengthenings of the semantics, is flawed, in that (contrary to previously published results) both suggested compilation schemes to the Power architecture are unsound. We propose a model, called RC11 (for Repaired C11), with a better semantics for SC accesses that restores the soundness of the compilation schemes to Power, maintains the DRF-SC guarantee, and provides stronger, more useful, guarantees to SC fences. In addition, we formally prove, for the first time, the correctness of the proposed stronger compilation schemes to Power that preserve load-to-store ordering and avoid "out-of-thin-air" reads.

References

[1]

C/C++11 mappings to processors, available at http://www. cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html. {Online; accessed 27-September-2016}.

[2]

Crossbeam: support for concurrent and parallel programming, available at https://github.com/aturon/crossbeam. {Online; accessed 24-October-2016}.

[3]

Supplementary material for this paper, available at http: //plv.mpi-sws.org/scfix/.

[4]

J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1–7:74, July 2014.

Digital Library

[5]

M. Batty, A. F. Donaldson, and J. Wickerson. Overhauling SC atomics in C11 and OpenCL. In POPL 2016, pages 634–648. ACM, 2016.

Digital Library

[6]

M. Batty, K. Memarian, K. Nienhuis, J. Pichon-Pharabod, and P. Sewell. The problem of programming language concurrency semantics. In ESOP 2015, pages 283–307. Springer, 2015.

[7]

M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell. Clarifying and compiling C/C++ concurrency: From C++11 to POWER. In POPL 2012, pages 509–520. ACM, 2012.

Digital Library

[8]

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In POPL 2011, pages 55–66. ACM, 2011.

Digital Library

[9]

H.-J. Boehm. Can seqlocks get along with programming language memory models? In MSPC 2012, pages 12–20. ACM, 2012.

Digital Library

[10]

H.-J. Boehm and S. V. Adve. Foundations of the C++ concurrency memory model. In PLDI 2008, pages 68–78. ACM, 2008.

Digital Library

[11]

H.-J. Boehm and B. Demsky. Outlawing ghosts: Avoiding out-of-thin-air results. In MSPC 2014, pages 7:1–7:6. ACM, 2014.

Digital Library

[12]

M. Dodds, M. Batty, and A. Gotsman. C/C++ causal cycles confound compositionality. TinyToCS, 2, 2013.

[13]

S. Flur, K. E. Gray, C. Pulte, S. Sarkar, A. Sezgin, L. Maranget, W. Deacon, and P. Sewell. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In POPL 2016, pages 608–621. ACM, 2016.

Digital Library

[14]

Intel. A formal specification of Intel Itanium processor family memory ordering, 2002. http://download.intel.com/ design/Itanium/Downloads/25142901.pdf. {Online; accessed 14-November-2016}.

[15]

A. Jeffrey and J. Riely. On thin air reads: Towards an event structures model of relaxed memory. In LICS 2016, pages 759–767. ACM, 2016.

Digital Library

[16]

J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis, and D. Dreyer. A promising semantics for relaxed-memory concurrency. In POPL 2017, pages 175–189. ACM, 2017.

Digital Library

[17]

O. Lahav, N. Giannarakis, and V. Vafeiadis. Taming releaseacquire consistency. In POPL 2016, pages 649–662. ACM, 2016.

Digital Library

[18]

O. Lahav and V. Vafeiadis. Owicki-Gries reasoning for weak memory models. In ICALP 2015, pages 311–323. Springer, 2015.

Digital Library

[19]

O. Lahav and V. Vafeiadis. Explaining relaxed memory models with program transformations. In FM 2016, pages 479–495. Springer, 2016.

[20]

L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690–691, 1979.

Digital Library

[21]

N. M. Lˆe, A. Pop, A. Cohen, and F. Zappa Nardelli. Correct and efficient work-stealing for weak memory models. In PPoPP 2013, pages 69–80. ACM, 2013.

[22]

Y. A. Manerkar, C. Trippel, D. Lustig, M. Pellauer, and M. Martonosi. Counterexamples and proof loophole for the C/C++ to POWER and ARMv7 trailing-sync compiler mappings. arXiv preprint arXiv:1611.01507, 2016.

[23]

L. Maranget, S. Sarkar, and P. Sewell. A tutorial introduction to the ARM and POWER relaxed memory models. http://www.cl.cam.ac.uk/˜pes20/ppc-supplemental/test7.pdf, 2012.

[24]

B. Norris and B. Demsky. CDSchecker: checking concurrent data structures written with C/C++ atomics. In OOPSLA 2013, pages 131–150. ACM, 2013.

Digital Library

[25]

S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86-TSO. In TPHOLs 2009, pages 391–407. Springer-Verlag, 2009.

Digital Library

[26]

J. Pichon-Pharabod and P. Sewell. A concurrency semantics for relaxed atomics that permits optimisation and avoids thinair executions. In POPL 2016, pages 622–633. ACM, 2016.

Digital Library

[27]

S. Sarkar, K. Memarian, S. Owens, M. Batty, P. Sewell, L. Maranget, J. Alglave, and D. Williams. Synchronising C/C++ and POWER. In PLDI 2012, pages 311–322. ACM, 2012.

Digital Library

[28]

D. Shasha and M. Snir. Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst., 10(2):282–312, Apr. 1988.

Digital Library

[29]

A. Turon, V. Vafeiadis, and D. Dreyer. GPS: Navigating weak memory with ghosts, protocols, and separation. In OOPSLA 2014, pages 691–707. ACM, 2014.

Digital Library

[30]

V. Vafeiadis, T. Balabonski, S. Chakraborty, R. Morisset, and F. Zappa Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In POPL 2015, pages 209–220. ACM, 2015.

Digital Library

[31]

V. Vafeiadis and C. Narayan. Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA 2013, pages 867–884. ACM, 2013.

Digital Library

[32]

J. Wickerson, M. Batty, T. Sorensen, and G. A. Constantinides. Automatically comparing memory consistency models. In POPL 2017, pages 190–204. ACM, 2017.

Digital Library

Cited By

Marmanis IKokologiannakis MVafeiadis V(2025)Model Checking C/C++ with Mixed-Size AccessesProceedings of the ACM on Programming Languages10.1145/37049119:POPL(2232-2252)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704911
Moiseenko EMeluzzi MMeleshchenko IKabashnyi IPodkopaev AChakraborty S(2025)Relaxed Memory Concurrency Re-executedProceedings of the ACM on Programming Languages10.1145/37049089:POPL(2149-2175)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704908
Golovin PKokologiannakis MVafeiadis V(2025)RELINCHE: Automatically Checking Linearizability under Relaxed Memory ConsistencyProceedings of the ACM on Programming Languages10.1145/37049069:POPL(2090-2117)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704906
Show More Cited By

Index Terms

Repairing sequential consistency in C/C++11
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Concurrent programming languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

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 ...
Repairing sequential consistency in C/C++11
PLDI '17

The C/C++11 memory model defines the semantics of concurrent memory accesses in C/C++, and in particular supports racy "atomic" accesses at a range of different consistency levels, from very weak consistency ("relaxed") to strong, sequential consistency ...
Efficient sequential consistency using conditional fences
PACT '10: Proceedings of the 19th international conference on Parallel architectures and compilation techniques

Among the various memory consistency models, the sequential consistency (SC) model, in which memory operations appear to take place in the order specified by the program, is the most intuitive and enables programmers to reason about their parallel ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2017

708 pages

ISBN:9781450349888

DOI:10.1145/3062341

General Chair:
Albert Cohen
Inria, France
,
Program Chair:
Martin Vechev
DeepCode, Switzerland / ETH Zurich, Switzerland

ACM SIGPLAN Notices Volume 52, Issue 6
PLDI '17
June 2017
708 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3140587
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2017 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: 14 June 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '17

Sponsor:

SIGPLAN

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

June 18 - 23, 2017

Barcelona, Spain

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

140
Total Citations
View Citations
948
Total Downloads

Downloads (Last 12 months)128
Downloads (Last 6 weeks)13

Reflects downloads up to 23 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Marmanis IKokologiannakis MVafeiadis V(2025)Model Checking C/C++ with Mixed-Size AccessesProceedings of the ACM on Programming Languages10.1145/37049119:POPL(2232-2252)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704911
Moiseenko EMeluzzi MMeleshchenko IKabashnyi IPodkopaev AChakraborty S(2025)Relaxed Memory Concurrency Re-executedProceedings of the ACM on Programming Languages10.1145/37049089:POPL(2149-2175)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704908
Golovin PKokologiannakis MVafeiadis V(2025)RELINCHE: Automatically Checking Linearizability under Relaxed Memory ConsistencyProceedings of the ACM on Programming Languages10.1145/37049069:POPL(2090-2117)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704906
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
Nagar KSahoo AChowdhury RJagannathan S(2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689802
Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
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
Park SKim JMulder IJung JLee JKrebbers RKang J(2024)A Proof Recipe for Linearizability in Relaxed Memory Separation LogicProceedings of the ACM on Programming Languages10.1145/36563848:PLDI(175-198)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656384
Bailleu MStavrakakis DRocha RChakraborty SGarg DBhatotia P(2024)Toast: A Heterogeneous Memory Management SystemProceedings of the 2024 International Conference on Parallel Architectures and Compilation Techniques10.1145/3656019.3676944(53-65)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1145/3656019.3676944
Margalit RChristakis MPradel M(2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685549
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