面向死锁检查的非阻塞MPI程序符号执行方法、系统及介质

摘要

本发明涉及计算机高性能计算的可靠性保证领域，公开了一种面向死锁检查的非阻塞MPI程序符号执行方法、系统及介质。针对非阻塞MPI程序的异步性和非确定性，本发明通过为通信操作的不同消息匹配情况和不同交叠执行情况创建不同待探索状态来确保符号执行能够系统遍历MPI程序的路径空间。发明框架中的语句符号执行方法能精确刻画不同类型语句执行所对应的符号化状态迁移，阻塞驱动匹配策略能够有效获取符号执行过程中通信行为的所有可能匹配情况。本发明基于符号执行来系统遍历非阻塞MPI程序的路径空间，在探索程序执行路径时自动检测路径是否发生死锁，直到探索完程序路径空间、发现死锁或者超时。