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

SHF：小型：CT-DDS——具有共享动态数据结构的并行应用程序的可扩展 Concolic 测试

• 批准号: 2226448
• 负责人: Rajiv Gupta
• 金额: $ 60万
• 依托单位: University of California-Riverside
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2226448&HistoricalAwards=false
• 关键词: SHF; Small; CT; DDS; Scalable

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.

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