The Semantics of Multiprocessor Machine Code: x86, Power, and ARM

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 prose, leading to widespread confusion.

We have developed rigorous and accurate semantics for multiprocessor programs above three architectures: x86, Power, and ARM. Each covers the relaxed memory model, instruction semantics, and instruction decoding, for fragments of the instruction sets, and is mechanized in HOL. This 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.

For x86, we test the semantics against actual processors and the vendor litmus-test examples, and give an equivalent abstract-machine characterisation of our axiomatic memory model. We prove that the memory model is equivalent to a simpler (`nice execution') definition. For programs that are, in some precise sense, data-race free, we prove in HOL that their behaviour is sequentially consistent. The model is, to the best of our knowledge, consistent with the current Intel and AMD documentation [Intel 64 and IA-32 Architectures Software Developer's Manual, April 2008 (vol 1,2A,2B; rev.27) and Feb. 2008 (vol.3A,3B; rev.26); Intel 64 Architecture Memory Ordering White Paper, Aug. 2007; AMD64 Architecture Programmer's Manual, Sept. 2007].

The Power and ARM architectures have a very different memory model to x86, but are very similar to each other. Our semantics is, to the best of our knowledge, consistent with the Power 2.05 specification and the ARM Architecture Reference Manual v7. Here the core memory model is also formalised in Coq.

Papers

• The Semantics of x86 Multiprocessor Machine Code (draft paper; revised version to appear in POPL 2009)
• Supplementary Examples (additional illustrations and discussion for the examples in the above, and a brief informal-mathematics summary of the x86 axiomatic memory model)
• The Semantics of Power and ARM Multiprocessor Machine Code (draft paper)

Code

• The x86 HOL sources: to browse and download (gzipped tarball).
• The x86 HOL definitions, typeset: in ps and in pdf
• The Power and ARM HOL sources: to browse and download (gzipped tarball).
• The Power and ARM HOL definitions, typeset: in ps and in pdf
• The Power and ARM Coq sources: to browse and download (gzipped tarball).

Tools

• memevents
• x86 litmus
• x86sem (gzipped tarball)

Experimental data

• From the x86 litmus memory model testing: summary and details.
• From the x86sem sequential testing: results

People

• Anthony Fox
• Magnus Myreen
• Scott Owens
• Tom Ridge
• Susmit Sarkar
• Peter Sewell

(Computer Laboratory, University of Cambridge)

• Jade Alglave
• Thomas Braibant
• Francesco Zappa Nardelli

(INRIA Paris-Rocquencourt)

• Samin Ishtiaq

(Microsoft Research Cambridge)