Programming and execution models for parallel bounded exhaustive testing
Programming and execution models for parallel bounded exhaustive testing
复制标题
DOI：
10.1145/3485543
复制
发表时间：
2021-10
影响因子：
--
通讯作者：
Nader Al Awar;Kush Jain;C. Rossbach;Miloš Gligorić
中科院分区：
文献类型：
--
作者：
Nader Al Awar;Kush Jain;C. Rossbach;Miloš Gligorić
有界穷举测试 (BET) 是一种检测软件错误的有效方法，它对所有输入执行受测程序的某些限制。基于属性的系统测试是一种 BET 方法，开发人员可以编写描述测试输入属性的测试生成程序。混合测试生成程序通过自由组合声明性过滤器和命令式生成器，提供了最具表现力的方式来编写所需的属性。然而，探索混合测试生成程序以获得测试输入既需要计算量，又难以并行化。我们提出了第一个编程和执行模型，称为 Tempo，用于混合测试生成程序的并行探索。我们描述了将计算映射到并行硬件的两种不同策略，并针对 GPU 和 CPU 实现了它们。我们通过生成 BET 领域基准测试常用的各种数据结构的实例来评估 Tempo。此外，我们还生成了 CUDA 程序来对 CUDA 编译器进行压力测试，发现了开发人员确认的四个错误。
Bounded-exhaustive testing (BET), which exercises a program under test for all inputs up to some bounds, is an effective method for detecting software bugs. Systematic property-based testing is a BET approach where developers write test generation programs that describe properties of test inputs. Hybrid test generation programs offer the most expressive way to write desired properties by freely combining declarative filters and imperative generators. However, exploring hybrid test generation programs, to obtain test inputs, is both computationally demanding and challenging to parallelize. We present the first programming and execution models, dubbed Tempo, for parallel exploration of hybrid test generation programs. We describe two different strategies for mapping the computation to parallel hardware and implement them both for GPUs and CPUs. We evaluated Tempo by generating instances of various data structures commonly used for benchmarking in the BET domain. Additionally, we generated CUDA programs to stress test CUDA compilers, finding four bugs confirmed by the developers.