The Semantics of Power and ARM Multiprocessor Programs

Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous (and sometimes flawed) prose, leading to widespread confusion.

We are working to develop mathematically rigorous and usable semantics for multiprocessor programs, focussing on three architectures: x86 (Intel 64/IA-32 and AMD64), Power, and ARM. Such models should provide a solid intuition for low-level programming, and a sound foundation for future work on verification, static analysis, and compilation of low-level concurrent code, and for the design of high-level concurrent programming languages.

This work is associated with a broader project on Relaxed-Memory Concurrency.

Power and ARM

The Power and ARM architectures have very different memory models to x86, but are broadly similar to each other. For Power, we have produced several models. Our PLDI 2011 paper gives an abstract-machine model that, to the best of our knowledge, accurately captures the architectural intent and observable processor behaviour for a wide range of subtle examples. The TACAS 2011 tool paper describes our Litmus experimental testing tool. The CAV 2010 paper gives an earlier axiomatic model that is sound with respect to current POWER processor behaviour, as far as we know, but does not match the architectural intent for some examples (as described in the PLDI 2011 paper). It is based on a general framework developed in Alglave's thesis. The DAMP 2009 paper gives a very preliminary axiomatic model, based on a naive reading of the Power and ARM vendor documentation.

Supplementary Material

Our preliminary DAMP 09 semantics was based on the Power 2.05 specification and the ARM Architecture Reference Manual v7.

Our CAV 2010 model was based primarily on empirical testing using a new tool suite; it includes theoretical results on the fences required to strengthen executions in the model.

People

Computer Laboratory, University of Cambridge:

INRIA Paris-Rocquencourt:

IBM:

  • Derek Williams

Microsoft Research Cambridge:

  • Samin Ishtiaq

Funding

We acknowledge funding from the EPSRC (grants EP/H005633/1 and EP/F036345), the INRIA equipes associees MM, and ANR grant ANR-06-SETI-010-02.

an x86-CC example execution

[validate]