Zircon 和 Fuchsia 中的运行时锁验证

简介

锁定验证是一种用于检查锁定行为一致性的技术 来找出潜在的死锁危险本文档讨论了 静态和动态方法锁定验证和 为 Google Cloud 控制台中提供的运行时锁定验证库奠定了基础， 锆石和紫红色。

背景

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

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

静态验证

静态验证通常在编译时通过分析调用 由编译器或其他源级处理器生成的图表。这个 因此有必要对代码进行插桩，并使用 注解，用于告知验证器哪些类型代表锁，哪些类型代表锁 规则是否应用于使用锁类型的代码。

静态验证的优势包括在构建时及早发现问题 确定性验证结果和零运行时开销。这个 属性组合使始终启用静态验证具有吸引力， 确保在代码进入 构建，而不会影响构建工件的性能。

静态验证也有一些缺点。其中一个问题是 验证时需要正确、一致地应用各种注释 锁定和代码以提供有用的结果。这可能会导致维护问题 问题，除非实施严格的代码审核标准。另一个问题是 静态验证的可视性有限，可能会被条件验证 跨路径、动态调度、移动语义和锁定依赖关系， 编译单元。

动态验证

动态验证可在运行时在线执行，具体方法是观察两者之间的关系 。通过这种方法， 足以只对锁定基元进行插桩处理并获取/释放 操作来提供验证所需的信息。

动态验证的优势包括更简单的检测（从 并且可能更清楚地了解实际运行时 程序行为。这使得动态验证在大型代码中非常有用 在这种情况下，静态验证可能无法查看完整的 一组可能的锁交互。

动态验证的主要缺点是运行时开销和执行情况 覆盖率要求由于动态验证必须跟踪锁定互动 在运行时，每次获取和释放都会产生非零的执行成本， 跟踪数据本身的内存开销。 运行时跟踪还会导致未执行的代码路径 无法由验证工具分析。这可能会增加 开发者和质量检查人员，以确保提供足够的执行覆盖率（如果尚未这样做） 项目要求。

锁定排序不变

锁验证器的作用是确定锁是否不可变 。主不变性是指两个或多个值之间的顺序， 锁：程序中所有获取两个或更多锁的路径都必须在 与涉及两个或多个相同锁的所有其他路径一致， 避免发生死锁的问题处理硬件的环境 中断（例如嵌入式系统和内核）具有额外的排序方式， 不变，以避免中断引起的死锁。这些不变量由 。

基本反转

最简单的反转形式是，一个程序有两个锁， 它们按顺序获取，并且在不同路径中顺序不一致。

例如，某个程序具有锁 A 和 B 以及代码路径 P1 和 P2，并且以下行为 出现死锁的可能性：

路径 P1 获取并释放序列中的锁：

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

路径 P2 按倒序获取和释放锁：

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

使用正确的交错，可能是因为两个路径同时执行 在不同线程上，当路径 P1 持有锁时会出现死锁 A 和等待锁定的区块B，而路径 P2 持有锁 B 和等待锁 A 的块。

循环依赖关系

两个以上的锁和路径之间也可能会发生反转。这种类型的 通过人工检查识别反转比人工检查的难度要大得多， 所涉及的一对锁可能在每个涉及 然而，就整体而言，可能仍存在潜在死锁 锁的顺序。

例如，某个程序具有锁 A、B 和 C；路径 P1、P2 和 P3；替换成 则可能会导致死锁：

路径 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、P2， 而 P3：当每条路径在 并在第二步等待锁。在实际使用中 由于存在许多不同的路径，这些路径会产生相同的 成对锁序列。

IRQ 安全排序

在处理硬件的系统中，会中断 irq-safe 和 非 Irq 安全锁至关重要：在调用请求触发时， 持有 irq 安全锁以防止间接锁反转。Irq 安全锁 保留 irq 和非 irq 上下文之间的排序；提供两个或两个 对于在 irq 和 非 Irq 上下文。对于非 irq 安全锁，情况并非如此。原因在于 非 irq 安全锁允许 irq 处理程序有效地插入锁 由处理程序在中断任务锁的任意点获取 序列。

