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

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

现的各种因果和互斥关系进行处理.为此,首先定义多线程程序操作间的依赖和互斥关系如下.
定义 1(操作的依赖与互斥关系). 给定一个多线程程序的运行轨迹σ=e 1 e 2 e 3 ...e n .
(1) 若事件 e i 与 e j 同属一个线程(即 e i .thread=e j .thread)且 i<j,则称 e i 和 e j 之间存在线程内因果依赖关系,
记为 e i < thread e j ;
(2) 若 e i =start(u,v),存在 k≤i 使得 e k .thread=u,存在 m>i 使得 e m .thread=v,则称 e k 与 e m 之间存在线程间因
果依赖关系,记为 e k < start e m ;若 e i =join(u,v),存在 k<i 使得 e k .thread=v,存在 m≥i 使得 e m .thread=u,则也称
e k 与 e m 之间存在线程间因果依赖关系,记为 e k < join e m ;
(3) 设 e i =acq(u,o),e j =rel(u,o),i<j,且 e i 与 e j 之间不存在事件 rel(u,o),但存在事件 e m =start(u,v),则对于区间
[m,j]中的任意整数 k 与线程 v 的任意操作 e,只要 e k .thread=u,就称 e k 与 e 之间存在“锁-start”耦合因果
依赖关系,记为 e k < lock_start e;
统称前述 3 种关系为因果依赖,记为<;
(4) 设 e i =acq(u,o1),e j =acq(v,o2),且两者相互间不具备前述 3 种因果依赖关系,记线程 u 执行 e i 时持有的锁
集为 lockSet(e i ),线程 v 执行 e j 时持有的锁集为 lockSet(e j ).若 lockSet(e i )∩lockSet(e j )≠∅,则称 e i 和 e j 之
间存在锁集互斥关系,记为 e i # lockSet e j ;
(5) 设 e i =acq(u,o1),e j =acq(v,o2),且两者相互间不具备前述 3 种因果依赖关系和锁集互斥关系,记线程 u
获取 lockSet(e i )中各把锁的过程中曾经获取过的所有锁的集合为 lockSet_OnceHeld(e i ),称之为 e i 执行
时的历史持有锁集;类似可得 e j 对应的历史持有锁集 lockSet_OnceHeld(e j ).记 Lock_IntSecion=lockSet_
OnceHeld(e i )∩lockSet(e j ),若要使得 e i 与 e j 能并发以导致死锁,则对于∀o∈Lock_IntSecion,线程 u 获取
历史持有锁 o 的操作 e′ = acq (, )u o 应先于线程 v 最后一次获取持有锁 o 的操作 e′ = acq (, )v o 而执行,
i j
称 e′ 与 e′ 之间存在“历史持有锁-持有锁”耦合因果依赖关系,记为 e′ < e′ .
i j i lock _ held j
不难发现:对于上述 5 类关系,若遗漏线程内依赖关系,则可能导致单线程环死锁误报;若遗漏线程间因果依
赖关系,则可能出现 start/join 导致的因果环死锁误报;若遗漏锁集互斥关系,则可能导致门锁环误报;若遗漏“锁
-start”耦合因果依赖关系和“历史持有锁-持有锁”耦合因果依赖关系,则可能导致本文所给程序实例中的误报.
已有的各类基于锁图及其各种变形模型的死锁动态分析方法主要识别和处理前 3 种关系导致的误报,难以解
决本文给出的两种新型关系导致的误报.
针对上述问题,本文一方面在扩展锁图的基础上添加语句的执行时序信息,以区分循环中不同轮次的锁获
取操作,据此提出时序增广锁图的概念;另一方面,在分段图的基础上扩充锁的申请和释放信息,以此识别锁获
取和释放操作与线程 start 操作耦合引起的因果关系,在此基础上对分段图作进一步细化,由此提出了锁增广分
段图的概念;最终,综合两个工具提出一种更为准确的死锁检测方法.下面给出具体介绍.

2 锁增广分段图与时序增广锁图的构造
本节对多线程程序的运行轨迹给出形式化定义,并对锁增广分段图和时序增广锁图的构造规则予以说明.

2.1 多线程程序的运行轨迹
定义 2(多线程程序运行轨迹). 对于一个多线程程序,其运行轨迹定义为死锁相关的并发原语在执行过程
中形成的轨迹σ,严格定义如下:
*
σ∈ConPrimitive ,
ConPrimitive::=start(u,v)|stop(v)|join(u,v)|acq(u,l)|rel(u,l).
其中,
*
• ConPrimitive 表示各类并发原语的集合,ConPrimitive 为并发操作构成的序列全体;
• u,v∈Tid 表示线程,l∈Lock 表示锁;
• start(u,v):线程启动线程;