Skip to content

全局快照与虚拟时间 ​

标签
分布式/时钟
字数
4533 字
阅读时间
18 分钟

Lamport 逻辑时钟 把偏序的事件集映射到线性有序的整数上,得到 C(a) < C(b) 这个必要不充分条件。Mattern 在 1988 年的 Virtual Time and Global States of Distributed Systems 里指出,这个映射本身有代价:它把本来无法比较的并发事件强行排出了先后。该文的说法是把偏序事件映射到线性有序整数集会丢信息,因为可能同时发生的事件被赋成了不同时间戳,看上去像有确定顺序。

对互斥这类只需要"不冲突"的问题,这个损失无所谓;对分布式调试这类要还原"谁和谁真并发"的场景,损失是致命的。所以那篇的出发点是不要线性时间,而要一个保留偏序的时钟结构,并在这个结构上重新定义"全局状态"—— 后半部分给的正是一套在不要求 FIFO 通道的前提下算一致全局快照的算法。

事件结构与因果关系 ​

形式化的起点是一个事件结构 (E,<):E 是事件集合,< 是 E 上的非自反偏序,称为因果关系。它是满足下面三条的最小关系:

  1. e 与 e′ 是同一进程上的事件,且 e 在 e′ 之前发生;
  2. e 是一条消息的发送事件,e′ 是它对应的接收事件;
  3. 存在 e″ 使 e<e″ 且 e″<e′(传递闭包)。

同一份事件结构可以画成两种同构的图:时空图(横轴表示真实时间,隐含了一个全局时钟)与偏序图(把 e′<e 画成 e 在 e′ 上方)。同构意味着图里那些"时间"信息是画出来的,不是结构自带的 —— 这是后面所有推理的立足点。

同一份事件结构的两种画法:

   时空图(横轴是真实时间)               偏序图(只画因果箭头)
      P1   ●1 ──── ●2                          ●2
           │        ╲                            ▲
           │         ╲ 消息                     │ 消息
           │          ▼                         │
      P2   ●1 ──── ●2 ──── ●3                   ●1 ──▶ ●3

   ⇒ 两张图同构。时空图里那些「时间」信息是画出来的,不是事件结构自带的。

先问:时间到底需要哪些性质 ​

Mattern 没有直接说"用向量代替整数",而是先列出"标准时间"作为偏序要满足的公理(设 < 是"早于"):

#公理含义
1非自反性没有瞬间早于自己
2非对称性w<x 蕴含 ¬(x<w)
3传递性w<x 且 x<y 蕴含 w<y
4线性任意两个瞬间可比
5稠密性w<x 时存在 y 使 w<y<x

关键观察是第 5 条可以换掉。 满足这五条的有多个互不同构的模型(有理数与实数),但实际用时钟时并不需要全部性质 —— 数字时钟显然不满足稠密性,却照样有用。把稠密性(5)换成离散性:

(5′) 离散性:每个瞬间都有直接后继

标准模型就变成整数 Z。这一步说明了"用硬件计数器或程序里的整型变量实现时钟"为什么是合法的。在大规模仿真等场景里公理 4 和 5 其实也没被完美满足(时钟变量会溢出;舍入误差会让不该同时的事件同时发生)—— 这类偏差是可以接受的。

由此得出这一节要回答的问题:能不能在不使用真实时间、物理时钟的前提下,构造一套逻辑时钟与同步机制,让它满足公理 (1)–(5)(或 (5′)),并用它给事件打时间戳使因果结构保持同构?

时钟向量形成格 ​

Mattern 给出的构造是给每个进程一个向量 Ci。Ci[j] 表示进程 i 目前知道的、进程 j 上已经发生的事件数。两个向量按逐分量的偏序比较:

Ci≤Cj⟺∀k:Ci[k]≤Cj[k]

两个向量的分量可能互有大小(Ci[k1]<Cj[k1] 而 Ci[k2]>Cj[k2]),这时两个事件并发 —— 这正是标量时钟丢掉的那部分信息。

在这些向量上定义逐分量的 max 与 min:

(a⊔b)[k]=max(a[k],b[k]),(a⊓b)[k]=min(a[k],b[k])

得到的结构是一个格(lattice)。向量时钟里 join 就是接收事件做的事(Vector 向量时钟 写作 Tjk=max(Tjk,MTk)),所以"格"这个结构不是额外发明的,它原本就在向量时钟的更新规则里。Mattern 的贡献是把这层代数结构挑明:时钟向量与因果关系同构,时间戳之间的偏序一一对应事件之间的因果关系。

这个构造与 Minkowski 相对论时空有直接类比:相对论里两个事件的先后只在类时间隔下无歧义,类空间隔下取决于观察者;分布式系统里的"并发事件"正对应类空间隔。这个类比说明线性时间是标准模型的一个特例,而不是唯一选择。

割:定义、格结构、与「可能发生过」 ​

要把"全局状态"说清楚,先得定义"系统的某一瞬间"。

