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

Race Detection Based on Petri-net Verification

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

Data race detection is limited to the uncertainty of concurrency. The most famous detection method is Lockset-based algorithm. However, theLockset algorithm produces a lot of false alarms, preventing it from being utilized in practical. In order to reduce the false positive radio, a new method is proposed in this paper,combining the Lockset algorithm with model checking. Model checking is precise, so it is suitable to verify potential data races produced by Lockset algorithm. Petri nets are chosen as the models. A Petri nets based verification algorithm is presented in this paper. Furthermore, we implemented the algorithm into a tool, named PeserX. To validate the efficiency of our method,PeserX is applied to SPLASH2 benchmarks. The experimental results show that our method reduces the false alarm radio significantly.