一种基于Petri网验证的数据竞争检测方法

• 作者: 丁世举 杜云开 邵祎康 顾乃杰
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 数据竞争 误报 漏报 Petri网 Lockset
• 年，卷（期）: 2017,（10）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 2352-2357
• 页数: 6页
• 分类号: TP311
• 字数: 7162字
• 语种: 中文

摘要

数据竞争是并行程序中常见的一类问题,由于并行程序的时序不确定性而导致数据竞争难以检测.传统的基于Locks-et的检测算法速度快,但检测结果中包含较多误报,影响了算法的实用性.为了降低Lockset算法的误报率,本文提出一种将Lockset算法与模型检查相结合的方法,充分利用模型检查的高准确性的特点,逐个验证Lockset算法报出的潜在数据竞争.在模型选择上,本文选择使用Petri网,并且提出了Petri网验证数据竞争的算法.此外,还介绍了我们基于此方法实现的检测工具PeserX,通过对SPLASH2测试集进行测试,我们发现提出的方法能够有效地降低数据竞争检测的误报率,使得数据竞争检测进一步走向实用.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	顾乃杰	中国科学技术大学计算机科学与技术学院	83	347	9.0	12.0
5	杜云开	中国科学技术大学计算机科学与技术学院	4	2	1.0	1.0
7	丁世举	中国科学技术大学计算机科学与技术学院	3	1	1.0	1.0
13	邵祎康	中国科学技术大学计算机科学与技术学院	1	0	0.0	0.0