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

点击翻译按钮获取中文摘要

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.