BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automatically comparing memory consistency models - John Wickerson
 \, Imperial College
DTSTART:20160624T130000Z
DTEND:20160624T140000Z
UID:TALK66212@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:We identify five tasks involved in designing and reasoning abo
 ut memory consistency models (MCMs): generating conformance tests\, distin
 guishing two MCMs\, searching for monotonicity violations\, debugging comp
 ilation schemes\, and checking the "SC-DRF guarantee". We show that each o
 f these tasks corresponds to solving an instance of a general constraint-s
 atisfaction problem. We further show that although these constraints are n
 ot tractable for automatic solvers when phrased over programs directly\, w
 e can solve analogous constraints over *program executions* and then recon
 struct programs that satisfy the original constraints.\n\nWe illustrate ou
 r technique\, which is implemented in the Alloy modelling framework\, on a
  range of software- and architecture-level MCMs\, both axiomatically and o
 perationally defined. In particular\, we generate: programs that distingui
 sh several recently-published variants of the C11 MCM\, monotonicity viola
 tions in both C11 and x86\, compilation quirks from OpenCL to NVIDIA and A
 MD-style GPUs\, and SC-DRF violations in an early draft of C11. In several
  cases\, our automatically-generated solutions are either new or substanti
 ally simpler than those found manually in previous work.\n\nThis is joint 
 work with Mark Batty (U Kent)\, Tyler Sorensen (Imperial) and George A. Co
 nstantinides (Imperial).
LOCATION:FW26
END:VEVENT
END:VCALENDAR