第三篇：时间和全局状态

Posted 2021-07-08 flying_1314

目录

全局状态

全局状态

定义

Cut:截断/切分

全局状态

走向和线性化

快照

Chandy-Lamport 快照算法

假设

算法

初始化快照

复杂度

一致性：定理

一致性：证明

快照算法的可到达性

可到达性：定理

 可到达性：证明

重要笔记

---

全局状态

目标

• 确定分布式系统中某个特定属性在执行时是否为真

如何做？

• 使用逻辑时间构建系统状态的全局视图

动机：

• 分布式的垃圾回收
  • 系统中是否存在对对象的引用？
    引用可能存在于本地进程、另一个进程或通信通道中。

• 分布式的死锁检测
  • 进程之间的“等待”关系图中是否存在循环？

• 分布式终止的检测
  • 分布式算法终止了吗？

• 分布式调试
  • 给定两个进程 p1 和 p2，分别带有变量 x1 和 x2，我们可以确定条件 |x1–x2| 是否成立 > δ 是真的吗？
  • 一个特别困难的问题
  • 清楚地表明需要观察全局状态（即：调试）

全局状态

我们可以从不同时间记录的局部状态组装一个全局状态吗？
记住：

• 分布式系统中物理时间无法完美同步
• 不可能在特定时间收集系统的全局状态

定义

• 进程 pi 的历史被定义为
  • 
• 历史的前缀定义为
  • 
• N 进程系统的全局历史 p0 到 pN–1
  • 
• 状态
  • 捕获通信通道中的消息：每个进程记录发送或接收消息作为其状态的一部分

Cut:截断/切分

系统执行的一部分

•  其全局历史的子集，它是进程历史前缀的联合.

切割的边界

• 每个进程的最后一个事件

一致的切割

• 对于所有事件 e 和 e’：e ∈ C 和 e’ → e ⇒ e’∈ C

切割的边界（红线）

左边的切割是不一致的

• 在 p2中 切割包括收到的 m1，但在 p1 它不包括该消息的发送
• 我们在切割中有事件的结果，而没有原因，分布式系统永远不会处于这种状态

全局状态

全局状态

• 单个进程的状态集：S = (s0, s1, ..., sN–1)
• pi 的状态 si 对应于切割前最后一个事件之后的 pi 状态

一致的全局状态

• 对应于一致切割的全局状态
• 切入边界中的事件之后的每个进程的本地状态（切入中由p处理的最后一个事件）

走向和线性化

分布式系统的执行可以看作是全局状态之间的一系列转换

• S0->S1->S2->...

每个转换对应一个进程中的一个事件

• 如果两个事件同时发生，它们必须是并发的，我们可以按任意顺序放置它们

走向

• 全局历史中所有事件的总排序与每个进程的本地历史排序一致（）

线性化（一致走向）

• 全局历史中事件的排序与之前发生的关系（➝）一致
• 只通过一致的全局状态

可达状态

• 如果存在通过这些状态的线性化，则状态 S' 可从另一个状态 S 到达

快照

分布式算法执行的快照

• 记录一致的全局状态

快照包括：

• 每个进程状态的本地快照
• 每个通道传输中消息的通道状态

快照的使用

• 失败后重新启动
• 稳定属性的离线确定，一旦它们成为真，例如死锁，垃圾对象，这些属性仍然为真
• 调试

这里需要注意的是：

分布式系统的执行通过一致的全局状态演变

• S0 → S1 → S2 …

每当事件发生时，全局状态都会发生变化

• 进程发送消息
• 进程接收消息
• 进程走一步

从（一致的全局）状态移动到（一致的全局）状态服从发生在之前的关系

举例快照：

• 两个进程：P1和P2
• 通道 C12 从 P1 到 P2
• 通道 C21 从 P2 到 P1

