Abstract

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.