BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Checking microarchitectural implementations of weak memory  - Dani
 el Lustig\, Princeton University
DTSTART:20141208T100000Z
DTEND:20141208T110000Z
UID:TALK56523@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:In parallel programs\, threads communicate according to the me
 mory consistency model: the set of memory ordering rules enforced by a giv
 en architecture. A great deal of research effort has gone into rigorous fo
 rmalization of memory models. However\, comparatively little attention has
  been paid to the microarchitectural implementation of these models.\nStan
 dard testing-based techniques are insufficient: unobserved behaviors are n
 ot guarantees of non-observability\, and failed tests offer little insight
  into the microarchitectural reason behind failure.\n\nI will present Pipe
 Check\, a methodology and automated tool for verifying that a given microa
 rchitecture correctly implements the memory consistency model specified by
  its architectural specification. PipeCheck adapts the formal notion of a 
 "happens before" graph to the microarchitecture space.\n\nArchitectural sp
 ecifications such as preserved program order are then treated as propositi
 ons to be verified\, rather than simply as assumptions. We also specify an
 d analyze the behavior of common microarchitectural optimizations such as 
 speculative load reordering. Using PipeCheck\, we were able to validate th
 e OpenSPARC T2 in just minutes\, and we found and fixed a bug in a archite
 ctural simulator widely used in academia.\nPipeCheck has been nominated fo
 r the Best Paper award at MICRO 2014\, to be held in Cambridge\, UK this D
 ecember. At the end\, I will also briefly introduce ArMOR\, a framework fo
 r defining dynamic binary translation layers that seamlessly translate bet
 ween memory consistency models such as those used by x86\, ARM\, and Power
 . \n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR