基于符号执行的MPI程序分析与验证技术研究

发布时间：2018-01-02 08:41

本文关键词：基于符号执行的MPI程序分析与验证技术研究　出处：《国防科学技术大学》2016年博士论文　论文类型：学位论文

【摘要】：软件可信性提高是计算机科学中的重要研究问题。MPI是高性能计算领域开发并发程序的主流框架,大部分运行在超级计算机上的并发程序是采用MPI开发的,有些开发代价超过几十人年。考虑到使用MPI开发的高性能应用的规模以及高性能计算中心的高昂构建、维护费用,MPI程序的可信性保障问题日渐引起人们的重视,而MPI程序的分析和验证技术作为可信性提高的手段,成为大规模并行程序开发的关键技术。由于MPI程序缺陷可能输入相关,即只有在某些特定输入的时候才表现出来,不提供输入覆盖的技术如测试、正确性检查、动态验证等,难以捕获到这些输入相关缺陷。符号执行是上世纪70年代提出的一种基于约束求解的程序分析技术,可以自动化地探索程序路径空间。符号执行可用于程序的缺陷查找、自动测试和自动验证。本文基本思路就是使用符号执行来分析MPI程序。然而,作为一种通用的基本程序分析方法,符号执行在应用于MPI程序分析上时,面临挑战:面对MPI程序本身的不确定性以及复杂性,在输入覆盖之外,符号执行本身无法提供MPI程序的非确定性覆盖;由于符号执行本身的特性,在分析规模较大的MPI程序时,其可扩展性面临一定的挑战。本文围绕这两方面的挑战展开了研究,旨在进一步提高MPI程序的可信性。本文的主要研究内容包括:1.同步MPI程序的符号执行方法。现存的绝大部分MPI程序缺陷检测方法不能同时提供输入和不确定性的双重覆盖,因此可能存在漏报问题。而在MPI程序中,人们为了获取高性能,允许所谓的“通配接收”,即标记和接收源允许使用通配符,运行时才决定此接收操作是和具体的哪个发送操作相匹配,这就带来了一定的非确定性。针对带有通配接收的阻塞MPI程序,本文采用符号执行来保证输入空间的覆盖,使用懒惰匹配的方法保证通配接收带来的非确定性覆盖,并提出了一种即时调度方法来减少盲目的交叠遍历;另外,我们证明了依据此调度方法,不会漏掉通配接收的匹配而导致漏报死锁。在基准测试集上的实验表明,该方法可以有效地找到程序中的死锁、运行时错误等。2.异步MPI程序的符号执行方法。人们为了开发高效的MPI程序,尽可能使得MPI任务的计算时间和底层MPI库的通信时间重叠,常常通过调用非阻塞接口的方法来实现。然而,本文之前针对阻塞MPI程序提出的方法在面对非阻塞MPI调用的时候,无法直接适用。为了继续保持不确定性和输入空间的双重覆盖,本文扩展了懒惰匹配方法,其主要思想是尽可能地推迟非确定性源接收的匹配时机。另一方面,符号执行的路径空间爆炸问题在分析MPI程序的时候更加突出:在没有采用路径削减技术的情况下,路径数目与程序的进程数、通配接收对应的匹配数、程序的分支数目都呈指数关系。本文提出了一种面向死锁的符号执行引导技术,根据已有路径信息,把引导问题转换成为一个死锁的模型检验问题,根据结果来引导符号执行更快找到死锁。3.MPI缓冲区错误检测。非阻塞MPI调用能够通过重叠部分计算和通信过程,从而能够有效降低通信开销,但是可能带来应用程序和底层MPI库的缓冲区错误。本文基于所提出的MPI程序符号执行方法提出了一种查找输入相关的缓冲区错误的方法,使用一个性质来规约非阻塞通信绑定的缓冲区上发生的事件应该满足的时序,然后在符号执行过程中对每条路径进行检查。同时针对检查方法中需要对大量内存访问指令的解释执行增加检查的问题,提出了两种优化方法,以减少在内存访问指令处的检查数目。此外,本文基于同步以及异步MPI程序的符号执行方法,实现了MPI符号执行平台MPISE。MPISE针对MPI程序的源代码进行分析,能够检测MPI程序的死锁、缓冲区错误与运行时错误,其主要优点有:为MPI程序分析提供输入和通配接收带来的非确定性接收双重覆盖、支持异步调用、不需要修改用户源代码等。在验证的程序规模方面,本文已使用MPISE分析最大多达80 k LOC的MPI程序。
[Abstract]:To improve the software trustworthiness is.MPI important research problems in Computer Science in the field of high performance computing framework is the mainstream development of concurrent programs, most run on a supercomputer concurrent program is developed using MPI, some development costs more than dozens of years. Considering the high performance applications developed using the MPI scale and high performance computing center high building, maintenance costs, dependability problem MPI program has attracted people's attention, and the MPI program analysis and verification techniques to improve credibility as a means to become the key technology of large-scale parallel program development. Because the MPI bugs may enter, i.e. only when certain inputs do not appear, do not provide input covering techniques such as testing, examination, dynamic verification, to capture these input related defects. Symbolic execution is the world Ji 70s proposed an analysis technique of constraint solving based on the procedures, can automatically explore the program path space. Can be used to find the defects of symbolic execution procedures, automatic test and automatic verification. The basic idea of this paper is to use symbolic execution to analyze MPI program. However, as a basic procedure of general analysis method, symbolic execution face the challenge in using MPI analysis program, the MPI program itself: in the face of uncertainty and complexity in the input coverage, symbolic execution itself cannot provide non deterministic MPI program by covering; to enforce its own characteristics in the analysis of symbols, the larger MPI program, its scalability facing certain challenges. This paper focuses on the two challenges of research, to further improve the credibility of the MPI program. The main contents of this paper include: 1. the symbol synchronization of MPI Method of execution. Most of the existing MPI program defect detection method can not provide input and double coverage uncertainty at the same time, so there may be missing. While in the MPI program, in order to obtain high performance, allowing the so-called "wildcard receiving", which are markers and receiving the source allows the use of wildcards, decide when this operation the receive operation and which is sending the specific operation, which brings uncertainty to some extent. Aiming at receiving wildcard blocking MPI program, this paper uses symbolic execution to ensure the input space coverage, using the method of lazy, that covers the non deterministic wildcard receive brought, and put forward a kind of instant scheduling method to reduce overlapping traversal blindness; in addition, we prove that the scheduling method based on this, will not miss the wildcard matching and receiving lead to underreporting deadlock. In the benchmark set. Experiment shows that this method can effectively find the deadlock in the program, such as asynchronous MPI program error.2. symbolic execution method runs. In order to develop efficient MPI program, as much as possible so that the communication time MPI task computing time and the underlying MPI library overlap, often by adjusting method using non blocking interface to achieve. However, this method for blocking before MPI procedure is proposed in the face of non blocking MPI call, can not be directly applicable. In order to continue to maintain double coverage uncertainty and input space, this paper extends the lazy matching method, the main idea is as far as possible, the time delay uncertainty source received. On the other hand, path the space explosion problem of symbolic execution is more prominent in the analysis of the MPI program: in the absence of the path cut technology, path number and course number, distribution of receiving The matching number should be the number of branches of the program have an exponential relationship. This paper presents a deadlock oriented symbolic execution guide technology, according to the existing path information, to guide the problem into a model checking problem of deadlock, according to the results to guide the symbolic execution faster to find errors in.3.MPI buffer deadlock detection. Non blocking MPI call through overlap of computation and communication process, which can effectively reduce the communication overhead, but may bring the buffer application and the underlying MPI library error. This paper proposed the implementation of the program symbol MPI proposed a method to find the input buffer related errors based on the sequential use of a property specification non blocking communication binding buffer events should be satisfied, then for each path in check during symbolic execution. At the same time for the inspection method for To access a lot of memory instructions to explain the implementation of increased inspection problems, put forward two kinds of optimization methods, to reduce the number of check in memory access instructions. In addition, the implementation method of synchronous and asynchronous MPI program based on the realization of the MPI symbol, symbolic execution platform MPISE.MPISE for MPI source code analysis can deadlock detection of the MPI program, running buffer error and error, its main advantages are: to provide non deterministic input and wildcard receive brought to receive double coverage for MPI program analysis, support for asynchronous calls, the user does not need to modify the source code. In the verification of the program size, this paper has analyzed the maximum up to 80 K LOC MPI program using MPISE.

【学位授予单位】：国防科学技术大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：TP311.1

【相似文献】