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

摘要：

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

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

所属期刊栏目：34

分类号：TP391(计算技术、计算机技术)

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

在线出版日期：2008-09-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：72-74