3 Alastair Donaldson Daniel Kroening Philipp Ruemmer. 2010 Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors TACAS Pahos, Cyprus Springer 6015 280-295 Lecture Notes on Computer Science 20/03/2010 <p>Modern multicore processors, such as the Cell Broadband Engine,<br />achieve high performance by equipping accelerator cores with small &ldquo;scratchpad&rdquo; memories. The price for increased performance is programming complexity &ndash; the programmer must manually orchestrate data movement using direct memory&nbsp;access (DMA) operations. Programming using asynchronous DMAs is errorprone, 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.<br />&nbsp;</p> http://www.kroening.com/publications/view-publications-dkr2010.html