BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Mu
 lticore Processors - Alastair Donaldson (University of Oxford)
DTSTART:20100115T140000Z
DTEND:20100115T150000Z
UID:TALK22198@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:Modern multicore processors\, such as the Cell Broadband Engin
 e\,\nachieve high performance by equipping accelerator cores with small\, 
 “scratchpad” memories. The price for increased performance is programm
 ing complexity – the programmer must manually orchestrate data movement 
 using direct memory\naccess (DMA) operations. Programming using asynchrono
 us DMAs is error-prone\,\nand DMA races can lead to nondeterministic bugs 
 which are hard to reproduce\nand fix. We present a method for DMA race ana
 lysis which works by\ninstrumenting a program with assertions modelling th
 e semantics of a memory\nflow controller. To enable automatic verification
  of instrumented programs\, we\npresent a new formulation of k-induction g
 eared towards software\, as a proof rule\noperating on loops. We present a
  tool\, SCRATCH\, which we apply to a large set\nof programs supplied with
  the IBM Cell SDK\, in which we discover a previously\nunknown bug. Our ex
 perimental results indicate that our k-induction method performs\nextremel
 y well on this problem class. To our knowledge\, this marks both\nthe firs
 t application of k-induction to software verification\, and the first exam
 ple\nof software model checking for heterogeneous multicore processors.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR