Modern multicore processors, such as the Cell Broadband Engine, achieve high
performance by equipping accelerator cores with small ``scratch-pad''
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 automatically instruments the 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.