基于绝对地址汇聚的数据访问冲突检测方法

摘要

基于绝对地址汇聚的数据访问冲突检测方法，是一种针对航天嵌入式C程序数据竞争检测的改进方法。本发明以语法分析技术为基础，结合领域知识，更准确地识别的数据竞争，降低数据竞争检测的漏报率。该方法对C源程序进行语法分析，构造源程序中使用的绝对地址集合，利用绝对地址集合，构造间接影响关系。根据C源程序中的中断响应函数，寻找C源程序包括的所有中断上下文。根据绝对地址之间的间接影响关系，判断中断上下文是否会触发数据访问冲突。与现有的数据访问冲突检测方法相比，本发明所提出的方法，能够降低漏报，提高分析准确度。

主权项

1.基于绝对地址汇聚的数据访问冲突检测方法，其特征在于步骤如下：（1）对C源程序进行语法分析，构造源程序中使用的绝对地址集合；利用绝对地址集合，构造间接影响关系；所述的间接影响关系是一组绝对地址上的一一映射关系，具有一一映射关系的两个绝对地址中，对其中一个绝对地址的写操作会导致另一个绝对地址的读操作的结果发生变化；（2）根据C源程序中的中断响应函数，寻找C源程序包括的所有中断上下文；（3）对于步骤（2）中确定的每个中断上下文，进行下列检查：（31）将C源程序的主程序中进行读操作的绝对地址构成的集合记作R₁，写操作构成的集合记作W₁，将C源程序的中断中进行读操作的绝对地址构成的集合记作R₂，写操作构成的集合记作W₂；（32）令w₁=closure(E,W₁)，w₂=closure(E,W₂)，其中E为步骤（1）中的间接影响关系；w_i=closure(E,W_i)，i=1、2的计算步骤如下：（321）令w_i=W_i；（322）对任意的d∈w_i，令w_i'=w_iU{E(d)}；其中E(d)为绝对地址d所处的间接影响关系对应的绝对地址；（323）如果w_i=w_i'那么w_i=closure(E,W_i)计算完毕，否则令w_i=w_i'，并回到步骤（322）；（33）令A=(w₁∩w₂)U(w₁∩R₂)U(R₁∩w₂)；如果A=，那么没有数据访问冲突；否则判定在集合A中的绝对地址处发生数据访问冲突。