The semantics of x86-CC multiprocessor machine code

Susmit Sarkar*, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract

Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous prose, leading to widespread confusion. We develop a rigorous and accurate semantics for x86 multiprocessor programs, from instruction decoding to relaxed memory model, mechanised in HOL. We test the semantics against actual processors and the vendor litmus-test examples, and give an equivalent abstract-machine characterisation of our axiomatic memory model. For programs that are (in some precise sense) data-race free, we prove in HOL that their behaviour is sequentially consistent. We also contrast the x86 model with some aspects of Power and ARM behaviour. This provides a solid intuition for low-level programming, and a sound foundation for future work on verification, static analysis, and compilation of low-level concurrent code.
Original languageEnglish
Pages (from-to)379-391
Number of pages13
JournalACM SIGPLAN Notices
Volume44
Issue number1
DOIs
Publication statusPublished - 21 Jan 2009

Keywords

  • Standardization
  • Documentation
  • Relaxed Memory Models
  • Reliability
  • Verification
  • Models
  • Shared-memory
  • Semantics
  • Theory

Fingerprint

Dive into the research topics of 'The semantics of x86-CC multiprocessor machine code'. Together they form a unique fingerprint.

Cite this