Zircon 和 Fuchsia 中的运行时锁验证

简介

锁验证是一种检查程序中锁定行为一致性以发现潜在死锁危险的技术。本文档讨论了静态和动态锁定验证方法的相关方面,并介绍了 Zircon 和 Fuchsia 中提供的运行时锁定验证库的基础。

背景

锁定验证可以静态或动态方式执行。下文总结了锁定验证的静态方法与动态方法之间的重要区别:

  • 执行验证时:编译时与运行时。
  • 验证工具在发现潜在问题方面的效果。
  • 程序员需要何种程度的参与。
  • 验证本身的开销成本。

静态验证

静态验证通常在编译时通过分析编译器或其他源代码级处理器生成的调用图来执行。采用这种方法时,有必要对代码进行插桩并使用注解锁定基元,以告知验证程序哪些类型表示锁,以及哪些规则应该(或不应用)到使用这些锁类型的代码。

静态验证的好处包括在构建时及早发现问题、确定性验证结果和零运行时开销。这种属性组合使得始终启用静态验证变得很有吸引力,以确保通常在代码进入 build 之前发现锁定问题,而不会影响 build 工件的性能。

静态验证也存在一些缺点。一个问题是,静态验证需要以正确、一致的方式对锁和代码应用各种注解,以提供有用的结果。除非实施严格的代码审核标准,否则这可能会导致维护问题。另一个问题是,静态验证的可见性有限,可能会被跨编译单元的条件路径、动态调度、移动语义和锁定依赖项所欺骗。

动态验证

动态验证在运行时在线执行,方法是在执行代码时观察锁之间的关系。使用这种方法,通常只需插桩锁定基元和获取/释放操作,即可提供验证所需的信息。

动态验证的优势包括更简单的插桩(从用户的角度来看),并且有可能更深入地了解程序的实际运行时行为。这使得动态验证在大型代码库中非常有用,在大型代码库中,静态验证可能无法看到全部可能的锁交互。

动态验证的主要缺点是运行时开销和执行覆盖率要求。由于动态验证必须在运行时跟踪锁互动,因此除了跟踪数据本身的内存开销之外,每次获取和释放都会产生非零的执行费用来更新跟踪数据。运行时跟踪还会导致验证程序无法分析未执行的代码路径。如果尚不是项目要求,这可能会增加开发者和质量检查人员的负担,以确保足够的执行覆盖率。

锁定排序不变

锁验证器的工作是确定程序的锁是否不变。主要不变量是两个或多个锁之间的顺序:一个程序中获取两个或更多锁的所有路径都必须与涉及两个或多个相同锁的所有其他路径一致,以避免发生死锁问题。处理硬件中断的环境(例如嵌入式系统和内核)具有额外的排序不变,以避免由中断引起的死锁。以下小节介绍了这些不变量。

基本反转

如果一个程序有两个锁,而这两个锁在不同路径中顺序不一致,则依序获取,则是最简单的反转形式。

例如,如果某个程序具有锁 AB 以及代码路径 P1P2,并且以下行为就可能会出现死锁:

路径 P1 获取和释放序列中的锁:

  1. 获取(A)
  2. 获取(B)
  3. 版本(B)
  4. 版本(A)

路径 P2 按反转序列获取和释放锁:

  1. 获取(B)
  2. 获取(A)
  3. 版本(A)
  4. 版本(B)

如果采用正确交错,则可能是由于两个路径在不同线程上并发执行,当路径 P1 持有锁 A 并等待锁 B 时,就会发生死锁;而路径 P2 持有锁 B 和块等待锁 A

循环依赖项

两个以上的锁定和路径之间也可能会发生反转。通过手动检查识别这种反转要困难得多,因为涉及的每对锁在仅涉及这些锁对的每条路径中看起来都似乎有正确的排序,但考虑到锁的总体顺序,可能存在潜在的死锁。

例如,一个程序包含锁 ABC;路径 P1P2P3;以下行为可能会导致死锁:

路径 P1 获取和释放序列中的锁:

  1. 获取(A)
  2. 获取(B)
  3. 版本(B)
  4. 版本(A)

路径 P2 获取和释放序列中的锁:

  1. 获取(B)
  2. 获取(C)
  3. 版本(C)
  4. 版本(B)

