一种基于约束求解的原子违背探测方法

摘要

本发明提供一种基于约束求解的原子违背探测方法，利用并发程序的原始执行轨迹确定原子性区域，结合原子违背的各种错误模式，建立原始执行轨迹中事件之间执行先后顺序的约束关系，利用Z3求解器进行约束求解，将原子违背的探测问题转化为约束等式的求解问题。本方法属于运行时预测技术，可根据约束求解出隐藏在原始执行轨迹中没有暴露出的原子违背错误，具有更好的探测原子违背的能力；对原始程序轨迹和每个不可序列化的执行交织建立一组约束，将探测原子违背问题转化为约束的求解问题，能够提高原子违背探测的精度。