The semantics of power and aRM multiprocessor machine code

Jade Alglave*, Anthony Fox, Ishtiaq Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

56 Citations (Scopus)

Abstract

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

Original languageEnglish
Title of host publicationProceedings of the 4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09
Pages13-24
Number of pages12
DOIs
Publication statusPublished - 2009
Event4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09 - Savannah, GA, United States
Duration: 20 Jan 200920 Jan 2009

Publication series

NameProceedings of the 4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09

Conference

Conference4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09
Country/TerritoryUnited States
CitySavannah, GA
Period20/01/0920/01/09

Keywords

  • ARM
  • Pow-erPC
  • Relaxed Memory Models
  • Semantics

Fingerprint

Dive into the research topics of 'The semantics of power and aRM multiprocessor machine code'. Together they form a unique fingerprint.

Cite this