定义 2(割的先后):割 C1 晚于(later than)割 C2 当且仅当 C2⊂C1。

注意这个"晚于"是自反的(一个割晚于它自己),所以它是割集合上的偏序。

定理 1:在集合运算 ∪ 与 ∩ 下,偏序事件集 E 的所有割构成一个格。

证明是直接的:格的定义是"任意两个元素都有最大下界与最小上界"。取上下确界即可 —— inf=C1∩C2,sup=C1∪C2。若不做任何限制,一个割可能含某条消息的接收事件却不含它的发送事件。这种割无法用来算全局状态(后面的快照算法要用它),所以要加一条左闭性:

定义 3(一致割):事件集 E 的一致割 C 是满足下式的有限子集

e∈C ∧ e′<e ⇒ e′∈C

一致割的等价说法是:每条被接收的消息,其发送事件也在割内(反过来不要求)。

定理 2:一致割的集合是全体割集合的子格。

证明是"验证一致割对 ∪ 与 ∩ 封闭",留给读者。格的实用含义是:任意两个一致割都存在更晚的与更早的一致割。这个结论可以推广到有限个:sup(C1,…,Ck)=C1∪⋯∪Ck 比它们每一个都晚。

橡皮筋检验 ​

一个几何判据:把割线想象成一条橡皮筋。若一条消息的箭头从右向左穿过它,割就不一致;否则一致。原因是出现这种穿越时会形成一条因果链 c3<e′<e<c1,从而 c3<c1,违反下面这条:

定理 3:一致割由割事件 c1,…,cn 组成时,任意一对割事件之间没有因果关系,即对任意 ch、ci 有 ¬(ch<ci)∧¬(ci<ch)。

这条定理就是上面的检验在形式上的对应物:一旦出现从右向左穿越割线的消息,割事件之间就产生了因果对,割必然不一致。

只看消息箭头穿过割线的方向:

     一致的割:箭头都从左往右穿           不一致的割:有箭头从右往左穿
        ──────╲────── 割线                 ──────╱────── 割线
               ╲                                  ╱
                ▼ 接收事件                       ▼ 接收事件
       (发送在割线左侧,                  (接收在割线左侧,
         接收在割线右侧)                    发送在割线右侧)

   形式化的对应物:从右往左穿时,割事件之间出现因果链 $c_3 < e' < e < c_1$,
   于是 $c_3 < c_1$ —— 违反定理 3(一致割的割事件之间没有因果关系)。

为什么沿一致割算出的全局状态是「正确的」 ​

定理 4:对任意有 n 个进程的时空图,总存在一个等价的时空图,在其中割线是一条竖直直线。

也就是说,一致割的所有割事件可以在真实时间里确实同时发生。这一步把"可能发生过"落到了实处:

  • 在所有进程的本地状态上、于同一真实时刻取快照,必然是一致的;
  • 所以沿一致割算出的全局状态是"正确的"。

全局状态的完整构成是两块:

  1. 各进程在割事件处的本地状态;
  2. 已发送但尚未被接收的消息集合 —— 在时空图上就是从左向右穿过割线的那些箭头。

快照算法:不要求 FIFO 的版本 ​

一套"重新发明"的 Chandy-Lamport 变体,用时间向量作为工具,并解决消息可能不按发送顺序被接收的问题。

现实世界里的快照(比如人口普查)很简单:所有"进程"约定一个未来时刻 τ,各自在 τ 取本地快照,之后收集起来拼成全局快照。搬到没有公共时钟的分布式系统上,难点是如何让所有进程就一个未来的虚拟时刻达成一致。这里先要一条定理:

在定理 12 之前先把用到的定理 5 补出来(定理编号沿用 Mattern 的编号):

定理 5:在任意真实时刻,对任意 i 与 j 都有 Ci[i]≥Cj[i] —— 进程 i 自己那一维的取值,是任何别的进程对「i 上已发生多少事件」的估计的上界。

定理 12:在 Ph 自己的分量发生 tick 的那一刻,不存在 i 使 Bh<Bi。

证明思路:用定理 5,并注意消息传输时间被假定为非零。它的实际含义是 —— 任何时刻请求快照都"不算晚",因为别的进程的时钟不可能超过 Ph 自己的分量。

五步 ​

设 Ph 是唯一的发起者:

  1. Ph tick 一次,然后把"下一次"时刻固定为r=Bh+(0,…,0,1,0,…,0)其中那个 1 在第 h 位。这就是约定的公共快照时刻。
  2. Ph 把 r 广播给所有其他进程。
  3. Ph 不再执行任何事件,直到它确知所有进程都已经知道 r(例如通过收到确认)。
  4. Ph 再 tick 一次(把自己的分量置为 r),取本地快照,并向所有进程广播一条哑消息 —— 这条哑消息迫使所有进程把时钟推进到 ≥r。
  5. 每个进程在自己的本地时钟等于 r,或者从小于 r 跳到大于 r 时取本地快照,并把快照发给 Ph。

