DSGEN: concolic testing GPU implementations of concurrent dynamic data structures
DSGEN: concolic testing GPU implementations of concurrent dynamic data structures
复制标题
DSGEN：并发动态数据结构的 concolic 测试 GPU 实现
DOI：
10.1145/3447818.3460962
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Gupta, Rajiv
中科院分区：
文献类型：
--
作者：
Sun, Xiaofan;Gupta, Rajiv
Concolic测试将具体执行与符号执行沿着执行路径相结合，以自动生成新的测试输入，这些输入可以执行程序路径，并在测试期间提供高代码覆盖率。GKLEE工具使用这种方法来暴露为执行GPGPU而编写的CUDA程序中的数据竞争。在采用并发动态数据结构的程序中，自动生成具有适当形状的数据结构是一个挑战，该数据结构使线程遵循所选择的、可能发散的路径。此外，必须为多个线程生成单个非冲突数据结构，也就是说，必须找到同时使所有线程遵循其各自选择的路径的单个形状。当执行暴露了错误（例如，数据竞争），生成的数据结构形状帮助程序员理解错误的原因。由于GKLEE不允许将构造动态数据结构的指针符号化，因此它不能自动生成不同形状的数据结构，并且必须依赖于用户编写构造它们的代码来执行所需的路径。我们已经开发了DSGEN自动生成非冲突的动态数据结构与不同的形状，并将其与GKLEE发现和促进了解的数据竞争程序，采用复杂的并发动态数据结构。与GKLEE相比，DSGEN通过在四种复杂的并发动态数据结构（B树，哈希数组映射Trie，RRB树和跳过列表）的实现中自动生成总共1，897个形状，将检测到的竞争数量从10增加到25。
Concolic testing combines concrete execution with symbolic execution along the executed path to automatically generate new test inputs that exercise program paths and deliver high code coverage during testing. The GKLEE tool uses this approach to expose data races in CUDA programs written for execution of GPGPUs. In programs employing concurrent dynamic data structures, automatic generation of data structures with appropriate shapes that cause threads to follow selected, possibly divergent, paths is a challenge. Moreover, a single non-conflicting data structure must be generated for multiple threads, that is, a single shape must be found that simultaneously causes all threads to follow their respective chosen paths. When an execution exposes a bug (e.g., a data race), the generated data structure shape helps the programmer understand the cause of the bug. Because GKLEE does not permit pointers that construct dynamic data structures to be made symbolic, it cannot automatically generate data structures of different shapes and must rely on the user to write code that constructs them to exercise desired paths. We have developed DSGEN for automatically generating non-conflicting dynamic data structures with different shapes and integrated it with GKLEE to uncover and facilitate understanding of data races in programs that employ complex concurrent dynamic data structures. In comparison to GKLEE, DSGEN increases the number of races detected from 10 to 25 by automatically generating a total of 1,897 shapes in implementations of four complex concurrent dynamic data structures -- B-Tree, Hash-Array Mapped Trie, RRB-Tree, and Skip List.
登录
查看更多内容
Java 字节码基于约束的测试输入生成
DOI：
10.1109/issre.2010.26
发表时间：
2010
期刊：
2010 IEEE 21st International Symposium on Software Reliability Engineering
影响因子：
--
作者：
Florence Charreteur;A. Gotlieb
通讯作者：
A. Gotlieb
基于 SMT 的可扩展 GPU 内核功能验证
影响因子：
12.6
作者：
Guodong Li;G. Gopalakrishnan
通讯作者：
G. Gopalakrishnan
数据结构故障自动定位
DOI：
--
发表时间：
2016
期刊：
International Conference on Compiler Construction
影响因子：
--
作者：
Vineet Singh;Rajiv Gupta;Iulian Neamtiu
通讯作者：
Iulian Neamtiu
RRB-Trees：高效的不可变向量
DOI：
--
发表时间：
2011
期刊：
影响因子：
--
作者：
P. Bagwell;Tiark Rompf
通讯作者：
Tiark Rompf
参数流：CUDA 程序中种族符号分析的自动行为等效
DOI：
--
发表时间：
2012
期刊：
International Conference for High Performance Computing, Networking, Storage and Analysis
影响因子：
--
作者：
Peng Li;Guodong Li;G. Gopalakrishnan
通讯作者：
G. Gopalakrishnan