Automatic analysis of DMA races using model checking and k-induction
Automatic analysis of DMA races using model checking and k-induction
复制标题
使用模型检查和 k 归纳自动分析 DMA 竞争
DOI：
10.1007/s10703-011-0124-2
复制
发表时间：
2011
影响因子：
0.8
通讯作者：
Donaldson A
中科院分区：
文献类型：
--
作者：
Donaldson A
现代的多核处理器，如Cell Broadband Engine，通过为加速器内核配备小型“暂存”存储器来实现高性能。提高性能的代价是更高的编程复杂性-程序员必须使用直接内存访问（DMA）操作手动编排数据移动。使用异步DMA操作编程容易出错，DMA竞争会导致难以重现和修复的不确定性错误。提出了一种在C程序中进行DMA竞争分析的方法。我们的方法的工作原理是自动仪表的程序与断言建模的语义的内存流控制器。然后可以使用最先进的软件模型检查器来分析插装程序。我们表明，有界模型检查是有效的检测DMA的比赛中有缺陷的程序。为了使自动验证的正确性的仪表程序，我们提出了一个新的配方ofk-感应面向软件，作为一个证明规则操作循环。我们的技术实现为一个工具，Scratch，我们将其应用于IBM Cell SDK提供的大量程序，其中我们发现了一个以前未知的错误。我们的实验结果表明，ourk归纳法在这类问题上表现得非常好。据我们所知，这标志着第一个应用ofk归纳软件验证，和第一个例子的软件模型检查的上下文中的异构多核处理器。
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, andDMA racescan 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 ofk-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 ourk-induction method performs extremely well on this problem class. To our knowledge, this marks both the first application ofk-induction to software verification, and the first example of software model checking in the context of heterogeneous multicore processors.
登录
查看更多内容
异构多核处理器暂存器代码的自动分析
DOI：
--
发表时间：
2010
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
作者：
Alastair F. Donaldson;D. Kroening;P. Rümmer
通讯作者：
P. Rümmer
CellFS：将“DMA”从 Cell 编程中剔除
DOI：
--
发表时间：
2009
期刊：
2009 IEEE International Symposium on Parallel & Distributed Processing
影响因子：
--
作者：
Latchesar Ionkov;Aki Nyrhinen;Andrey Mirtchovski
通讯作者：
Andrey Mirtchovski
基于 SAT 的归纳中的显式安全属性强化
DOI：
--
发表时间：
2007
期刊：
International Conference on VLSI Design
影响因子：
--
作者：
Vishnu C. Vimjam;M. Hsiao
通讯作者：
M. Hsiao
DOI：
10.1145/1941553.1941605
发表时间：
2011
期刊：
--
影响因子：
--
作者：
Botincan M
通讯作者：
Botincan M
关于民间定理
DOI：
--
发表时间：
1980
期刊：
CACM
影响因子：
--
作者：
D. Harel
通讯作者：
D. Harel