Sarkar, Susmit and Sewell, Peter and Zappa Nardelli, Francesco and Owens, Scott and Ridge, Tom and Braibant, Thomas and Myreen, Magnus O. and Alglave, Jade (2009) The Semantics of x86-CC Multiprocessor Machine Code. In: POPL '09: 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 21st - 23rd, 2009, Savannah, Georgia, USA.
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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.
|Item Type:||Conference or workshop item (Paper)|
|Subjects:||Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,|
|Divisions:||Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group|
|Depositing User:||Scott Owens|
|Date Deposited:||24 Oct 2012 10:22|
|Last Modified:||18 Mar 2013 14:41|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/31907 (The current URI for this page, for reference purposes)|
- Depositors only (login required):