Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors

Add to your list(s) Download to your calendar using vCal

• Alastair Donaldson (University of Oxford)
• Friday 15 January 2010, 14:00-15:00
• Room FW11, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Matthew Parkinson.

Modern multicore processors, such as the Cell Broadband Engine, achieve high performance by equipping accelerator cores with small, “scratchpad” memories. The price for increased performance is programming complexity – the programmer must manually orchestrate data movement using direct memory access (DMA) operations. Programming using asynchronous DMAs is error-prone, and DMA races can lead to nondeterministic bugs which are hard to reproduce and fix. We present a method for DMA race analysis which works by instrumenting a program with assertions modelling the semantics of a memory flow controller. To enable automatic verification of instrumented programs, we present a new formulation of k-induction geared towards software, as a proof rule operating on loops. We present a tool, SCRATCH , which we apply to a large set of programs supplied with the IBM Cell SDK , in which we discover a previously unknown bug. Our experimental results indicate that our k-induction method performs extremely well on this problem class. To our knowledge, this marks both the first application of k-induction to software verification, and the first example of software model checking for heterogeneous multicore processors.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.