Understanding POWER Multiprocessors

Susmit Sarkar*, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

158 Citations (Scopus)


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 extensive experiments on several generations of processors: POWER G5, 5, 6, and 7. Based on these, on published details 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 behaviour of a range of subtle examples. Our semantics is explained in prose but defined in rigorous machine-processed mathematics; we also confirm that it captures the observable 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 multiprocessors.

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.

Original languageEnglish
Pages (from-to)175-186
Number of pages12
JournalACM SIGPLAN Notices
Issue number6
Publication statusPublished - Jun 2011


  • Standardization
  • Documentation
  • Relaxed Memory Models
  • Reliability
  • Verification
  • Semantics
  • Theory
  • Languages


Dive into the research topics of 'Understanding POWER Multiprocessors'. Together they form a unique fingerprint.

Cite this