BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Fences and Stability in Weak Memory Models - Jade Alglave\, Univer
 sity of Oxford
DTSTART:20110520T090000Z
DTEND:20110520T100000Z
UID:TALK31481@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:We present a class of relaxed memory models\, defined in Coq\,
  parameterised by the chosen permitted local reorderings of reads and writ
 es\, and the visibility of inter- and intra-processor communications throu
 gh memory (e.g. store atomicity relaxation).  Based on this class of model
 s we develop a tool\, diy\, that systematically and automatically generate
 s and runs litmus tests to determine properties of processor implementatio
 ns.  We detail the results of our experiments on Power and the model we ba
 se on them. This work identified a rare implementation error in Power 5 me
 mory barriers (for which IBM is providing a workaround)\; our results also
  suggest that Power 6 does not suffer from this problem.\n\nWe prove resul
 ts on the required behaviour and placement of synchronisation primitives t
 o restore a given model\, such as Sequential Consistency (SC)\, from a wea
 ker one. We implemented these results in our offence tool\, which places e
 ither lock-based or lock-free synchronisation in a x86 or Power program to
  ensure what we call its stability\, i.e. it behaves as if running on SC.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR