Page 116 - 《软件学报》2021年第6期

1690 Journal of Software 软件学报 Vol.32, No.6, June 2021

段的开头,此时无需添加新的分段,s′_new 为 6);
(2.2) 与 s″同属一个线程的、s″的子孙节点中必然存在一个以 l 的释放为尾操作和分段点的段 s″_desc
(例如图 2 种的 5 号段),显然,s″_desc 与 s′_new 存在一种依赖关系,仅当 s″_desc 执行结束、释放
l 后,s′_new 中的操作方能执行,故在 s″_desc 与 s′_new 之间添加一条有向弧(例如,图 2 种由 5 号
段到 6 号段之间的有向弧).
相比传统的分段图,锁增广分段图中添加的锁授权和释放信息有助于死锁检测过程中计算各个操作执行
前历史曾经持有的锁信息,而且按前述规则对段进行细分后,能够刻画锁的释放和授权操作引起的段之间的因
果关系,这为后续准确地进行死锁检测奠定了基础.锁增广分段图的形式化定义及构造规则如下(与传统分段图
构造规则不同的部分加粗显示).
定义 3(锁增广分段图). 给定一个多线程程序的运行轨迹σ=e 1 e 2 e 3 ...e n ,其对应的锁增广分段图 SegG_Lock σ
是满足如下条件的四元组(SegSet σ ,SegR σ ,ϕ s ,ϕ r ),其中,SegSet σ 是顶点集,SegR σ ⊆SegSet σ ×SegSet σ 是关系集,ϕ s 与ϕ r
分别是定义在顶点和边上的标签函数:
(1) SegSet σ 是顶点集,每个顶点对应程序的一个分段,其生成规则如下.
(a) 添加一个 0 号段作为主线程的初始分段;
(b) 每当有线程 u 执行操作 start(u,v)时,则在线程 u 此操作之处添加一个新段,并为线程 v 添加一个
初始分段;
(c) 每当有线程 u 执行操作 join(u,v)时,则为线程 u 添加一个新分段;
(d) 每当有一个线程 u 在段 s 中执行操作 rel(u,l)时,若 u 此前获取 l 的操作不在段 s 中,则在此处为
线程 u 添加一个新段;
(e) 每当有一个线程 v 在段 s′中执行操作 acq(v,l)时,从该段节点逆向寻找第一个获取锁 l 的段节点
s″,若 s″所属线程 u≠v 且 s″中未释放 l,则将 s′从当前 l 的获取操作处开始一个新的分段,记其段号
为 s′_new(若 acq(v,l)是 s′的第 1 个操作,则不必添加新分段,令 s′_new:=s′即可);记与 s″同属线程
u 的、s″的子孙节点中第 1 个以 rel(u,l)为尾操作的段为 s″_desc,将(s″_desc,s′_new)加入关系集
SegR σ ,并令这个关系对应的ϕ r 标签函数值为 rel(u,l);
(f) 每个段设置一个全局唯一的段号作为其 ID(从 0 开始递增,每次增加 1);
(2) SegR σ ⊆SegSet σ ×SegSet σ 记录段之间执行次序上的先后关系,ϕ r 是定义在 SegR σ 上的标签函数,他们的
产生和定义规则如下.
(a) 每当有线程 u 执行操作 start(u,v)时,记线程 u 之前的最后一个段为 latest_Seg(u),记因为这个操
作而为 u 和 v 添加的新段为 new_Seg(u)和 new_Seg(v),向 SegR σ 中添加两个新关系(latest_Seg(u),
new_Seg(u))和(latest_Seg(u),new_Seg(v));并令这两个关系对应的ϕ r 标签函数值为 start(u,v);
(b) 每当有线程 u 执行操作 join(u,v)时,记线程 u 之前的最后一个段为 latest_Seg(u),记因为这个操作
而为 u 添加的新段为 new_Seg(u),向 SegR σ 中添加新关系(latest_Seg(u),new_Seg(u));并令这该关
系对应的ϕ r 标签函数值为 join(u,v);
(c) 每当有线程 v 执行操作 stop(v)时,若之前曾有线程 u 执行操作 join(u,v),并假设线程 u 由于操作
join(u,v)而新添加的分段为 new_Seg(u),同时记线程 v 的最后一个段为 latest_Seg(v),则向 SegR σ
中添加新关系(latest_Seg(v),new_Seg(u));并令这两个关系对应的ϕ r 标签函数值为 join(u,v);
(d) 每当有线程 u 因执行锁的释放 rel(u,l)操作而添加一个新段 s 时,记线程 u 之前的最后一个分段
为 s′,将(s′,s)加入关系集合 SegR σ 中,并令这个关系对应的ϕ r 标签函数值为 rel(u,l);
(e) 每当有线程 u 因执行锁的获取 acq(u,l)操作而添加一个新段 s 时,记线程 u 之前的最后一个分段
为 s′,将(s′,s)加入关系集合 SegR σ 中,并令这个关系对应的ϕ r 标签函数值为 acq(u,l);
(3) ϕ s 是定义在 SegSet σ 上的标签函数,其生成规则如下.
(a) 每个段最初生成时,其ϕ s 标签函数值为空;