例如，一个具有非 irq 安全锁 A 和 irq-safe 锁的系统 Birq；路径 P1、P2 和 irq 路径 Pirq;具有以下行为的线程有可能发生死锁：

CPU1 上的路径 P1 按顺序获取和释放锁：

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

CPU1 上的路径 Pirq 按顺序获取和释放锁：

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

CPU2 上的路径 P2 按顺序获取和释放锁：

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

通过路径 P1、P2 和 Pirq 当 Pirq 尝试获取 Birq，而 P2 包含 Birq 和块 等待 A。这是间接锁反转：Pirq 可在应用期间有效插入Birq的获取/释放序列， P1 路径中 A 的获取/释放序列的中间， 与路径中相同锁的锁序列不一致 P2。

执行验证

上一部分讨论的不变量可以使用 有向图。有向图会跟踪锁的身份和顺序， 会遍历代码路径。这种图可以通过遍历 由编译器或源级处理器（静态 或通过观察程序执行期间锁的顺序（动态 分析）。本部分以抽象术语介绍该流程，该过程适用于 为开发具体的动态分析做好准备 策略

一般来说，从代码路径构建有向图需要 在路径遍历时维护主动持有的锁的列表： 每当获取表示锁时，并向列表中添加该锁，并且 从列表中移除。除了维护 活跃列表，则向图添加一条有向边，该边表示 新获取的锁，指向表示列表中已有的锁的每个顶点。

基本反转示例

本部分介绍了检测基本双锁的有向图方法 反转。

回顾一下前面的示例包含锁 A 和 B 的程序；代码 路径 P1 和 P2；以及以下行为：

路径 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。

初始状态：

级别1 V 东
() {} {}

完成 P1 第 1 步后：

级别1 V 东
（A） {A} {}

此步骤将向活动列表添加锁 A，并为该对象引入一个顶点， 对有向图的锁。由于有效密钥中没有任何其他锁 列表中，没有添加边。

完成 P1 第 2 步后：

级别1 V 东
（A、B） {A, B} {(B, A)}

此步骤向活动列表添加锁 B，并引入 绘制一个顶点。这一次，活动列表包含锁 到现有锁的新锁将会添加到图表中。这条边缘 表示锁 B 现在依赖于在任何情况下的锁 A 前面的锁 ABB 另一个涉及两种锁的路径。

完成 P1 第 3 步后：

级别1 V 东
（A） {A, B} {(B, A)}

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

完成 P1 第 4 步后：

级别1 V 东
() {A, B} {(B, A)}

从活动列表中移除了锁 A。图表没有更新。

路径分析 P2

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

初始状态：

级别2 V 东
() {A, B} {(B, A)}

在本例中，初始状态是路径 P1 中的最终状态。

完成 P2 第 1 步后：

级别2 V 东
(B) {A, B} {(B, A)}

此步骤将为活动列表添加锁 B。由于此层中没有任何其他锁 活动列表中，不会向图表添加边。由于 BB 在 则图表中没有变化 V。

完成 P2 第 2 步后：

级别2 V 东
（B、A） {A, B} {(B, A), (A, B)}

此步骤将向有效列表添加锁 A。由于此锁已有 vertex，V 没有变化。不过，由于在 Active 列表，从新锁定到现有锁定的边缘会添加到 图表。利用这条新边，图表现在会在顶点 A 和顶点 A 之间形成循环 B，这表明这些锁之间的顺序不一致， 到目前为止考虑的两条路径，并且存在潜在死锁。

循环依赖关系示例

本部分介绍了检测圆形的有向图方法 使用前面讨论过的不变量中的示例来反转依赖项 部分。由于与 上图。

假设某个程序具有锁 A、B 和 C 以及路径 P1、P2 和 P3 及以下 行为：

