Page 127 - 《软件学报》2021年第7期
P. 127
高凤娟 等:高精度的大规模程序数据竞争检测方法 2045
束并得到最终的数据竞争警报.
3.1 MHP分析
GUARD 应能快速、准确地查询 query 关系以减少潜在的数据竞争数量.为了实现这一点,我们设计了线程
流图(TFG),用于为线程操作建模.基于 TFG,将 MHP 关系编码为线程标签,并使用转换规则模拟由线程操作所引
入的语义信息.最后,根据 TFG 以及转换规则总结出 MHP 关系.
3.1.1 线程标签流
在构建完 TFG 之后,GUARD 使用线程标签及预设的转换规则来建模线程操作所引入的语义信息.首先,线
程标签的定义如图 4 所示.CT 是一个调用序列,它由一系列调用点 CS i 拼接而成, 是 L 的集合,其中,L 是由一个
三元组 ID ,,T CT 表示的线程标签.ID 指明何种线程操作,T 表示标签种类,可以是 Thread、CS 或 Other. Thread
_
_
_
意味着该标签是由 thread create 创建的,并且 CS 是 thread create 的调用点. Other 代表不由 thread create 创
建的标签.CT 表示由调用点标识组成的调用轨迹.一个节点的 MHP 关系由一个五元组 NodeID , , , 表
,
c j wn l
_
示. NodeID 是当前节点的标识, 是线程标签集. 、 、 、 分别代表 thread create 、 thread _ join 、
c j wn l
_
_
thread_wait、 thread notify 和 thread lock 所对应的线程标签集.
Fig.4 Definition of thread labels
图 4 线程标签定义
接下来,对于每个函数,根据图 5 中的转换规则对线程标签进行转换. TL ( )[ ]n t 表示查找节点 n 对应的 其
,
t
中, t { , ,c j wn , }.l 如果 t 未给出,则通过 TL ()n 表示检索出节点 n 的 NL(图 4 中定义).N(CS)用于查找出具有调用
点 CS 的节点.N i (CS)和 N o (CS)代表 CS 所在函数级 TFG 的入口点和出口点. n t n 表示 n i 通过类型为 t 的边
i
j
)
连接至 n j .注意,n i (或 n j )可能为 N(CS)(即 N (CS t n ),这时它表示一个具有调用点 CS 的节点通过类型为 t 的边
j
)
(
连接至 n j . NCS 和 NCS 分别表示节点 N(CS)之前和之后的点. Succ ()n 和 Pred ()n 表示 TFG 中节点 n i 的后
)
(
i
i
继和前驱. Obj Oper Obj j 代表通过 Oper 的一次赋值,例如 Obj i Obj 表示合并这两个集合并复制给 Obj i .
j
i
Flow 规则表示一次基本的线程标签转换.如果有 k 个节点通过 flow 与点 n m 相连,它将来自前驱节点(例如
分支)的 合并,并取 、 、 各自的交集.如果一个节点只有一个前驱节点,其后继节点与前驱节点拥有相
c j wn l
同的线程标签.
Call 规则用于在函数调用处转换线程标签.当一个线程标签集合到达一处函数调用时,调用点将其当前的
标签集传递给被调用者,调用点的输出标签集则是合并被调用者出口节点的标签集.
_
Create 规则对应 thread create 操作的转换规则.注意,线程的创建引入两个新的标签(L CS 和 L T ),这两个标
签被添加至 NL 中对应的 内.在被创建的线程上,该规则将标签传递给被创建线程并将它们合并.在 thread_
C
create 的调用点,只将 中的标签合并,而不是将 4 个集合中的标签都合并.这是线程创建和函数调用两个规则
C
在标签传播上的核心区别.在一个函数调用中,被调用者可被视为一个内联函数,这意味着调用点之前的线程标
签与被调用者出口节点之前的线程标签是相同的.类似地,调用点之后的线程标签和被调用者出口节点之后的
线程标签是相同的.相比之下,线程的创建操作引入了不同的语义,因而不能被视为内联函数,所以 GUARD 为函
数调用和线程创建定义了两种转换规则.
Join Wait、 / Notify Lock Unlock CallingContext、 、 、 规则展现了剩余线程操作的线程标签流.Join 规则表示,
/
如果一个标签 L j 被等待终止,则会将标签添加至 join 集中.Wait Notify 规则说明会将一个 ID(即这两种操作的
_
_
唯一标识)加入 thread notify 所有前驱节点以及 thread wait 所有后继节点(包括过程间节点)的标签集中.