Understanding POWER multiprocessors

Abstract : Exploiting today's multiprocessors requires high-performance and correct concurrent systems code (op-timising compilers, language runtimes, OS kernels, etc.), which in turn requires a good understanding of the observable processor behaviour that can be relied on. Unfortunately this Exploiting today’s multiprocessors requires high-performance and correct concurrent systems code (optimising compilers, language runtimes, OS kernels, etc.), which in turn requires a good understanding of the observable processor behaviour that can be relied on. Unfortunately this critical hardware/software interface is not at all clear for several current multiprocessors. In this paper we characterise the behaviour of IBM POWER multiprocessors, which have a subtle and highly relaxed memory model (ARM multiprocessors have a very similar architecture in this respect). We have conducted ex-tensive experiments on several generations of processors: POWER G5, 5, 6, and 7. Based on these, on published de-tails of the microarchitectures, and on discussions with IBM staff, we give an abstract-machine semantics that abstracts from most of the implementation detail but explains the be-haviour of a range of subtle examples. Our semantics is ex-plained in prose but defined in rigorous machine-processed mathematics; we also confirm that it captures the observ-able processor behaviour, or the architectural intent, for our examples with an executable checker. While not officially sanctioned by the vendor, we believe that this model gives a reasonable basis for reasoning about current POWER mul-tiprocessors. Our work should bring new clarity to concurrent systems programming for these architectures, and is a necessary precondition for any analysis or verification. It should also inform the design of languages such as C and C++, where the language memory model is constrained by what can be efficiently compiled to such multiprocessors.
Type de document :
Communication dans un congrès
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2011, San Jose, United States. 2011, 〈10.1145/1993498.1993520〉
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-01100824
Contributeur : Luc Maranget <>
Soumis le : vendredi 23 janvier 2015 - 16:54:38
Dernière modification le : mercredi 9 septembre 2015 - 01:04:40

Identifiants

Collections

Citation

Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams. Understanding POWER multiprocessors. PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2011, San Jose, United States. 2011, 〈10.1145/1993498.1993520〉. 〈hal-01100824〉

Partager

Métriques

Consultations de la notice

60