research-article

Synchronising C/C++ and POWER

Authors:

Kayvan Memarian,

Derek WilliamsAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 6

Pages 311 - 322

https://doi.org/10.1145/2345156.2254102

Published: 11 June 2012 Publication History

Abstract

Shared memory concurrency relies on synchronisation primitives: compare-and-swap, load-reserve/store-conditional (aka LL/SC), language-level mutexes, and so on. In a sequentially consistent setting, or even in the TSO setting of x86 and Sparc, these have well-understood semantics. But in the very relaxed settings of IBM®, POWER®, ARM, or C/C++, it remains surprisingly unclear exactly what the programmer can depend on.

This paper studies relaxed-memory synchronisation. On the hardware side, we give a clear semantic characterisation of the load-reserve/store-conditional primitives as provided by POWER multiprocessors, for the first time since they were introduced 20 years ago; we cover their interaction with relaxed loads, stores, barriers, and dependencies. Our model, while not officially sanctioned by the vendor, is validated by extensive testing, comparing actual implementation behaviour against an oracle generated from the model, and by detailed discussion with IBM staff. We believe the ARM semantics to be similar.

On the software side, we prove sound a proposed compilation scheme of the C/C++ synchronisation constructs to POWER, including C/C++ spinlock mutexes, fences, and read-modify-write operations, together with the simpler atomic operations for which soundness is already known from our previous work; this is a first step in verifying concurrent algorithms that use load-reserve/store-conditional with respect to a realistic semantics. We also build confidence in the C/C++ model in its own terms, fixing some omissions and contributing to the C standards committee adoption of the C++11 concurrency model.

References

[1]

S. V. Adve andM. D. Hill. Weak ordering---a new definition. In Proc. ISCA, 1990.

Digital Library

[2]

J. Alglave and L. Maranget. Stability in weak memory models. In Proc. CAV, 2011.

Digital Library

[3]

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models. In Proc. CAV, 2010.

Digital Library

[4]

H.-J. Boehm and S.V. Adve. Foundations of the C++ concurrency memory model. In Proc. PLDI, 2008.

Digital Library

[5]

P. Becker, editor. Programming Languages --- C++. 2011. ISO/IEC 14882:2011. A non-final but recent version is available at http://www.open-std.org/jtc1/sc22/ wg21/docs/papers/2011/n3242.pdf.

[6]

M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell. Clarifying and compiling C/C++ concurrency: from C++11 to POWER. In Proc. POPL, 2012. http://www.cl.cam.ac. uk/~pes20/cppppc/.

Digital Library

[7]

H.-J. Boehm. Threads cannot be implemented as a library. In Proc. PLDI, 2005.

Digital Library

[8]

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

Digital Library

[9]

Supplementary material. http://www.cl.cam.ac.uk/users/pes20/cppppc-supplemental.

[10]

F. Corella, J. M. Stone, and C. M. Barton. A formal specification of the PowerPC shared memory architecture. Technical Report RC18638, IBM, 1993.

[11]

M. Herlihy. A methodology for implementing highly concurrent data objects. TOPLAS, 15(5):745--770, Nov 1993.

Digital Library

[12]

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

[13]

Programming Languages --- C. 2011. ISO/IEC 9899:2011. A non-final but recent version is available at http://www. open-std.org/jtc1/sc22/wg14/docs/n1539.pdf.

[14]

E. H. Jensen, G. W. Hagensen, and J. M. Broughton. A new approach to exclusive data access in shared memory multiprocessors. (Technical Report UCRL-97663), Nov 1987.

[15]

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

Digital Library

[16]

P. E. McKenney. {patch rfc tip/core/rcu 0/28} preview of rcu changes for 3.3, November 2011. https://lkml.org/lkml/2011/11/2/363.

[17]

M. M. Michael. Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst., 15:491--504, June 2004.

Digital Library

[18]

P. E. McKenney and R. Silvera. Example POWER implementation for C/C++ memory model. http: //www.rdrop.com/users/paulmck/scalability/paper/N2745r.2011.03.04a.html, 2011.

[19]

S. Owens, P. Böhm, F. Zappa Nardelli, and P. Sewell. Lem: A lightweight tool for heavyweight semantics. In Proc. ITP, LNCS 6898, 2011. Rough Diamond" section.

Digital Library

[20]

M. Parkinson, R. Bornat, and P. O'Hearn. Modular verification of a non-blocking stack. In Proc. POPL, 2007.

Digital Library

[21]

Power ISA Version 2.06. IBM, 2009.

[22]

J. Ševčík. Safe optimisations for shared-memory concurrent programs. In Proc. PLDI, 2011.

