2010 | OriginalPaper | Buchkapitel
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors
verfasst von : Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 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.