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

2044 Journal of Software 软件学报 Vol.32, No.7, July 2021

_
)
 thread lock (mutex 和 thread unlock (mutex 给 mutex 加锁或去锁.
_
)
2.4 线程流图
GUARD 首先生成函数级 TFG,并根据线程操作和函数调用将函数级 TFG 连接起来构建起一个全局 TFG.
TFG 定义为   ( , ), 它包含一个点集   {,n  ,n m } 以及一个由有向边组成的边集   {,E  1 ,E K }, 其
1
中,K 是边的种数,E k 是类型为 k 的边的集合.在一个函数级 TFG 中,每个节点由指令序列构成,彼此间以控制流
指令或函数调用为分割.为了连接各节点,TFG 引入用于指明控制流的边 flow .与 CFG 类似,TFG 也有一个入口
节点和一个出口节点(在  中).入口节点没有入边而出口节点没有出边.
在一个全局 TFG 中,函数调用中的调用者和被调用者由 6 种边连接,分别是: call 、 create 、 join 、 notify 、
 lock 和 unlock .其中, create 将 thread_create 的调用点连接至线程的入口点; join 将线程的出口点连接至 thread_
join 的调用点;thread_notify 的调用点通过 notify 与相应的 thread_wait 的调用点连接起来;从 n 1 到 n 2 的同步边(即
 notify )表明:一旦 thread_wait 在 n 2 处执行,n 2 必定会接收到来自 n 1 的消息;thread_lock 或 thread_unlock 的调用
点通过 lock 或 unlock 连接至其后继节点.其他函数调用通过 call 将它们的调用点连接至对应的被调用者的入
口点.除此之外,后 5 种边需要通过线程标识符(thread ID)匹配对应的操作,例如 thread_join 需要匹配与其参数
(即线程标识符)对应的,且由 thread_create 创建的线程.这一部分通过值流分析实现(见第 3.2 节).
从 TFG 中可以看出,同一节点中的所有指令拥有相同的 MHP 关系.此外,相邻节点可能也具有相同的 MHP
关系.为了提高 MHP 分析的效率,GUARD 根据算法 1 将具有相同 MHP 信息的邻接节点合并为一个.对于按拓
扑序排列的每个函数级 TFG(第 1 行),首先用函数调用对 TFG 节点进行标记(第 3 行).allMinimalLoopOrBranch
抽取出循环及分支所对应的节点.如果存在嵌套的循环或分支,它只获取最深层的循环或分支.换言之,给定一
i
,
,
个嵌套的分支或循环   {,l  1 , },l n 其中,l i 包含点集  分析出 l j s.t. l l j   l i . 之后对于 allMinimal
i
l
LoopOrBranch 抽取出的每个循环或分支,对其相应的节点进行标记(第 5 行~第 8 行).在标记节点之后,基于循环
或分支对节点进行合并.该算法一直合并节点,直到没有节点可以被合并(第 10 行~第 14 行).
算法 1. Compressing Thread-flow Graph.
Input: TFG 
;
. 
Output: Compact TFG 

(1) for  in reversedTopologicalOrder(  ) do
f
(2) //It marks function calls, including thread operations.
(3) markNodeWithFunctionCall(  );
f
(4)  =allMinimalLoopOrBranch(  );
f

(5) for  do
v
(6) if  , is Marked ( )v  true then
(7) for v do
(8) markNode( v );
(9)     f f ;

(10) while  is unchanged do
f
(11)  =allMinimalLoopOrBranch(   );
f

(12) for  do
v
(13) if  , is Marked ( )v  false then
(14) mergeNodes(  );
3 GUARD 分析方法
本节将展示 GUARD 分析一个程序时的详细步骤.首先,具体阐释 GUARD 如何通过 TFG 分析 MHP 关系.
之后,基于 source-sink 检测出数据访问对,并根据 MHP 分析筛除不可行路径.最后,通过约束求解器求解路径约