(19)国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202210536587.2 (22)申请日 2022.05.17 (71)申请人 大连理工大 学 地址 116024 辽宁省大连市甘井 子区凌工 路２ 号 申请人 北京轩宇信息技 术有限公司 (72)发明人 屈磊　张媛　吴逸飞　陈睿　 于婷婷　孔维强　 (74)专利代理 机构 辽宁鸿文知识产权代理有限 公司 21102 专利代理师 许明章　王海波 (51)Int.Cl. G06F 9/48(2006.01) G06F 9/50(2006.01) (54)发明名称 基于单变量访问序模式的中断数据竞争模 型检测方法 (57)摘要 本发明公开了一种基于单变量访问序模式 的中断数据竞争模型检测方法， 属于软件模型检 测领域。 首先选择待检测模式并输入待检测变量 的名称和类型， 然后对中断程序进行顺序化处 理， 根据选择的模式在待检测变量的读写语句前 后添加赋值语句和断言， 再将其输入 给有界模型 检测工具CBMC， 最终根据返回结果得到待检测变 量是否存在该种模式的数据竞争。 此方法可以检 测中断程序中存在的特定单变量访问序模式， 同 时对反例路径进行 可视化。 权利要求书2页 说明书4页 附图2页 CN 114924852 A 2022.08.19 CN 114924852 A 1.一种基于单变量访问序模式的中断数据竞争模型检测方法， 其特征在于， 包括以下 步骤： 1)指定待检测的单变量访 问序模式和全局变量： 指定单变量访问序模式读写写、 写写 读、 读写读或写读写中的某一种模式； 同时需要给定待检测全局变量名， 若是数组的某个单 元则需要给定数组名和下 标； 2)源中断程序顺序化： 先将中断驱动程序转为多线程程序， 再将多线程程序顺序化， 使 得顺序化程序的执行能够模拟多线程程序里 的线程交互执行情况； 同时增加约束， 使得程 序的执行顺序满足源中断程序的优先级要求， 并且顺序化程序里能支持源中 断程序里的各 种中断使能和中断去能操作； 3)自动添加断言： 在步骤2)所得到的顺序化程序里， 对检测到的关于全局变量的读或 写语句， 根据指定的模式和读或写添加赋值语句和断言； 4)调用有界模型检测工具： 将步骤3)得到的顺序化程序作 为输入， 设置参数， 用有界模 型检测工具CBM C验证其中的断言； 5)得出验证结果： 若存在程序中的断言为假， 则根据反例路径将具体的语句按照执行 的先后顺序进行 可视化。 2.根据权利要求1所述的一种基于单变量访问序模式的中断数据竞争模型检测方法， 其特征在于， 步骤3)中， 自动添加断言的过程包括： 选取并发流组合； 遍历并发流， 判断每条 语句的读写类型； 若该语句是指定的全局变量的读写语句， 则根据指定的单变量访问序模 式处理方法自动添加赋值语句和断言； 若该语句不是指定的全局变量的读写语句， 则不做 处理， 继续判断下一条语句； 具体如下： 3‑1)选取并发流组合： 在单变量访问序模式中， 需要先确定 并发流组合； 一个并发流组 合包含一个并发流 1和一个并发流2， 其中并发流 1具有低优先级， 并发流2具有高优先级； 故 并发流1在主函数和除最高优先级以外的所有中 断构成的集合里选取， 并发流2在所有中 断 构成的集 合里选取； 3‑2)遍历并发流， 判断每条语句的读写类型： 对顺序化程序代码进行解析， 生成抽象语 法树AST对象， 可以得到每条语句的类型； 根据指 定的全局变量在语句中的位置判断该语句 的读写类型； 如若为if判断语句且条件为关于全局变量的表达式， 则该语句属于该全局变 量的读； 若为赋值语句且全局变量在等号左边， 则该语句属于该全局变量的写； 若为赋值语 句且全局变量在等 号右边， 则该语句属于该全局变量的读； 3‑3)不同情况 下各个单变量访问序模式处 理方式 (a)读写写模式处理方法： 在顺序 化程序中定义和待检测变量同类型的变量reader_i， write_i， 以及整型的读操作计数器变量num_i， i为所选并发流1对应的编号； 在并发流1中 关于全局变量的读 语句之后插入 赋值语句将该变量的值赋给变量reader_i， 同时将读操作 计数器变量num_i加1； 在并发流1中关于全局 变量的写语句之前插入赋值语句将该变量的 值赋给变量wr ite_i， 同时使用if语句判断读操作计数器变量num_i是否不为0， 若满足则插 入断言assert(write_i＝＝reader_i)， 并将读操作计数器变量num_i置为0； 对 并发流2不 做处理； (b)写写读模式处理方法： 在顺序化程序定义和待检测变量同类型的变量reader_i， write_i， 以及整型的写操作计数器变量num_i， i为所选并发流1对应的编号； 在并发流1中权　利　要　求　书 1/2 页 2 CN 114924852 A 2关于全局 变量的写语句之后插入赋值语句将该变量的值赋给变量write_i， 同时将写操作 计数器变量num_i加1； 在并发流1中关于全局 变量的读语句之前插入赋值语句将该变量的 值赋给变量reader_i， 同时使用if语句判断写操作计数器变量num_i是否不为0， 若满足则 插入断言assert(write_i＝＝reader_i)， 并将写操作计数器变量num_i置为0； 对 并发流2 不做处理； (c)读写读模式处理方法： 在顺序 化程序中定义和待检测变量同类型的变量reader_i， tmp_i， 以及整型的写操作计数器变量num_i， i为所选并发流1对应的编号； 在并发流1中关 于全局变量的读 语句之后插入 赋值语句将该变量的值赋给变量reader_i， 再使用if语句判 断读操作计数器变量num_i是否不为0， 若满足则添加断言assert(reader_i＝＝tmp_i)， 最 后将读操作计数器变量num_i加1， 并将reader_i值赋给缓存变量tmp_i； 在并发流1中关于 写操作之后将 读操作计数器 变量num_i置0； 对并发流2不做处 理； (d)写读写模式处理方法： 在顺序化程序中定义整型变量a_i， 以及整型的写操作计数 器变量num_i， i为所选并发流1对应的编号； 在并发流1中关于全局 变量的写语句之后使用 if语句判断写操作计数器变量num_i是否不为0， 若满足则添加断言assert(a_i＝＝0)； 最 后将写操作计数器变量num_i加1， 并将a_i置为0； 在并发流2中关于全局变量的读 语句之后 将变量a_i置为1。权　利　要　求　书 2/2 页 3 CN 114924852 A 3