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

Checking Method of Large-scale Concurrent Program Model

作　　者：杨明远[1] 罗贵明[1] 

机构地区：[1]清华大学软件学院,北京100084

出　　处：《计算机工程》2008年第13期72-74,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60474026;60672110);清华大学研究基金资助项目;清华信息学院基金资助项目

摘　　要：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.

关 键 词：JPF工具 并行程序 运行信息 Data-Race算法 启发式搜索 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]