Automatic analysis of scratch-pad memory code for heterogeneous multicore processors

Abstract. 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 mem-ory access (DMA) operations. Programming using asynchronous DMAs is error-prone, and DMA races can lead to nondeterministic bugs which are hard to repro-duce 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 per-forms 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.