Page 125 - 《软件学报》2021年第7期

高凤娟 等:高精度的大规模程序数据竞争检测方法 2043

Fig.3 Simplified analysis procedures for Fig.1
图 3 图 1 示例的简化分析过程

MHP 分析.GUARD 通过为 TFG 节点构建线程标签来表示 MHP 信息.首先提取出线程相关的信息(即
thread_create 和 thread_join),并用线程标签对它们建模.然后基于线程标签分析两条路径的 MHP 关系.图 3(b)
中展现了每个节点简化的线程标签.初始标签集是,然后 thread_create 函数创建了一个新的线程标签.线程标
签包含两种标签,一类以1,T,表示,分配给刚创建的线程.它所对应的标签是1,C,1,在 thread_create 调用点之
后被赋给节点.在 thread_join 的调用点处,添加一个标签(1,C,1),表明这个标签执行了等待线程终止这个操作.线
程标签中的第 1 个元素是 thread_create 的标识,第 2 个元素表明了标签类型,最后一个元素用于区分不同的调
用上下文.和()分别表示 thread_create 和 thread_join 所对应的标签集.有关线程标签的详细讨论见第 3.1.1 节.
Source-Sink 框架.该框架基于值流分析(value flow analysis),自动依据与特定缺陷对应的 source-sink 模式
分析缺陷.很多软件缺陷都可以被表达为如下的形式:在任意一个程序中,一个由程序事件 A 生成的值 v 一定能
够流向另一个程序事件 B 中的一个值 [24] .所以,该框架检测任何一个能够被建模成基于 source 和 sink 模式的全
局值流的缺陷.并且,检测出的由 source 到 sink 的路径并不会由程序入口开始.
数据竞争检查器.如图 3(c)所示,最后一步是竞争检测,这依赖于 Source-Sink 框架以及 MHP 分析.首先,它会
基于 source-sink 框架检测读-写或写-写对.source 和 sink 都被设定为对变量的读或写操作,因此第 7 行、第 9
行和第 14 行的变量 arg 同时为 sources 和 sinks.接着,GUARD 分析程序的值流,找到从 source 到 sink 的路径.
在这一步中,检测到的 source-sink 路径是14,4,7和14,4,9.然后根据这两条路径的子路径(即{4,7,4,14}和
{4,9,4,14})提取出线程标签以及路径约束.最后一步是根据它们所对应的线程标签和路径约束检测数据竞
争.由于第 4 行创建的线程在第 8 行执行了等待结束操作,14,4,9并不是 MHP 的,因此对于启发性示例,GUARD
只会报告一个数据竞争对14,4,7.
前文展示的启发性示例描述了 GUARD 检测数据竞争的基本思路.接下来,本文将介绍有关检测实际程序
数据竞争时的分析细节.

2.3 线程模型
图 1 的示例程序中只包含两种线程操作:thread_create 和 thread_join.现代编程语言提供了种类繁多的线程
操作来实现不同的并行模式.本文考虑如下 6 种具有代表性的函数.
,
,
)
_
 thread create (tid routine para 接受 3 个参数:一个线程标识号(线程 ID)、一个指向所要执行任务的指
针及其所需的单个参数值.
 thread _ join (tid 等待 tid 所指明的线程终止.
)
_
_
 thread notify ()c 唤醒执行了 thread wait ()c 的线程.