路径 P3 获取和释放序列中的锁:

  1. 获取(C)
  2. 获取(A)
  3. 版本(A)
  4. 版本(C)

在路径 P1P2P3 的正确交错的情况下,当每条路径在第一步获取锁并在第二步等待锁时,就会发生死锁。在实践中,存在生成相同成对锁定序列的不同路径可能会使这种情况更加复杂。

IRQ 安全排序

在处理硬件的系统中,中断 irq 安全锁和非 irq 安全锁之间的排序至关重要:当持有 irq 安全锁以防止间接锁反转时,不得获取非 irq 安全锁。Irq 安全锁保留了 irq 和非 irq 上下文之间的排序;两个或多个 irq 安全锁的一致顺序保证对于在 irq 和非 irq 环境中运行的路径而言是安全的。对于非 irq 安全锁也是如此。其原因在于,非 irq 安全锁允许 irq 处理程序在中断任务的锁定序列的任意点有效地插入处理程序获取的锁。

例如,如果系统具有非 irq 安全锁 A 和 irq 安全锁 Birq,路径为 P1P2 和 irq 路径 Pirq,则以下行为可能会导致死锁:

CPU1 上的路径 P1 会依序获取和释放锁:

  1. 获取(A)
  2. Pirq 会在 CPU1 上中断
  3. 版本(A)

CPU1 上的路径 Pirq 会依序获取和释放锁:

  1. 获取(Birq)
  2. 版本(Birq)

CPU2 上的路径 P2 会依序获取和释放锁:

  1. 获取(Birq)
  2. 获取(A)
  3. 版本(A)
  4. 版本(Birq)

在路径 P1P2Pirq 的正确交错的情况下,当 Pirq 尝试获取 Birq 时,P2 持有 Birq 且块等待 A 时,便会发生死锁。这是一种间接锁反转:Pirq 在路径 P1A 的获取/释放序列中间有效地插入了 Birq 的获取/释放序列,此序列与路径 P2 中相同锁的锁定序列不一致。

执行验证

上一部分中介绍的不变量可以使用有限有向图进行验证。在分析遍历代码路径时,有向图会跟踪锁的身份和顺序。您可以通过遍历编译器或源代码级处理器生成的调用图(静态分析)或通过在程序执行期间观察锁的顺序(动态分析)来构建此类图。本部分用抽象的术语来介绍这两种方法的过程,为以后制定具体的动态分析策略做好准备。

一般来说,通过代码路径构建有向图需要在遍历路径时维护主动持有的锁的列表:每当获取锁时,系统都会将一个表示锁的节点添加到列表中,并在每次解锁时从列表中移除。除了维护活跃列表之外,系统还会向图添加一条定向边,即从表示新获取锁的顶点到每个表示列表中已有的锁的顶点。

基本反转示例

本部分说明了用于检测基本双锁反转的有向图方法。

让我们回想一下前面的示例,一个程序具有锁 AB;代码路径 P1P2;以及以下行为:

路径 P1 获取和释放序列中的锁:

  1. 获取(A)
  2. 获取(B)
  3. 版本(B)
  4. 版本(A)

路径 P2 按反转序列获取和释放锁:

  1. 获取(B)
  2. 获取(A)
  3. 版本(A)
  4. 版本(B)
路径分析 P1

从路径 P1 开始,我们定义并更新有向图。

L1 是路径 P1 持有的锁的有序的活动列表。

让 G = (V, E) 成为有向图,其中一组顶点 V 表示观察到的锁定,而顶点 E 之间的有向边集。

初始状态:

L1 V E
() {} {}

P1 第 1 步之后:

L1 V E
(A) {A} {}

此步骤将锁 A 添加到活动列表,并在有向图中引入一个锁的顶点。由于活跃列表中没有其他锁,因此不会添加边缘。

P1 第 2 步之后:

L1 V E
AB {AB} {(BA)}

此步骤向活动列表添加锁 B,并向图中引入一个相应的顶点。这一次,活跃列表包含锁,因此向图中添加了从新锁到现有锁的边。这条边缘表示锁 B 现在依赖于A在涉及这两个锁的其他任何路径中都先依赖锁。

P1 第 3 步之后:

L1 V E
(A) {AB} {(BA)}

