Synchronising C/C++ and POWER

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 sanc-tioned 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, in-cluding 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 con-fidence in the C/C++ model in its own terms, fixing some omis-sions and contributing to the C standards committee adoption of the C++11 concurrency model.
Type de document :
Communication dans un congrès
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2012, Beijing, China. 2012, 〈10.1145/2254064.2254102〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01100798
Contributeur : Luc Maranget <>
Soumis le : vendredi 23 janvier 2015 - 16:11:28
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : vendredi 24 avril 2015 - 10:05:56

Fichier

top2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, et al.. Synchronising C/C++ and POWER. PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2012, Beijing, China. 2012, 〈10.1145/2254064.2254102〉. 〈hal-01100798〉

Partager

Métriques

Consultations de la notice

248

Téléchargements de fichiers

138