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

• 作者: 杨明远 罗贵明
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: JPF工具 并行程序 运行信息 Data-Race算法 启发式搜索
• 年，卷（期）: 2008,（13）
• 所属期刊栏目: 软件技术与数据库
• 页码范围: 72-74
• 页数: 3页
• 分类号: TP391
• 字数: 3657字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2008.13.027

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗贵明	清华大学软件学院	19	125	6.0	10.0
2	杨明远	清华大学软件学院	1	6	1.0	1.0