B 已从活动列表中移除。图表没有更新。

P1 第 4 步之后:

L1 V E
() {AB} {(BA)}

A 已从有效列表中移除。图表没有更新。

路径分析 P2

L2 成为 P2 持有的锁的有效列表。

初始状态:

L2 V E
() {AB} {(BA)}

在这种情况下,初始状态是路径 P1 中的最终状态。

P2 第 1 步之后:

L2 V E
(B) {AB} {(BA)}

此步骤会向活动列表添加锁 B。由于活跃列表中没有其他锁,因此没有向图添加边。由于 B 在图中已有一个顶点,因此 V 也未发生变化。

P2 第 2 步之后:

L2 V E
BA {AB} {(B, A)、(A, B)}

此步骤会向活动列表添加锁 A。由于此锁定已有一个顶点,因此 V 没有变化。但是,由于活动列表中有一个锁定,因此从新锁定到现有锁定的边会添加到图中。利用这条新边,图表现在在顶点 A 和 B 之间形成循环,这表示这些锁定在目前为止考虑的两条路径之间的顺序不一致,并且可能存在死锁。

循环依赖项示例

本部分说明了使用不变量部分前面讨论的示例检测循环依赖关系反转的有向图方法。由于此插图与上一个插图类似,所以在一定程度上采用了缩写形式。

假设某个程序具有锁 AB 和 C 以及路径 P1P2P3 以及以下行为:

路径 P1 获取和释放序列中的锁:

  1. 获取(A)
  2. 获取(B)
  3. 版本(B)
  4. 版本(A)

路径 P2 获取和释放序列中的锁:

  1. 获取(B)
  2. 获取(C)
  3. 版本(C)
  4. 版本(B)

路径 P3 获取和释放序列中的锁:

  1. 获取(C)
  2. 获取(A)
  3. 版本(A)
  4. 版本(C)
路径分析 P1

L1 是路径 P1 持有的锁的有序的活动列表。

让 G = (V, E) 成为有向图,其中一组顶点 V 表示观察到的锁定,而顶点 E 之间的有向边集。

初始状态:

L1 V E
() {} {}

P1 第 1 步之后:

L1 V E
(A) {A} {}

P1 第 2 步之后:

L1 V E
AB {AB} {(BA)}

P1 第 3 步之后:

L1 V E
(A) {AB} {(BA)}

P1 第 4 步之后:

L1 V E
() {AB} {(BA)}
路径分析 P2

L2 是路径 P2 持有的锁的有序的活动列表。

初始状态:

L2 V E
() {AB} {(BA)}

P2 第 1 步之后:

L2 V E
(B) {AB} {(BA)}

P2 第 2 步之后:

L2 V E
BC {ABC} {(B, A)、(C, B)}

此步骤向活动列表添加锁 C,并向图中引入一个相应的顶点。活跃列表包含锁 B,因此系统从 C 到 B 添加了一条边缘。

P2 第 3 步之后:

L2 V E
(B) {ABC} {(B, A)、(C, B)}

P2 第 4 步之后:

L2 V E
() {ABC} {(B, A)、(C, B)}
路径分析 P3

L3 是路径 P3 持有的锁的有序的活动列表。

初始状态:

L3 V E
() {ABC} {(B, A)、(C, B)}

P3 第 1 步之后:

L3 V E
(C) {ABC} {(B, A)、(C, B)}

P3 第 2 步之后:

L3 V E
CA {ABC} {(B, A), (C, B), (A, C)}

此步骤会向活动列表添加锁 A。活跃列表包含锁 C,因此系统添加一个从 AC 的边缘。有了这条新边,图现在会在顶点(ABC)中形成循环,这表示循环依赖关系,并且如果路径 P1P2P3 以正确方式交错,则可能会出现死锁情况。

IRQ 安全排序示例

本部分介绍了使用不变量部分前面讨论的示例检测 irq-safe 订单违规行为的有向图方法。

回想一下上述示例系统,该系统具有非 irq 安全锁 A 和 irq 安全锁 Birq;路径 P1P2 和 irq 路径 Pirq;其行为如下:

路径 P1 按顺序获取和释放锁:

  1. 获取(A)
  2. 版本(A)

路径 Pirq 会依序获取和释放锁:

  1. 获取(Birq)
  2. 版本(Birq)

