SHF: Small: CT-DDS -- Scalable Concolic Testing of Parallel Applications With Shared Dynamic Data Structures

尽管并行程序通过利用现代多核机器、机器集群或通用图形处理单元（GPU）支持的并行性来提供性能，但它们也容易出现难以发现的并发性错误。为了产生可靠的并行软件，必须部署强大的自动化测试技术和工具来彻底地测试程序行为，从而暴露并消除并发错误。自动化测试最强大的手段是集合测试，它将程序执行与程序分析（符号执行）结合起来，自动生成不同的程序输入，以执行不同的程序路径。最近的创新使基于编译器的符号执行大大提高了concolic测试的效率。因此，在多核、GPU和集群上测试更复杂的并行程序时，利用聚合测试的时机已经到来。本研究的目标是通过解决两个关键问题，将并行测试推广到异构大规模并行计算平台上的并行程序测试：如何自动测试使用并发动态数据结构的并行程序，其中并行线程保持共享状态；如何提高并行测试的效率，使具有大量线程的并行程序的自动化测试成为可能。构建如此强大的系统将提供高度可靠的并行软件。此外，它将导致在国家需要的领域培养研究生。这个项目的技术目标分为两个重点。第一部分开发了一种方法，用于检验并行程序的行为，从而揭示数据竞争和程序挂起等并发性错误。为了通过concolic测试来练习这些行为，本研究将解决生成非冲突并发数据结构的复杂性，这些数据结构的形状和大小使并行线程能够以一种暴露并发错误（如数据竞争）的方式进行交互。现有技术是不够的，因为它们无法自动探索并发数据结构形状，严重限制了可以执行的并发行为。第二部分提出了一种提高具有大量线程的并行程序的一致性测试效率的方法。为了避免重复的高成本符号执行，需要维护捕获数据结构形状的摘要，然后在聚合测试期间重用它们。因此，不必重复地收集和求解约束，而是可以快速地重新创建所需形状和大小的保存的数据结构。要处理大量线程，采用的方法包括：使线程标识符具有符号化；并将昂贵的符号求值限制在单个线程中。这些摘要还可以识别潜在的并发错误，从而指导探索并发线程所采取的路径，从而确认或否定潜在的错误。在这个项目过程中开发的软件将提供给其他研究人员。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Although parallel programs deliver performance by exploiting parallelism supported by a modern-day multicore machine, a cluster of machines, or a general-purpose graphics processing unit (GPU), they are also prone to concurrency bugs that are hard to uncover. To produce reliable parallel software, powerful automated-testing techniques and tools must be deployed to thoroughly exercise program behaviors to expose and then eliminate concurrency bugs. The most powerful means for automated testing is concolic testing, which combines program execution with program analysis (symbolic execution) to automatically generate different program inputs to exercise different program paths. Recent innovation enabling compiler-based symbolic execution has greatly increased the efficiency of concolic testing. Thus, time has arrived to take advantage of concolic testing in testing even more complex parallel programs for a multicore, a GPU, and a cluster. The goal of this research is to generalize concolic testing to test parallel programs on heterogeneous massively parallel computing platforms by addressing two key challenges: how to automatically test parallel programs that use concurrent dynamic data structures in which parallel threads maintain shared state; and how to scale the efficiency of concolic testing so that automated testing of parallel programs with large number of threads can be made practical. Building such powerful systems will deliver parallel software that is highly reliable. In addition, it will result in training graduate students in an area of national need.The technical aims of this project are divided into two thrusts. The first thrust develops an approach for exercising the behaviors of parallel programs that reveal concurrency bugs such as data races and program hangs. To exercise such behaviors via concolic testing, this research will address the complexity of generating non-conflicting concurrent data structures of those shapes and sizes that enable parallel threads to interact in a manner that exposes concurrency bugs like data races. Existing techniques are inadequate because their inability to automatically explore concurrent data structure shapes severely limits concurrent behaviors that can be exercised. The second thrust develops an approach for improving the efficiency of concolic testing for parallel programs with large numbers of threads. To avoid incurring repeated high cost of symbolic execution, summaries that capture data structure shapes are maintained and then reused during concolic testing. Thus, instead of repeatedly collecting and solving constraints, a saved data structure of desired shape and size can be quickly recreated. To deal with large numbers of threads, approaches employed include: making the thread identifiers symbolic; and limiting expensive symbolic evaluation to a single thread. The summaries also enable identification of potential concurrency bugs that guide exploration of paths taken by concurrent threads to either confirm or disprove potential bugs. The software developed over the course of this project will be made available to other researchers.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.