基于约束求解的并发程序错误预测方法研究

摘要

为保证正确性，并发程序的执行过程中必须保证存在一致性关系的共享变量得到原子性执行。若对存在一致性关系的共享变量的访问语句与其他线程中的语句产生预期之外的交织，且执行结果与任意这些语句的原子执行结果均不相同，则产生了原子集合序列化违背。原子集合序列化违背是一种常见的并发缺陷，可导致共享变量读写值不一致、读写值丢失等严重后果。现有的原子集合序列化违背探测技术大多采用较为保守的并发程序模型，仍存在漏报率和误报率较高的问题。 为提高原子集合序列化违背的探测能力，本文提出一种基于约束求解的原子集合序列化违背探测方法。该方法在程序执行过程中动态收集程序的执行轨迹，然后根据最大因果模型和收集的执行轨迹推导出其他的可执行交织，并在这些可执行交织中探测在原执行轨迹中未暴露的原子集合序列化违背，将并发执行的可行性要求转化为一组约束条件，从而将原子集合序列化违背的探测问题转化为约束求解问题。该方法考虑了程序控制流信息，扩大可搜索的交织空间，提高了工具的探测能力，降低了漏报率；且该方法是基于约束求解的探测方法，因此求解出的原子集合序列化违背一定是真实的，不产生误报。 在上述工作的基础上，本文设计并实现了基于约束求解的原子集合序列化违背探测工具ASVDetector，并与并发错误探测工具PECAN进行比较。实验结果表明：ASVDetector可有效探测原子集合序列化违背，在13个被测程序中，ASVDetector探测出的原子集合序列化违背个数是PECAN的约2倍，显著降低了漏报率，且不存在误报；对分支事件可行性松弛可进一步提高其探测能力，降低漏报率。

目录

第一个书签之前