BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proving safety of asynchronous multi-core programs - Matko Botinca
 n
DTSTART:20100726T114500Z
DTEND:20100726T130000Z
UID:TALK25435@talks.cam.ac.uk
DESCRIPTION:Asynchronous memory operations provide a means for avoiding th
 e memory wall in multicore processors. When multiple cores concurrently ac
 cess shared memory in a synchronous manner\, the gap between processor and
  memory performance leads to a bottleneck: scalable performance improvemen
 ts due to increased parallelism are lost due to contention for memory. Asy
 nchronous memory operations offer a solution. Cores delegate data-movement
  to dedicated hardware\, and continue processing in parallel with data-mov
 ement\, thus overlapping computation with communication. With the advent o
 f multicore and GPU computing\, asynchronous memory operations are availab
 le in many programming platforms and libraries\, e.g.\, DMA operations in 
 the IBM Cell Broadband Engine\, I/O Acceleration Technology in Intel Xeon 
 processors\, and asynchronous memory copying in the OpenCL and CUDA langua
 ges. \n\nHowever\, asynchronous memory operations lead to potential memory
  races\, increasing programming complexity. Reasoning about correct usage 
 of such operations involves complex flow-\, path- and context-sensitive an
 alysis of memory accesses dealing with possibly overlapping regions of mem
 ory. We develop a methodology for a C-like language based on separation lo
 gic that enables automatic reasoning about memory safety of multicore prog
 rams utilizing asynchronous memory operations. We present a set of proof r
 ules\, and show that if the rules can be used to show that a program satis
 fies a given specification then the program is memory-safe\, and\, in part
 icular\, free of memory races. We discuss some of the implementation issue
 s and demonstrate how the approach can be applied for checking absence of 
 DMA races in the Cell Broadband Engine.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR