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
  higher programming complexity -- the programmer must manually
  orchestrate data movement using direct memory access (DMA)
  operations.  Programming using asynchronous DMA operations 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 in C programs.  Our method works by automatically
  instrumenting a program with assertions modeling the semantics of a
  memory flow controller.  The instrumented program can then be
  analyzed using state-of-the-art software model checkers.  We show
  that bounded model checking is effective for detecting DMA races in
  buggy programs.  To enable automatic verification of the correctness
  of instrumented programs, we present a new formulation of
  k-induction geared towards software, as a proof rule operating on
  loops.  Our techniques are implemented as 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 in the context of
  heterogeneous multicore processors.