Heuristics for efficient dynamic verification of message passing interface and thread programs

Update Item Information
Publication Type thesis
School or College College of Engineering
Department Computing
Author Chiang, Wei-Fan
Title Heuristics for efficient dynamic verification of message passing interface and thread programs
Date 2011-05
Description Concurrent programs are extremely important for efficiently programming future HPC systems. Large scientific programs may employ multiple processes or threads to run on HPC systems for days. Reliability is an essential requirement of existing concurrent programs. Therefore, verification of concurrent programs becomes increasingly important. Today we have two significant challenges in developing concurrent program verification tools: The first is scalability. Since new types of concurrent programs keep being created, verification tools need to scale to handle all these new types of programs. The second is providing formal coverage guarantee. Dynamic verification tools always face a huge schedule space. Both these capabilities must exist for testing programs that follow multiple concurrency models. Most current dynamic verification tools can only explore either thread level or process level schedules. Consequently, they fail to verify hybrid programs. Exploring mixed process and thread level schedules is not an ideal solution because the state space will grow exponentially in both levels. It is hard to systematically traverse these mixed schedules. Therefore, our approach is to determinize all concurrent APIs except one API whose schedules will then be explored. To improve search efficiency, we proposed a random-walk based heuristic algorithm. We observed many concurrent programs and concluded some common structures of them. Based on the existence of these structures, we can make dynamic verification tools focusing on specific regions and bypassing regions of less interest. We propose a random sampling of executions in the regions of less interest.
Type Text
Publisher University of Utah
Subject Dynamic verification; Heuristic; MPI programs; Thread programs
Dissertation Institution University of Utah
Dissertation Name Master of Science
Language eng
Rights Management Copyright © Wei-Fan Chiang 2011
Format Medium application/pdf
Format Extent 502,661 bytes
Identifier us-etd3,35714
Source Original housed in Marriott Library Special Collections, QA3.5 2011 .C45
ARK ark:/87278/s6057wn5
Setname ir_etd
ID 194600
Reference URL https://collections.lib.utah.edu/ark:/87278/s6057wn5