The Semantics of Power and ARM Multiprocessor Machine Code
- Jade Alglave ,
- Anthony Fox ,
- Samin Ishtiaq ,
- Magnus O. Myreen ,
- Susmit Sarkar ,
- Peter Sewell ,
- Francesco Zappa Nardelli
Workshop on Declarative Aspects of Multicore Programming |
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.