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; Myreen, MO; (2009) The semantics of x86-CC multiprocessor machine code. In: (pp. pp. 379-391).

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.

Type: Proceedings paper
Title: The semantics of x86-CC multiprocessor machine code
ISBN-13: 9781605583792
DOI: 10.1145/1480881.1480929
URI: http://discovery.ucl.ac.uk/id/eprint/1366410
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item