• P1 和 P2 的进程状态
• C12 和 C21` 的通道状态（即消息）
• 这是我们的初始全局状态
• 也是一个全局快照

• P1 告诉 P2 将其状态变量 X2 从 1 更改为 4
• 这是另一个全局快照

• P2收到来自P1的消息
• 另一个全局快照

• P2 将其变量 X2 从 1 更改为 4
• 另一个全局快照

Chandy-Lamport 快照算法

使用称为标记(Marker)的控制消息

标记Marker 分隔通道中的消息

• 在进程记录其状态后，它会在发送更多消息之前沿其所有传出通道发送一个标记。
• 标记将通道中的消息分为要包含在快照中的消息和不包含在快照中的消息
• 进程必须在不迟于在其任何传入通道上接收标记时记录其状态。

假设

通道和进程都不会失败

• 通讯可靠

通道是单向的，消息按顺序到达 (FIFO)
任意两个进程之间存在路径

•  强连接网络

任何进程都可以发起快照算法
快照发生时，进程可以继续工作
基本信息和控制信息

• 区分底层分布式算法的基本消息和快照算法的控制消息

算法

对于进程Pi标记Marker的接受规则

在 pi 通过通道 c 收到标记消息时：
    如果（pi 还没有记录它的状态）它
        现在记录它的进程状态；
        将 c 的状态记录为空集；
        打开通过其他传入通道到达的消息的记录；
        遵循标记发送规则
    否则
        pi 将 c 的状态记录为自 c 保存状态以来它通过 c 接收到的消息；

对于进程Pi标记Marker的发送规则

在 pi 记录其状态后，对于每个传出通道 c：
pi 通过 c 发送一条标记消息（在通过 c 发送 q进程 任何其他消息之前）

初始化快照

假设进程Pi发起快照

• pi 记录自己的状态
• pi 准备了一个特殊的标记消息（控制消息）
• pi 将标记消息发送到所有其他进程（使用 N-1 出去的消息通道）
• 开始记录来自所有传入通道的所有传入消息

终止快照

所有进程在所有 N-1 个传入通道上都收到了一个标记（并记录了它们的状态）

举例子：

P1 初始化一个快照

P1 记录它的状态

接下来，P1 向 P2 发送一条标记消息并开始记录入站通道上的所有消息
同时，P2向P1发送消息

 P2第一次收到一个marker消息，所以记录下它的状态
P2然后向P1发送一个标记消息

 P1 从 P2 接收标记消息，它已经记录了它的状态，因此它将它在入站通道上接收到的所有消息记录到相应通道的状态
两个进程都记录了它们的状态和所有传入通道的所有状态
快照以蓝色突出显示

 例子2

两个进程交换“小部件”(widgets)

• 进程 p1 通过 c2 向 p2 发送小部件订单，每个小部件 10 美元
• 后来，进程 p2 沿通道 c1 向 p1 发送小部件
• 进程具有如图所示的初始状态
• 进程 p2 已经收到了五个小部件的订单

 

 最后记录的快照是：P1 <1000, 0>, P2 <50, 1995>, c1 <five widgets>, c2 < >

重要的笔记：
请注意，快照不需要是实际状态，而是算法记录的一致状态。比如上面的图和最终的快照结果并不一样。

复杂度

设 e 是边的数量，d 是网络的直径

记录算法的单个实例需要 O(e) 消息和 O(d) 时间

一致性：定理

定理

• Chandy-Lamport 算法拍摄的快照对应于一致的全局状态

记住

• 一致的全局状态对应一致的cut
• 一致切割cut：如果 ei → ej 并且如果 ej 在cut中，那么 ei 也在cut中

我们需要证明算法拍摄的全局快照对应于一致的切割cut

• 如果 ei 发生在进程 pi 中，ej 发生在进程 pj 和 ei → ej 则，如果 ei 发生在 pi 记录其状态之前（即 ei 在切割cut中），那么 ej 也发生在 pj 记录其状态之前

一致性：证明

设 ei 和 ej 是 pi 和 pj 处的事件，让 ei → ej
我们需要证明：如果 ej 在切割cut中，那么 ei 也在切割cut中
pi = pj：显而易见
pi ≠ pj：反证法：

• 假设如果 ej 在切割cut中，则 ei 不在
• ei 不在切割cut中，所以 ei 发生在 pi 记录其状态之后
• 必须有一个有限的消息序列 m1, ..., mn 导致 ei → ej
• 在 m1, ..., mn 中的任何一个到达之前，标记必须到达 pj，并且 pj 必须在 ej 发生之前记录其状态，即 ej 不在切割cut中（矛盾！）

快照算法的可到达性

Sinit:

• 全局状态紧接在第一个进程记录了它的状态之前

Sfinal：

• 快照算法终止时的全局状态，（紧接在最后一个状态记录动作之后）

Ssnap:

• 记录的全局状态

接下来，我们将Sinit，Sfinal和Ssnap映射到我们之前的第二个例子中。

可到达性：定理

令 Sys = e0, e1, ... 是系统执行的线性化。 然后有一个序列Sys'= e'0, e'1, ... 的 Sys 使得

• Sinit、Ssnap 和 Sfinal 发生在 Sys’
• Ssnap 可从 Sys' 中的 Sinit 访问，Sfinal 可从 Sys' 中的 Ssnap 访问

 可到达性：证明

在 Sys 中拆分事件

• Pre-snap 快照前事件：在此事件发生的进程记录其状态之前发生
• Post-snap快照后事件：所有其他事件

排序事件以获取 Sys’

• 假设 ej 是一个进程中的 post-snap 事件，而 ej+1 是另一个进程中的 pre-snap
• ej → ej+1 是不可能的（否则标记消息会先于消息，使消息的接收成为 post-snap 事件，但我们假设 ej+1 是 pre-snap 事件）
• 因此，ej 和 ej+1 可以在 Sys' 中交换
• 如有必要和可能，交换相邻事件，直到在 Sys 中所有 pre-snap 事件先于所有 post-snap 事件 
• 由于我们既没有干扰 Sinit 也没有干扰 Sfinal 我们建立了这些状态之间的可达性关系

重要笔记

快照算法的可到达性：

• 用于检测稳定断言
• 如果稳定断言在状态 Ssnap 中为真，则在状态 Sfinal 中断言为真
• 原因：如果一个稳定的断言对于一个状态是真，那么它对于任何可从它到达的状态都将保持真
• 同样，如果我们快照的稳定断言是 FALSE，我们可以说它从一开始就是 FALSE

在垃圾收集、死锁检测和终止检测等问题中很有用。

以上就是本片内容，有点略长，时间和全局状态部分就暂告一段落了，辛苦大家观看，有问题欢迎随时评论交流哦。