The semantics of power and ARM multiprocessor machine code

We develop a rigorous semantics for Power and ARM multiprocessor programs, including their relaxed memory model and the behaviour of reasonable fragments of their instruction sets. The semantics is mechanised in the HOL proof assistant. This should provide a good basis for informal reasoning and formal verification of low-level code for these weakly consistent architectures, and, together with our x86 semantics, for the design and compilation of high-level concurrent languages.

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli
• Keywords: ARM Multiprocessor Programs, HOL Proof Assistant, POPL 2009, Programming Languages, Weakly Consistent Architectures