路径 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。

初始状态：

级别1 V 东
() {} {}

完成 P1 第 1 步后：

级别1 V 东
（A） {A} {}

完成 P1 第 2 步后：

级别1 V 东
（A、B） {A, B} {(B, A)}

完成 P1 第 3 步后：

级别1 V 东
（A） {A, B} {(B, A)}

在完成 P1 第 4 步后：

级别1 V 东
() {A, B} {(B, A)}
路径分析 P2

让 L2 为路径持有的锁的有序活跃列表 P2。

初始状态：

级别2 V 东
() {A, B} {(B, A)}

完成 P2 第 1 步后：

级别2 V 东
(B) {A, B} {(B, A)}

完成 P2 第 2 步后：

级别2 V 东
（B、C） {A, B, C} {(B, A), (C, B)}

此步骤会向活跃列表添加锁 C，并引入 绘制一个顶点。活动列表包含锁 B，因此添加了边 从“C”到“B”。

完成 P2 第 3 步后：

级别2 V 东
(B) {A, B, C} {(B, A), (C, B)}

完成 P2 第 4 步后：

级别2 V 东
() {A, B, C} {(B, A), (C, B)}
路径分析 P3

让 L3 为路径持有的锁的有序活跃列表 P3。

初始状态：

级别3 V 东
() {A, B, C} {(B, A), (C, B)}

完成 P3 第 1 步后：

级别3 V 东
(C) {A, B, C} {(B, A), (C, B)}

完成 P3 第 2 步后：

级别3 V 东
（C、A） {A, B, C} {(B, A), (C, B), (A, C)}

此步骤将向有效列表添加锁 A。有效列表包含锁形图标 C，因此会从 A 到 C 添加边。有了这条新的边，图现在 在顶点（A、B、C）中形成循环，表示是圆形 依赖项，以及路径 P1 出现死锁的可能性， P2 和 P3 正确交错。

IRQ 安全排序示例

本部分介绍了检测 irq 安全顺序的有向图方法 使用前面讨论的“不变量”部分的示例来预测违规行为。

回顾一下具有非 irq 安全锁 A 和 irq-safe 锁的示例系统 Birq；路径 P1、P2 和 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。

初始状态：

级别1 V 东
() {} {}

完成 P1 第 1 步后：

级别1 V 东
（A） {A} {}

完成 P1 第 2 步后：

级别1 V 东
() {A} {}
路径 Pirq 分析

让 Lirq 作为路径所持有的锁的有序活动列表 Pirq。

初始状态：

Lirq V 东
() {A} {}

完成 Pirq 第 1 步后：

Lirq V 东
(Birq) {A、Birq} {}

完成 Pirq 第 2 步后：

Lirq V 东
() {A、Birq} {}
路径 Pirq 分析

让 L2 为路径持有的锁的有序活跃列表 P2。

初始状态：

级别2 V 东
() {A} {}

完成 P2 第 1 步后：

级别2 V 东
(Birq) {A、Birq} {}

完成 P2 第 2 步后：

级别2 V 东
（Birq、A） {A、Birq} {(A, Birq)}

此步骤将向有效列表添加锁 A。有效列表包含锁 Birq，因此将边缘从 A 添加到 Birq。 由于这是从非 irq 安全锁到 irq 安全锁的边缘，因此 irq-safe 锁 违反排序不变性，并可能出现死锁。

从理论到实现

本部分将介绍实现有向图的具体策略 验证工具。

实现策略具有以下目标：

  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 会在所有 Foo 和 Bar 的实例；无法将此顺序应用于其他 当 Foo 的相同实例时，程序的各个部分会导致死锁 和 Bar 以不同顺序同时锁定。

请注意，您可能有意或无意地将不同的 Foo 和 Bar 的集合，以便按不同顺序锁定实例 绝不能重叠不过，这仍然很危险，因为看似无害 对程序的输入、结构或时间的更改都有可能使 隔离并造成潜在死锁。此问题可以避免 完全以同等方式处理 Foo 和 Bar 的所有实例，并应用 相同的排序规则。

