基于多线程程序约束构建的数据竞争检测与证据生成方法

摘要

一种基于多线程程序约束构建的数据竞争检测与证据生成方法，根据多线程程序语义构建约束表达式，将数据竞争检测问题转化为约束求解问题，采用约束求解器检测可能存在的数据竞争，并生成触发数据竞争的程序执行路径，首先插桩被检测程序，执行此程序并得到执行路径；其次根据多线程程序执行语义将执行路径转化为无量词一阶逻辑表达式，此约束表达式涵盖所有可行的线程交织；然后根据发生数据竞争时语句间时序关系构建数据竞争候选集合，生成候选发生竞争的条件；最后遍历候选集合判定是否存在数据竞争，如有则生成对应的证据序列，本方法可找出一次执行中所有的数据竞争且不存在误报情况，对每一个数据竞争都生成一个展示了数据竞争触发过程的证据序列。