路径 P2 按顺序获取和释放锁:

  1. 获取(Birq)
  2. 获取(A)
  3. 版本(A)
  4. 版本(Birq)
路径分析 P1

L1 是路径 P1 持有的锁的有序的活动列表。

让 G = (V, E) 成为有向图,其中一组顶点 V 表示观察到的锁定,而顶点 E 之间的有向边集。

初始状态:

L1 V E
() {} {}

P1 第 1 步之后:

L1 V E
(A) {A} {}

P1 第 2 步之后:

L1 V E
() {A} {}
路径 Pirq 分析

Lirq 是路径 Pirq 持有的锁的有序的活动列表。

初始状态:

角色 V E
() {A} {}

Pirq 第 1 步之后,执行以下操作:

角色 V E
Birq {ABirq} {}

Pirq 第 2 步之后,执行以下操作:

角色 V E
() {ABirq} {}
路径 Pirq 分析

L2 是路径 P2 持有的锁的有序的活动列表。

初始状态:

L2 V E
() {A} {}

P2 第 1 步之后:

L2 V E
Birq {ABirq} {}

P2 第 2 步之后:

L2 V E
BirqA {ABirq} {(ABirq)}

此步骤会向活动列表添加锁 A。活跃列表包含锁 Birq,因此系统添加一个从 ABirq 的边缘。由于这是从非 irq 安全锁到 irq 安全锁的边缘,因此违反了 irq 安全排序不变性,并且存在潜在的死锁。

从理论到实现

本部分根据上一部分中的分析技术,制定了实现有向图验证器的具体策略。

该实现策略具有以下目标:

  1. 尽可能避免动态分配。
  2. 最大限度减少验证开销。
  3. 支持管理硬件中断的环境。

使用锁定类别移除冗余

在本文档前面的分析中,我们将锁视为抽象,这意味着所跟踪的对象是锁的各个实例。虽然跟踪单个实例会生成正确的结果,但有几种可能避免的结果:

  1. 随着锁实例的增加和消失,跟踪结构必须进行动态调整,这可能需要动态分配或其他实例数据存储。
  2. 当相同的代码路径以相同的方式使用多个锁实例时,该图会包含多余的信息。
  3. 因此,如果锁提供相同的函数,但尚未单独传播到所有必要的代码路径,则可能需要更长的时间才能识别违规行为。

一个重要的观察结果是,无论实例数是多少,提供相同函数的锁都应遵循相同的排序规则。

请考虑以下具有锁定成员的类型,以及同时更改这两种类型的操作:

struct Foo {
    Mutex lock;
    int data; GUARDED_BY(lock);
};

struct Bar {
    Mutex lock;
    int data; GUARDED_BY(lock);
};

void Swap(Foo* foo, Bar* bar) {
    foo->lock.Acquire();
    bar->lock.Acquire();

    int temp = foo->data;
    foo->data = bar->data;
    bar->data = temp;

    bar->Release();
    foo->Release();
}

由于操作 Swap 可以在 Foo 的任何实例以及 Bar 的任何实例上运行,因此 Swap 会在 FooBar 的所有实例的锁定之间建立顺序;如果在程序的其他部分以一致的方式应用此订单,则当 FooBar 的相同实例以不同顺序同时锁定时,可能会导致死锁。

请注意,您可能会有意或无意地隔离 FooBar 的不同集合,以使按不同顺序锁定的实例永远不会重叠。不过,这仍然很危险,因为对程序的输入、结构或时间做出的看似无害的更改可能会使隔离失败并引入潜在死锁。通过等效对 FooBar 的所有实例并在整个程序中应用相同的排序规则,可以完全避免此问题。

通过跟踪锁类(而不是锁实例),确保整个程序中的通用排序可以实现:每种类型中的每个锁成员都代表一个唯一的锁类。您可以使用与单个锁相同的有向图技术跟踪和分析每个锁类之间的关系。

跟踪锁定类具有以下优势:

  1. 静态分配的内存:由于所有锁定类在编译时都是已知的,因此可以预先将跟踪结构作为静态全局数据分配。
  2. 消除冗余图节点:同一类中的锁使用相同的跟踪结构。
  3. 更快地检测不变的违规行为:当锁定类别顺序不一致时,系统会检测到违规行为,即使所涉及的各个实例从未一起使用过。

