Understanding POWER multiprocessors

Exploiting today’s multiprocessors requires highperformance 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 e 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 mat...

• Type: Journal
• Year: 2011
• Where: PLDI
• Authors: Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams
• Keywords: Hardware Software Interface, Necessary Precondition, Os Kernels, PLDI 2011, Programming Languages