uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Automatic analysis of DMA races using model checking and k-induction
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2011 (English)In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 39, no 1, 83-113 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
2011. Vol. 39, no 1, 83-113 p.
Keyword [en]
Model checking, k-induction, DMA, Multicore programming, Cell BE
National Category
Computer Science
URN: urn:nbn:se:uu:diva-156592DOI: 10.1007/s10703-011-0124-2ISI: 000292565100003OAI: oai:DiVA.org:uu-156592DiVA: diva2:432827
Available from: 2011-08-07 Created: 2011-08-04 Last updated: 2011-08-07Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text
By organisation
Computer Systems
In the same journal
Formal methods in system design
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 152 hits
ReferencesLink to record
Permanent link

Direct link