分布式系统中的全局谓词检测

# 分布式系统中的全局谓词检测 ## 1. 全局谓词检测基础 ### 1.1 检测流程 在预定义的生成树上，根节点（协调器）在树广播的扇出扫描中发送查询消息。在随后的树汇聚广播的扇入扫描中，每个节点收集以自身为根的子树中节点的本地状态，并将这些本地状态转发给其父节点。当根节点从其树中的所有节点获取到本地状态时，第一阶段完成。接着启动包含另一次广播和汇聚广播的第二阶段。 ### 1.2 不稳定谓词 不稳定谓词是指那些并非稳定的谓词，因此可能只是间歇性地成立。检测不稳定谓词存在以下挑战： - 由于消息传播时间的不可预测性，以及在不同负载条件下处理器上各进程调度的不可预测性，即使是确定性执行，同一分布式程序的多次执行也可能经过不同的全局状态。此外，该谓词在某些执行中可能为真，而在其他执行中可能为假。 - 由于分布式系统中不存在瞬时时间： - 即使监视器发现谓词在某个全局状态中为真，它在实际执行中可能并未成立。 - 即使谓词在某个瞬态期间为真，也可能无法通过间歇性监控检测到。 因此，对执行进行定期监控是不够的。为应对这些挑战，有两个重要的观察结果： - 似乎有必要检查执行中出现的所有状态，以免错过谓词为真的情况。因此，在整个执行的观察上定义谓词，而不是在单个状态上定义，似乎更有用。 - 对于同一分布式程序，即使它是确定性的，多次观察也可能经过不同的全局状态。此外，谓词在某些程序观察中可能为真，但在其他观察中可能为假。因此，在分布式程序的所有观察上定义谓词，而不仅仅是在其单个观察上定义，更为有用。 ## 2. 谓词的模态 为解决上述复杂性问题，谓词不是在全局状态或执行的单个观察上定义，而是在分布式执行的所有可能观察上定义。对于任何谓词 $\varphi$，定义了以下两种模态： - **Possibly($\varphi$)**：存在执行的一致观察，使得谓词 $\varphi$ 在该观察的某个全局状态中成立。 - **Definitely($\varphi$)**：对于执行的每个一致观察，都存在其某个全局状态，使得谓词 $\varphi$ 在该状态中成立。 ### 2.1 示例分析 考虑一个在进程 $P_1$ 和 $P_2$ 上运行的执行示例。事件 $e_k^i$ 表示进程 $P_i$ 上的第 $k$ 个事件。变量 $a$ 是 $P_1$ 的局部变量，变量 $b$ 是 $P_2$ 的局部变量。执行的状态格如图所示，每个状态由元组 $(c_1, c_2)$ 标记，其中 $c_1$ 和 $c_2$ 分别是 $P_1$ 和 $P_2$ 上的事件计数。 - **Definitely($a + b = 10$)**：当 $b$ 在事件 $e_1^2$ 被赋值为 7 时，进程 $P_1$ 的执行可能处于从初始状态到事件 $e_3^1$ 之前的任何状态，此时 $a = 3$。然而，在事件 $e_4^2$ 中 $b$ 的值从 7 变为 5 之前，实际上在 $P_2$ 执行事件 $e_3^2$ 之前，$P_1$ 必须已经执行了事件 $e_1^1$，此时 $a = 3$。这对于所有等效执行都是成立的。因此，Definitely($a + b = 10$) 成立。从状态格中可以看出，在每个执行中，状态 $(2, 2)$ 必然会出现，并且在该状态下，$a + b = 10$。 - **Possibly($a + b = 5$)**：谓词 $a + b = 5$ 只有在以下情况下才可能为真： - $a = 3 \land b = 2$，在状态 $(2, 5)$ 和 $(3, 5)$ 中为真。 - $a = 0 \land b = 5$，在状态 $(6, 4)$ 中为真。 - $a = 8 \land b = -3$，在状态 $(5, 7)$ 中为真。 状态 (i) 在物理时间上可能在事件 $e_5^2$ 发生之后且在事件 $e_4^1$ 发生之前出现。在所示的执行中，$e_5^2$ 在 $e_4^1$ 之后发生。然而，在等效执行中，事件 $e_4^1$ 可能会延迟到事件 $e_5^2$ 之后发生，在这种情况下，$a$ 变为 8 后 $b$ 变为其他值。因此，该谓词在这种等效执行中为真。类似的论证也适用于 (ii) 和 (iii)。 - **Definitely($a + b = 5$)**：在所示的执行中为假，因为存在至少一条通过状态格的路径，使得在该路径上的任何状态下 $a + b = 5$ 都不为真。 ### 2.2 谓词检测的复杂性 从上述示例可以推测，谓词检测问题是复杂的。对于 $n$ 个进程，每个进程最多有 $m$ 个事件，我们需要检查多达 $m^n$ 个指数级数量的状态。全局谓词检测问题可以通过从可满足性问题进行标准归约，很容易地证明是 NP 完全问题。 ## 3. 关系谓词的集中式算法 ### 3.1 假设与前提 为了检测谓词，首先假设状态格是可用的。全局状态 $GS = [s_{k_1}^1, s_{k_2}^2, \cdots, s_{k_n}^n]$ 缩写为 $GS_{k_1,k_2,\cdots,k_n}$。 ### 3.2 检测算法 #### 3.2.1 Possibly($\varphi$) 为了检测 Possibly($\varphi$)，需要对状态格进行详尽搜索，以找到任何一个满足 $\varphi$ 的状态。一旦找到这样的状态，搜索就可以终止。通常，人们特别关注找到满足 $\varphi$ 的“最早”状态。全局状态 $[s_{k_i}^i](\forall i)$ 的级别是 $\sum_{i = 1}^{n} k_i$。算法按级别逐个检查状态格，从级别 0 的初始状态开始，直到最终状态。检查每个级别，以找到 $\varphi$ 为真的状态。如果找到这样的状态，算法终止。 ```plaintext (variables) set of global states Reach_φ, Reach_Next_φ ← {GS_{0,0,\cdots,0}} int lvl ← 0 (1) Possibly(φ): (1a) while (no state in Reach_φ satisfies φ) do (1b) if (Reach_φ = {final state}) then return false; (1c) lvl ← lvl + 1; (1d) Reach_φ ← {states at level lvl}; (1e) return true. ``` #### 3.2.2 Definitely($\varphi$) 为了使 Definitely($\varphi$) 为真，应该存在一组满足 $\varphi$ 的状态，使得通过状态格的每条路径都经过这些状态中的一个。在状态格的任何特定级别上，所有状态都满足 $\varphi$ 是充分但非必要的条件。考虑图中的执行示例，Definitely($\varphi$) 为真，但满足 $\varphi$ 的状态处于不同的级别。 ```plaintext (2) Definitely(φ): (2a) remove from Reach_φ those states that satisfy φ (2b) lvl ← lvl + 1; (2c) while (Reach_φ ≠ ∅) do (2d) Reach_Next_φ ← {states of level lvl reachable from a state in Reach_φ}; (2e) remove from Reach_Next_φ all the states satisfying φ; (2f) if Reach_Next_φ = ```