Sarkar, S; Sewell, P; Nardelli, FZ; Owens, S; Ridge, T; Braibant, T; ... Alglave, J; + view all Sarkar, S; Sewell, P; Nardelli, FZ; Owens, S; Ridge, T; Braibant, T; Myreen, MO; Alglave, J; - view fewer (2009) The semantics of x86-CC multiprocessor machine code. Conference Record of the Annual ACM Symposium on Principles of Programming Languages 379 - 391. 10.1145/1480881.1480929.
Full text not available from this repository.
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 > Faculty of Engineering Science > Computer Science|
Archive Staff Only: edit this record