其他排序规则

在锁定同一类的多个锁时,跟踪锁类引入了额外的排序注意事项。由于不跟踪单个实例,因此在必须同时获取同一类的多个锁时,需要采取额外的步骤来确保一致性。

外部有序锁

当分层或其他有序数据结构在每个节点中具有锁,并且必须同时持有多个每个节点的锁时,需要嵌套同一类。在这种情况下,数据结构或访问模式必须提供稳定的排序,用于保证锁的排序。

若要验证可嵌套的锁类,只需在每个可嵌套锁的“活动锁”列表中记录外部顺序,并在将同一类的新锁添加到列表中时进行比较。这种设计的后果是,其他锁类不得穿插在同一类的嵌套锁之间,而只能完全在嵌套锁集合之前或之后散布。

例如,不可嵌套的锁类 AB 以及可嵌套的锁类 N 可以按以下方式穿插显示:

AN0N1 ... NnB

但不像这样:

AN0BN1 ... NnAN0N1B ... Nn 或... 等等

在大多数情况下,这是一个合理的限制,因为在具有任意深度的嵌套结构中散布其他锁可能会导致在结构在运行时更新时反转。另一方面,如果嵌套仅限于几个级别,则为每个级别定义单独的锁定类(而不是使用嵌套类)可能更为有效。在这种情况下,可按照常规的锁排序规则在特定级别允许其他锁定。

地址排序

如果在不同的时间获取锁,如果没有外部提供的顺序,将很难泛化同一类的锁之间的锁排序。不过,您可以在同时获取多个锁时提供排序保证,而不需要时间分离。在这种情况下,锁可以按地址排序,从而保证获取同一套锁的任何路径都会产生一致的锁定顺序。

例如,假设操作 FSaSb)对结构 S 的两个实例执行操作,每个实例具有类 L 的锁,并且在操作 F 中必须同时锁定两个锁。

如果实例 S0 在内存中的排序先于实例 S1,则锁的相对排序与其所属实例相同。我们可以将锁视为分别具有 L0L1 子类。

如果我们以不同的顺序执行操作,就会出现锁排序问题:

FS0S1)和 FS1S0

如果不进行干预,这些会产生反转的锁定序列:

L0L1L1L0

由于 F 可以同时访问这两个锁,因此可以按地址对锁进行排序,从而获得一致的锁定序列,无论参数的原始顺序如何。

现在,假设我们向序列中添加了另外两个锁定类:在操作 F 之前获得的类 A,以及在操作 F 之后获得的类 B。生成的锁定序列如下:

AL0L1B

请注意,这与上一部分中的嵌套锁类序列图类似。实际上在相同情况下,只有锁的顺序由地址提供,而不是外部顺序。这意味着,在这两种情况中都可以使用活跃线程列表中的同一记账法。

锁定类跟踪数据结构

本部分介绍了跟踪锁类的相关实现详情,以及用于检测潜在死锁的具体处理技术。

每个锁类在有向图中都有一个静态分配的节点,代表属于该类的所有锁。每个节点都具有以下数据结构:

无锁、无需等待的哈希集

每个锁定类节点都有一个哈希集,用于跟踪从锁定类到在其之前排序的锁类的边。

TODO:添加哈希集的实现详情。

无锁、无需等待的独立集合结构

每个锁定类节点都有一个父指针,用于跟踪在有向图中按周期连接的节点。这允许循环检测算法之前已报告周期,而无需完全重新遍历图表。

TODO:添加不相交集结构的实现细节。

线程本地锁定列表

每个线程都会维护其当前持有的锁的线程局部列表。

TODO:添加线程局部锁定列表的实现详情。

循环检测线程

每当向有向图添加新的边时,都会触发循环检测线程遍历图,以查找涉及两个以上锁的循环依赖关系。Tarjan 的强连接集算法是一种高效的选择,最糟糕的情况是复杂性为 O(|E| + |V|)。即使在遍历由其他线程并发更新的图时,此算法也保持稳定。

TODO:添加循环检测线程的实现细节。

参考编号

  1. Clang 静态线程安全分析
  2. LLVM 运行时线程排错程序
  3. Linux 内核 lockdep 子系统