We present ongoing work on applying model checking techniques to
automatically analyse multicore software where data is managed
explicitly by the programmer via direct memory access (DMA)
operations. We describe SCRATCH, a DMA race analysis tool for the Cell
BE processor which employs bounded model checking and k-induction. We
then outline our plans to extend this work.