一种大规模并行程序模型的检测方法

Checking Method of Large-scale Concurrent Program Model

JPF是NASA开发的Java程序模型检测工具。该文通过改写JPF内核中生成状态空间的模块,使待检测程序在受监控状态下模拟执行。用Data-Race算法收集警告信息,引导程序模型检测工具只对死锁相关线程进行模型检测,避免了状态空间爆炸,实现了对大规模并行程序部分线程死锁问题的模型检测。利用启发式搜索算法,在不同的搜索深度赋给待执行线程不同的权值,进一步优化了模拟执行结果。

JPF is a Java program model checker developed by NASA. The module that generates the state space in JPF is rewritten to make the program waiting for model checking run under supervision. The Data-Race algorithm is applied to record warnings which guide JPF to check deadlock related threads. This design avoids the state space explosion and realizes model checking of large-scale programs with only some threads in deadlocks. A heuristic method is also proposed to optimize the efficiency of simulation running by giving different weights to live threads according to search depths.