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

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

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.