The Semantics of x86-CC Multiprocessor Machine Code

Add to your list(s) Download to your calendar using vCal

• Susmit Sarkar (University of Cambridge)
• Tuesday 25 November 2008, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

Susmit Sarkar (1), Peter Sewell (1), Francesco Zappa Nardelli (2), Scott Owens (1), Tom Ridge (1), Thomas Braibant (2), Magnus O. Myreen (1), Jade Alglave (2)

(1) University of Cambridge (2) INRIA

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 semantics for x86 multiprocessor programs, as described by the current Intel and AMD informal specifications, from instruction decoding to relaxed memory model. Our semantics is 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.

Such models are needed to provide 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.

However, it now appears that the current informal specifications are not useful descriptions of the real processors. We discuss examples showing that they are both too weak and not sound, and speculate about how they should be improved.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.