可通过跟踪 类中的锁而非锁实例：每种类型中的每个锁成员 表示唯一的锁定类。每个锁类之间的关系 跟踪和分析图表的 一把锁。

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

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

其他排序规则

跟踪锁定类在锁定时引入了其他排序注意事项 同一个类的多个锁。因为系统不会跟踪个别实例 如果有多个客户 ID，则需要采取额外措施来确保一致性。 必须同时获取同一类的锁。

外部订购的锁

当存在多个层级或其他元素时，有必要嵌套同一类的锁 有序数据结构在每个节点中都设置了锁，并且每个节点有多个锁 同时保持在这种情况下，数据结构或访问模式 必须提供稳定的排序，用于保证锁的排序。

验证可嵌套锁类仅需要外部顺序 会记录为每个可嵌套锁的有效锁列表中 将同一类的锁添加到列表中。这种设计的后果是 其他锁类不得穿插在 只能指定在一系列嵌套锁之前或之后。

例如，A 和 B 不可嵌套的锁类，以及可嵌套的锁类 N 可以这样穿插使用：

A、N0、N1... Nn、B

但请不要采用以下形式：

A、N0、B、N1 ... Nn 或 A、N0、N1、B ... Nn 或 等等

在大多数情况下，这是一个合理的约束条件， 使用任意深度的嵌套结构中可能会导致反转 因为结构在运行时更新。另一方面，在 嵌套限制在几个级别上，定义单独的 使用嵌套类，而不是使用嵌套类。 按照正常锁定顺序，在特定级别允许其他锁定 规则。

地址排序

很难在同一类的锁之间泛化锁排序 而不需要外部提供的顺序，而锁是在不同的 次。不过，您可以在获取 Pod 时 多个锁，而不需要时间分离。在这种情况下 可以按地址对锁进行排序， 从而确保获取 相同的一组锁定会产生一致的锁定顺序。

例如，假设运算 F(Sa, Sb) 对结构 S 的两个实例执行操作，每个实例都有一个类锁 L 和 F 必须锁定这两种锁定（作为操作的一部分）。

如果实例 S0 在内存中的排序顺序早于实例 S1，则锁具有与其相同的相对顺序， 实例。我们可以将锁视为具有子类 分别为 L0 和 L1。

如果我们使用不同的 ID 来执行操作， 订单：

F(S0、S1) 和 F（S1、S0）

如果不进行干预，这些过程会产生反转的锁定序列：

L0、L1 和 L1、L0

由于 F 可以同时访问这两个锁，因此 按地址对锁排序 从而实现锁的一致性 序列，而不考虑参数的原始顺序。

现在，假设我们为序列再添加两个锁类：获得的 A 类 在操作 F 之前以及在操作 F 之后获取 B 类。通过 为：

A、L0、L1、B

请注意，这与 上一节。事实上，情况是一样的 按地址而非外部订单提供。也就是说， 这两种情况都可以使用活动讨论帖列表中的簿记功能。

锁定类跟踪数据结构

本部分讨论跟踪锁类的实现详情，以及 具体处理技术来检测潜在死锁。

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

免锁定、无需等待的哈希集

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

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

无锁、无等待的不相交集合结构

每个锁类节点都有一个父指针，用于跟踪连接的节点 在有向图中以周期为单位。这样可以允许 而无需完全遍历图。

TODO：添加不相交集结构的实现详情。

线程本地锁定列表

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

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

循环检测线程

每当有向图添加新的边时，循环检测线程 被触发来遍历图表，找出涉及超过 两把锁。Tarjan 的强连接集算法是一种有效的选择， 最差情况的复杂度为 O(|E| + |V|)。此算法稳定 即使在遍历由其他线程并发更新的图时也是如此。

TODO：添加循环检测线程的实现详情。

参考文档

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