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.
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01100824
Contributor : Luc Maranget <>
Submitted on : Friday, January 23, 2015 - 4:54:38 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM

Links full text

Identifiers

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. ⟨10.1145/1993498.1993520⟩. ⟨hal-01100824⟩

Share

Metrics

Record views

118