The semantics of power and ARM multiprocessor machine code
Jade Alglave, Anthony C. J. Fox, Samin S. Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli · 2009
We develop a rigorous semantics for Power and ARM multi-processor programs, including their relaxed memory model and the behaviour of reasonable fragments of their instruc-tion 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 seman- tics, for the design and compilation of high-level concurrent languages.C ©2009 ACM.