UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

The semantics of x86-CC multiprocessor machine code

Sarkar, S; Sewell, P; Nardelli, FZ; Owens, S; Ridge, T; Braibant, T; ... Alglave, J; + view all (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