1.一种面向死锁检查的非阻塞MPI程序符号执行方法，其特征在于实施步骤包括：1）输入MPI程序、运行进程个数N和符号化变量集合Sym；2）初始化待探索状态集合Worklist为全局初始化状态init，所述全局初始化状态init为所有进程初始状态的组合；3）按照状态空间搜索策略从待探索状态集合Worklist中选出一个尚未处理的全局状态作为当前全局状态S c ；4）按照轮询调度策略，选取待探索状态S c 下的活跃进程i来执行，其中进程i的符号化状态包括该进程的变量映射关系M i 、待执行语句Stat i 、路径约束条件PC i 和进程运行状态F；5）基于全局状态S c 对进程i的待执行语句Stat i 进行语句符号执行，根据语句符号执行方法更新进程i的符号执行状态，并判断是否进入全局阻塞状态，即S c 中所有进程运行状态是否都阻塞或者终止，如果是则跳转至步骤6），否则继续执行步骤4）；6）在全局阻塞状态下进行通信行为的匹配，为通信操作的不同消息匹配情况和不同交叠执行情况创建待探索状态，并加入到Worklist中；根据通信操作的匹配情况更新进程的运行状态及进行死锁检查；7）判断是否发生死锁、超时或者待探索状态集合Worklist为空，如果是则终止分析，否则，跳转执行步骤3）；步骤6）中在全局阻塞状态S c 下进行消息匹配和死锁检查，其详细步骤包括：6.1）初始化用于记录任意源接收操作匹配情况的集合PS W 为空；6.2）匹配获取全局阻塞状态S c 下一对非任意源操作的匹配pair n ；6.3）如果匹配pair n 为非空，执行消息匹配pair n 并创建新状态S c ’，其中新状态S c ’对应于基于S c 执行消息匹配pair n 所带来的状态变化，更新S c ’中匹配对pair n 所包含阻塞通信动作所在进程的运行状态为活跃，将新状态S c ’加入到Worklist中并返回；否则，执行步骤6.4）；6.4）针对全局状态S c 匹配任意源接收操作，将匹配结果加入集合PS W ；如果集合PS W 非空，则基于全局状态S c 为集合PS W 中的每一种任意源操作的匹配pair w 创建一个相应的新状态S c ’，其中S c ’表示状态S c 执行消息匹配pair w 所迁移到的状态，添加新状态S c ’到待探索状态集合Worklist中并返回；否则，执行步骤6.5）；6.5）在该全局阻塞状态下检查是否仍有未终止的进程，若有则报告产生死锁，否则返回。
2.根据权利要求1所述的面向死锁检查的非阻塞MPI程序符号执行方法，其特征在于，步骤5）中符号执行活跃进程i的待执行语句Stat i 的详细步骤包括：5.1）判断待执行语句Stat i 的类型，如果Stat i 为非阻塞通信操作则执行步骤5.2）；如果Stat i 为阻塞通信操作则跳转执行步骤5.3）；否则跳转执行步骤5.4）；5.2）通过序列Seq i 来记录进程i流出的通信操作序列，记录方法为将新流出的通信操作拼接在之前流出的操作序列尾部，且保持进程i的运行状态仍为活跃；5.3）通过序列Seq i 来记录进程i流出的通信操作序列，记录方法为将新流出的通信操作拼接在之前流出的操作序列尾部；更新进程i的运行状态为阻塞；5.4）按照传统符号执行方法执行语句，且保持进程i的运行状态仍为活跃。
3.根据权利要求1所述的面向死锁检查的非阻塞MPI程序符号执行方法，其特征在于，步骤6.2）匹配获取全局阻塞状态S c 下一对非任意源操作的匹配pair n ，详细步骤包括：判断每个进程i的通信序列Seq i 中是否存在未匹配的栅栏同步操作Barrier，如果成立则返回该栅栏同步操作Barrier作为匹配；否则按照进程编号i的升序扫描通信序列Seq i ，首先判断通信序列Seq i 中是否存在等待操作Wait(r)且句柄r所对应的非阻塞通信操作已经完成，如果成立则返回该阻塞等待操作Wait(r)作为匹配，否则继续判断通信序列Seq i 中是否存在能够匹配的消息发送操作send(j)且通信序列Seq j 中存在能够匹配的消息接收操作recv(i)，如果成立则返回消息发送操作send(j)和消息接收操作recv(i)作为匹配；否则，返回空的匹配。
4.根据权利要求1所述的面向死锁检查的非阻塞MPI程序符号执行方法，其特征在于，步骤6.4）中匹配获取全局阻塞状态S c 下任意源接收操作的匹配集合，对于一个给定任意源接收操作，会扫描所有其他进程流出的通信序列来获取MPI语义下能够与之匹配的发送操作，当全局阻塞状态S c 下存在多个任意源接收操作可以被匹配时，符号执行会为它们之间的每一种匹配顺序创建一个待探索状态。
5.一种面向死锁检查的非阻塞MPI程序符号执行系统，包括计算机设备，其特征在于，该计算机设备被编程或配置以执行权利要求1-4中任意一项所述面向死锁检查的非阻塞MPI程序符号执行方法的步骤。
6.一种面向死锁检查的非阻塞MPI程序符号执行系统，包括计算机设备，其特征在于，该计算机设备的存储介质上存储有被编程或配置以执行权利要求1-4中任意一项所述面向死锁检查的非阻塞MPI程序符号执行方法的计算机程序。
7.一种计算机可读存储介质，其特征在于，该计算机可读存储介质上存储有被编程或配置以执行权利要求1-4中任意一项所述面向死锁检查的非阻塞MPI程序符号执行方法的计算机程序。
8.一种面向死锁检查的非阻塞MPI程序符号执行系统，其特征在于包括：输入程序单元，用于输入MPI程序、运行进程个数N和符号化变量集合Sym；状态初始化程序单元，用于初始化待探索状态集合Worklist为全局初始化状态init，所述全局初始化状态init为所有进程初始状态的组合；遍历状态选择程序单元，用于按照给定搜索策略从待探索状态集合Worklist中选择一个尚未处理的全局状态S c 来探索；进程调度程序单元，用于按照轮询调度策略，选取待探索状态S c 下的活跃进程i，其状态包括变量映射关系M i 、下一条执行语句Stat i 、进程路径条件PC i 和进程运行状态F i ；语句符号执行程序单元，用于在全局状态S c 下对进程i的待执行语句Stat i 进行符号执行，并更新进程的符号化状态；消息匹配和死锁检查程序单元，用于在全局阻塞状态下对通信行为进行匹配、更新待探索状态集合Worklist和检查探索路径是否发生死锁；语句符号执行程序单元在全局阻塞状态S c 下进行消息匹配和死锁检查的详细步骤包括：6.1）初始化用于记录任意源接收操作匹配情况的集合PS W 为空；6.2）匹配获取全局阻塞状态S c 下一对非任意源操作的匹配pair n ；6.3）如果匹配pair n 为非空，执行消息匹配pair n 并创建新状态S c ’，其中新状态S c ’对应于基于S c 执行消息匹配pair n 所带来的状态变化，更新S c ’中匹配对pair n 所包含阻塞通信动作所在进程的运行状态为活跃，将新状态S c ’加入到Worklist中并返回；否则，执行步骤6.4）；6.4）针对全局状态S c 匹配任意源接收操作，将匹配结果加入集合PS W ；如果集合PS W 非空，则基于全局状态S c 为集合PS W 中的每一种任意源操作的匹配pair w 创建一个相应的新状态S c ’，其中S c ’表示状态S c 执行消息匹配pair w 所迁移到的状态，添加新状态S c ’到待探索状态集合Worklist中并返回；否则，执行步骤6.5）；6.5）在该全局阻塞状态下检查是否仍有未终止的进程，若有则报告产生死锁，否则返回。
