The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

The semantics of power and ARM multiprocessor machine code

The work

AuthorsJade Alglave; Anthony C. J. Fox; Samin S. Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli
Editors
Typemisc
Year2009
Citekeyalglave2009semantics

Where it appeared

Pages13--24

Identifiers

DOI10.1145/1481839.1481842
OpenAlexW2110879934

Access

Landing pagehttps://doi.org/10.1145/1481839.1481842

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

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 ©2009 ACM.

How it got here

How it got hereagent via openalex
Added2026-10-26 12:17 UTC
Not denied bya person 2026-10-29 17:12 UTC

Filed under

petersewell

Cite it as

@misc{alglave2009semantics,
  title        = {The semantics of power and ARM multiprocessor machine code},
  author       = {Jade Alglave and Anthony C. J. Fox and Samin S. Ishtiaq and Magnus O. Myreen and Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli},
  year         = {2009},
  pages        = {13--24},
  doi          = {10.1145/1481839.1481842},
}

This record lives at https://refs.drheap.org/alglave2009semantics/ and will keep doing so.