第 3 步的代价是 Ph 在这段时间里被"冻结",绕过办法是:虚构第 m+1 个虚拟进程,它的时钟由 Ph 管理。Ph 就可以照常用自己的时钟、行为与其他进程一样。两个进一步简化:既然虚拟时钟 Bm+1 只在 Ph 发起新一轮快照时才 tick,那么前 m 个分量就没用了、可以省掉;而且第一轮广播也没必要 —— 各进程已经知道下一个快照时刻。

Ph 发起一轮快照的时序:

   P_h   ── tick ──▶ 定下公共时刻 r ──▶ 广播 r
                                              │
                    ┌─────────────────────────┘
                    │ 冻结:从此不再执行任何事件,直到确知所有进程都知道 r(例如收到确认)
                    ▼
              ── tick(把自己的分量置为 r)── 取本地快照
              ── 广播一条哑消息:迫使别的进程把时钟推进到 ≥ r
                    │
   P_i   ◀──────────┘
         自己的时钟等于 r,或从小于 r 跳到大于 r ⇒ 取本地快照并把快照发给 P_h

   冻结的代价用「虚构第 m+1 个虚拟进程」绕开 —— 它的时钟由 P_h 管,
   于是 P_h 不必冻结自己;进一步,前 m 个分量与第一轮广播都可以省掉。

white/red 着色 ​

用整数计数器记快照轮次是浪费,模 2 的布尔状态指示器就够。两种状态记作 white(快照前)与 red(快照后),算法变成:

  • 每个进程初始为 white;
  • 进程第一次收到 red 消息时,自己变 red 并立刻取本地快照;
  • white 进程只发 white 消息,red 进程只发 red 消息;
  • 发起进程自发变红,然后通过虚拟广播(直接或间接发 red 哑消息,例如沿虚拟环,或者让变红的进程向所有邻居发)保证最终所有进程变红。

正确性证明(完整论证):算法诱导的割由所有 white 事件组成。要证它一致,只需证不存在"red 进程发出、white 进程接收"的消息 —— 因为这样一条消息会在被接收之前就把接收方染红,矛盾。所以该割是一致的。

算法在消息不按发送顺序被接收时仍然正确。

white / red 与在途消息:

   white ──white 消息──▶ white        快照前,无所谓
   white ──white 消息──▶ red          ← 这条就是「在途消息」:
                                         red 进程收到后,要把一份副本发给发起者
   red   ──red 消息────▶ red          快照后

   规则:进程第一次收到 red 消息 ⇒ 变红并立刻取本地快照;
        white 只发 white,red 只发 red。
   正确性:不存在「red 发出、white 接收」的消息 ——
          它会在被接收之前先把接收方染红,矛盾 ⇒ 这个割必然一致。

在途消息与终止判定 ​

全局状态还要包含在途消息。它们很好识别:white 但被 red 进程接收的那些消息。red 进程收到这种消息时,把一份副本发给发起者即可。

剩下的问题只有终止判定:发起者拿到所有在途消息的副本,却不知道哪一份是最后一份。 解法很巧:

  • 给每个进程配一个计数器,计数已发送消息数减已接收消息数(快照算法自己的消息不计入);
  • 这个计数器是本地状态的一部分,随快照一起收集上来;
  • 发起者把它们累加,就知道一共有多少条 white 消息在途 —— 也就知道应该收到多少份副本,从而判定结束。
  • 终止时所有进程都是 red、没有 white 消息在途,所以下一轮不需要重新初始化,把 white 与 red 的角色交换一下即可。

与 Lai-Yang 的对比,以及它可以当终止检测用 ​

对照 Lai 与 Yang 的不要求 FIFO 的快照算法:那个算法把已发送/已接收消息的完整历史捎带在每条消息上,发起者据此算差值、从而确定在途消息,不需要收副本。它的好处是"快",代价是空间开销大得多。Mattern 的方案用消息计数器换掉了历史。

最后一个副产品:这个快照算法可以直接当分布式终止检测算法用。若本地状态本身不关心,只留消息计数器 —— 累加结果为 0 就意味着没有消息穿过割线,于是系统已终止。

与向量时钟那篇的关系 ​

Vector 向量时钟 讲的是同一个数学对象在消息传递系统里的落地形态与冲突检测用途;这一篇补的是它背后的结构(格)与它延伸出的全局状态判定(一致割、快照、稳定性质)。

判据结论
Ca≤Cba 因果先于 b(或并发,取决于严格性)
Ca∥Cb(分量互有大小)并发,对副本就是冲突
割内不含任何 e′<e 的缺口一致割,是"可能发生过"的全局状态
有消息箭头从右向左穿过割线割不一致(橡皮筋检验)

相关 ​

参考 ​

  • Friedemann Mattern. Virtual Time and Global States of Distributed Systems. International Workshop on Parallel and Distributed Algorithms(Chateau de Bonas, France, October 1988),M. Cosnard et al. (ed.),Elsevier Science Publishers B.V. (North-Holland), 1989。

贡献者 ​

文件历史 ​