Digital Library

[23]

D. Shasha and M. Snir. Efficient and correct execution of parallel programs that share memory. TOPLAS, 10:282--312, 1988.

Digital Library

[24]

S. Sarkar, P. Sewell, J. Alglave, L.Maranget, and D. Williams. Understanding POWER multiprocessors. In PLDI, 2011

Digital Library

Cited By

Moiseenko EPodkopaev AKoznov D(2021)A Survey of Programming Language Memory ModelsProgramming and Computer Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
https://doi.org/10.1134/S0361768821060050
Bender JPalsberg J(2019)A formalization of Java’s concurrent access modesProceedings of the ACM on Programming Languages10.1145/33605683:OOPSLA(1-28)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360568
MALEEHUAN PCHIBA YAOKI T(2018)A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT SolverIEICE Transactions on Information and Systems10.1587/transinf.2018EDP7099E101.D:12(3038-3058)Online publication date: 1-Dec-2018
https://doi.org/10.1587/transinf.2018EDP7099
Show More Cited By

Index Terms

Synchronising C/C++ and POWER

Recommendations

Synchronising C/C++ and POWER
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation

Shared memory concurrency relies on synchronisation primitives: compare-and-swap, load-reserve/store-conditional (aka LL/SC), language-level mutexes, and so on. In a sequentially consistent setting, or even in the TSO setting of x86 and Sparc, these ...
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 ...
Mathematizing C++ concurrency
POPL '11

Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 6

PLDI '12

June 2012

534 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2345156

Issue’s Table of Contents

PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2012
572 pages
ISBN:9781450312059
DOI:10.1145/2254064
General Chairs:
Jan Vitek
Purdue University
,
Haibo Lin
Microsoft China
,
Program Chair:
Frank Tip
IBM T.J. Watson Research Center

Copyright © 2012 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: 11 June 2012

Published in SIGPLAN Volume 47, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

78
Total Citations
View Citations
460
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Moiseenko EPodkopaev AKoznov D(2021)A Survey of Programming Language Memory ModelsProgramming and Computer Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
https://doi.org/10.1134/S0361768821060050
Bender JPalsberg J(2019)A formalization of Java’s concurrent access modesProceedings of the ACM on Programming Languages10.1145/33605683:OOPSLA(1-28)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360568
MALEEHUAN PCHIBA YAOKI T(2018)A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT SolverIEICE Transactions on Information and Systems10.1587/transinf.2018EDP7099E101.D:12(3038-3058)Online publication date: 1-Dec-2018
https://doi.org/10.1587/transinf.2018EDP7099
Batty M(2017)Compositional relaxed concurrencyPhilosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences10.1098/rsta.2015.0406375:2104(20150406)Online publication date: 4-Sep-2017
https://doi.org/10.1098/rsta.2015.0406
Doko MVafeiadis V(2017)Tackling Real-Life Relaxed Concurrency with FSL++Programming Languages and Systems10.1007/978-3-662-54434-1_17(448-475)Online publication date: 19-Mar-2017
https://doi.org/10.1007/978-3-662-54434-1_17
Pirkelbauer PMilewicz RGonzalez J(2016)A Portable Lock-Free Bounded QueueAlgorithms and Architectures for Parallel Processing10.1007/978-3-319-49583-5_4(55-73)Online publication date: 25-Nov-2016
https://doi.org/10.1007/978-3-319-49583-5_4
Abdulla PAtig MJonsson BLeonardsson C(2016)Stateless Model Checking for POWERComputer Aided Verification10.1007/978-3-319-41540-6_8(134-156)Online publication date: 13-Jul-2016
https://doi.org/10.1007/978-3-319-41540-6_8
Le HGuthrie GWilliams DMichael MFrey BStarke WMay COdaira RNakaike T(2015)Transactional memory support in the IBM POWER8 processorIBM Journal of Research and Development10.1147/JRD.2014.238019959:1(8:1-8:14)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1147/JRD.2014.2380199
Hoefler TDinan JThakur RBarrett BBalaji PGropp WUnderwood K(2015)Remote Memory Access Programming in MPI-3ACM Transactions on Parallel Computing10.1145/27805842:2(1-26)Online publication date: 29-Jun-2015
https://dl.acm.org/doi/10.1145/2780584
de Vilhena PLahav OVafeiadis VRaad A(2024)Extending the C/C++ Memory Model with Inline AssemblyProceedings of the ACM on Programming Languages10.1145/36897498:OOPSLA2(1081-1107)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689749
Show More Cited By

View Options

Get Access

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