Journal article icon

Journal article

Automatic analysis of DMA races using model checking and k-induction

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 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...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.1007/s10703-011-0124-2

Authors


Donaldson, AF More by this author
More by this author
Department:
Oxford, MPLS, Computer Science
Rümmer, P More by this author
Publisher:
Springer Publisher's website
Journal:
Formal Methods in System Design Journal website
Volume:
39
Issue:
1
Pages:
83-113
Publication date:
2011-08-01
DOI:
EISSN:
1572-8102
ISSN:
0925-9856
Pubs id:
pubs:327208
URN:
uri:c60eec90-4c52-4dfb-ba2a-56aa753a7c49
UUID:
uuid:c60eec90-4c52-4dfb-ba2a-56aa753a7c49
Local pid:
pubs:327208
Keywords:

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP