Paper Info
Title
Strengthening induction-based race checking with lightweight static analysis
Abstract
Direct Memory Access (DMA) is key to achieving high performance in system-level software for multicore processors such as the Cell Broadband Engine. Incorrectly orchestrated DMAs cause DMA races, leading to subtle bugs that are hard to reproduce and fix. In previous work, we have shown that k- induction yields an effective method for proving absence of a restricted class of DMA races. We extend this work to handle a larger class of DMA races. We show that the applicability of k-induction can be significantly improved when combined with three inexpensive static analyses: 1) abstract-interpretation-based static analysis; 2) chunking, a domain-specific invariant generation technique; and 3) code transformations based on statement independence. Our techniques are implemented in the SCRATCH tool. We evaluate our work on industrial benchmarks.
Year
DOI
Venue
2011
10.1007/978-3-642-18275-4_13
VMCAI
Keywords
Field
DocType
induction-based race checking,cell broadband engine,inexpensive static analysis,lightweight static analysis,abstract-interpretation-based static analysis,larger class,scratch tool,direct memory access,dma race,previous work,restricted class,domain-specific invariant generation technique,static analysis,multicore processors
Scratch,Computer science,Abstract interpretation,Static analysis,Parallel computing,Software,Direct memory access,Chunking (psychology),Invariant (mathematics),Multi-core processor
Conference
Volume
ISSN
Citations 
6538
0302-9743
6
PageRank 
References 
Authors
0.47
13
3
Name
Order
Citations
PageRank
Alastair F. Donaldson166152.35
Leopold Haller21276.93
Daniel Kroening33084187.60