- view fewer
The semantics of x86-CC multiprocessor machine code.
(pp. pp. 379-391).
Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is as-sumed 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 re-laxed memory model, mechanised in HOL. We test the se-mantics against actual processors and the vendor litmus-test examples, and give an equivalent abstract-machine charac- terisation 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.c©2009 ACM.
|Title:||The semantics of x86-CC multiprocessor machine code|
|UCL classification:||UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
Archive Staff Only