软件可信性提高是计算机科学中的重要研究问题。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程序。