BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Semantics of x86-CC Multiprocessor Machine Code\n - Susmit Sar
 kar (University of Cambridge)
DTSTART:20081125T130000Z
DTEND:20081125T140000Z
UID:TALK13426@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Susmit Sarkar (1)\, Peter Sewell (1)\, Francesco Zappa Nardell
 i (2)\, Scott Owens (1)\, Tom Ridge (1)\, Thomas Braibant (2)\, Magnus O. 
 Myreen (1)\, Jade Alglave (2)\n\n(1) University of Cambridge\n(2) INRIA \n
 \nMultiprocessors are now dominant\, but real multiprocessors do not provi
 de the sequentially consistent memory that is assumed by most work on sema
 ntics and verification.  Instead\, they have subtle relaxed (or weak) memo
 ry models\, usually described only in ambiguous prose\, leading to widespr
 ead confusion.\n\nWe develop a rigorous semantics for x86 multiprocessor p
 rograms\, as described by the current Intel and AMD informal specification
 s\, from instruction decoding to relaxed memory model. Our semantics is me
 chanised in HOL. We test the semantics against actual processors and the v
 endor litmus-test examples\, and give an equivalent abstract-machine chara
 cterisation of our axiomatic memory model. For programs that are (in some 
 precise sense) data-race free\, we prove in HOL that their behaviour is se
 quentially consistent.  \n\nSuch models are needed to provide a solid intu
 ition for low-level programming\, and a sound foundation for future work o
 n verification\, static analysis\, and compilation of low-level concurrent
  code.\n\nHowever\, it now appears that the current informal specification
 s are not useful descriptions of the real processors. We discuss examples 
 showing that they are both too weak and not sound\, and speculate about ho
 w they should be improved.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR