TY - GEN
T1 - The semantics of power and aRM multiprocessor machine code
AU - Alglave, Jade
AU - Fox, Anthony
AU - Samin Ishtiaq, Ishtiaq
AU - Myreen, Magnus O.
AU - Sarkar, Susmit
AU - Sewell, Peter
AU - Nardelli, Francesco Zappa
PY - 2009
Y1 - 2009
N2 - 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
AB - 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
KW - ARM
KW - Pow-erPC
KW - Relaxed Memory Models
KW - Semantics
UR - http://www.scopus.com/inward/record.url?scp=67650691299&partnerID=8YFLogxK
U2 - 10.1145/1481839.1481842
DO - 10.1145/1481839.1481842
M3 - Conference contribution
AN - SCOPUS:67650691299
SN - 9781605584171
T3 - Proceedings of the 4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09
SP - 13
EP - 24
BT - Proceedings of the 4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09
T2 - 4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09
Y2 - 20 January 2009 through 20 January 2009
ER -