Understanding POWER Multiprocessors

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

158 Citations (Scopus)

Abstract

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
Title of host publicationPLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION
Place of PublicationNEW YORK
PublisherACM
Pages175-186
Number of pages12
ISBN (Print)978-1-4503-0663-8
Publication statusPublished - 2011
Event32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 11) - San Jose, Canada
Duration: 4 Jun 20118 Jun 2011

Conference

Conference32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 11)
Country/TerritoryCanada
CitySan Jose
Period4/06/118/06/11

Keywords

  • MICROARCHITECTURE
  • Relaxed Memory Models
  • MODELS
  • SHARED-MEMORY
  • Semantics

Fingerprint

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

Cite this