TLA+（形式化规范语言） 最适合在分布式系统的设计环节使用，因为它可以帮助工程师让设计、沟通及验证的过程变得有理可据。

在我们的案例中，原系统的设计和实现早已完成，但 TLA+ 依然显示其高超的价值。当我加入 Splunk 从事 Apache BookKeeper 的工作时，我对 BookKeeper 本身的使用经验很少。早在 2018 年，我就基于一系列混沌测试实验以及与 Pulsar 开发者就工作原理的讨论写了关于 Apache Pulsar/BookKeeper 的系列博客文章，因此我对其上层有不错的理解。然而，鉴于我的前几个项目都与提高 BookKeeper 的数据完整性有关，我觉得我应该在设计和修改代码前了解所有的细节和项目的底层。据我所知，了解一个新分布式系统最好的方式就是将其逆向工程为 TLA+ 规范。

TLA+ 与逆向工程

BookKeeper 复制协议文档对上层有很好的描述，但没有包含规范的细节，唯一的方法是直接阅读源码。就我个人而言，整个读源码、写 TLA+、重读源码然后写/编辑 TLA+ 的过程大概用了两周时间，然后用一周时间优化。其中，60% 的时间用在了读源码以理解协议上，另外 40% 则花在了写 TLA+ 及其测试上。

在编写过程中，不变量在定位协议规范中的 bug 时非常有用。只要是误解或完全略过一小段实现规范的代码片段，就会导致规范出错，进而违反不变量。我时常会遇到数据丢失的情况，因为那时我还没有完全理解代码的含义以及代码做了哪些检查与决策。在这过程中，我理解了协议的所有细微差别，甚至还有一些意外发现。

可以说，我深信将代码通过逆向工程转化为正式规范是很好的学习过程。

规范

我们使用规范对单个 ledger 从创建到关闭的生命周期进行了建模。对单个规范做任何改动都会导致问题。即便是单个 ledger，对其生命周期建模仍然相当复杂，状态空间也很大。一旦我们确定单个 ledger 生命周期的正确性，就可以基于这种假定，在其上层编写其他的规范来对 ledger 的链路进行建模。

在之前的博客中，我们讨论了 BookKeeper 的客户端如何进行读写。在 TLA+ 中，我们只会让客户端写入，不妨就在规范中称其为 writer。

变量与常量

元数据：

• 版本号
• 状态，包括打开（OPEN）、恢复中（IN_RECOVERY）以及关闭（CLOSED）
• Ledger Fragment，其中每个 Fragment 都由第一个 entry id 以及 bookie ensemble 组成。
• LastEntryId

Bookie：一个包含了每个 bookie 状态的 map，其值包括：

• 存储的 entry
• Ledger 的受保护（fenced）状态
• 最后添加确认（Last Add Confirmed，即 LAC）

Writer：

• Ledger 元数据版本
• 最后添加确认（LAC）与最后添加推送（Last Add Pushed，即 LAP）
• 运行中的新增操作
• 已知受保护（fenced）的 bookie
• 恢复阶段与响应

执行器与响应

在我们的规范中，仅有两类执行器（也称之为处理器）：bookie 与 writer。

在规范的模型中只有两个 writer（w1 和 w2），其中一个是 ledger 的所有者，另一个则可以在任何时候尝试恢复及关闭 ledger。规范同样规定了一个或多个 bookie，记为 b1 到 bN。

该规范使用消息传递来模拟 writer 与 bookie 之间的通信。每条消息有三种流向：

• Writer 向 bookie 发送一条消息。发送的消息可能会丢失。
• 消息被 bookie 处理并返回响应给 writer，但响应可能会丢失。
• Writer 收到并且处理了响应。

在以下消息传递示例中，writer 发送一条 entry 到 bookie 并且收到来自 bookie 的 ack。

writer 交互过程

图 1. Writer 1 与 bookie 和 ZooKeeper 的交互过程

图 2. Writer 2 的交互过程

完整的规范大约有 1000 行，下面我们只给出与上图交互有关的 Next 表达式。其中 \/ 字符表示或逻辑，因此每一步只有一条路径被选中。

Next ==
\* Bookies
\/ BookieSendsAddConfirmedResponse
\/ BookieSendsAddFencedResponse
\/ BookieSendsFencingReadLacResponse
\/ BookieSendsReadResponse
\* W1
\/ W1CreatesLedger
\/ W1SendsAddEntryRequests
\/ W1ReceivesAddConfirmedResponse
\/ W1ReceivesAddFencedResponse
\/ W1ChangesEnsemble
\/ W1TriesInvalidEnsembleChange
\/ W1SendsPendingAddOp
\/ W1CloseLedgerSuccess
\/ W1CloseLedgerFail
\* W2
\/ W2PlaceInRecovery
\/ W2ReceivesFencingReadLacResponse
\/ W2SendsReadRequests
\/ W2ReceivesNonFinalRead
\/ W2CompletesReadSuccessfully
\/ W2CompletesReadWithNoSuchEntry
\/ W2WritesBackEntry
\/ W2ReceivesAddConfirmedResponse
\/ W2ChangesEnsemble
\/ W2TriesInvalidEnsembleChange
\/ W2SendsPendingAddOp
\/ W2ClosesLedger

这 25 种交互行为为 BookKeeper 复制协议的核心操作建立了模型。可见这些操作类型十分多样，同时规范的状态空间也十分广泛。

不变量

本规范包含以下几种不变量。

No Divergence Between Writer And MetaData

NoDivergenceBetweenWriterAndMetaData指的是每次确认的写操作的 entry id（由 writer 1 确认）不能大于 ledger 关闭时的 Last Entry id。如果违反这一不变量，则意味着发生了丢数据的情况，并且可能在第二个 writer 进行接收和关闭操作时暴露出问题。

下面就是违反了上述不变量的例子。

图 3. 通过 ledger 元数据对其截断而造成数据丢失的情况

No Out of Order Entries

NoOutOfOrderEntries 表明 ledger 上的 entry 都是 ledger ensemble 按照时间顺序逻辑存储的。

All Committed Entries Reach Ack Quorum

AllCommittedEntriesReachAckQuorum 表明所有已确认过的 entry 的副本数量均达到最小复制因子，只要 bookie 没有永久性丢失数据，将持续满足最小复制因子的要求。当 writer 向其客户端返回确认写入信息时，若没有达到 entry 的 Ack Quorum 副本数，则会违反该不变量。

Only Valid Fragments

OnlyValidFragments 表明不能存在前一个创建的 Fragment 其 first entry id 大于后一个 Fragment first entry id 的情况。如果 writer 在执行恢复操作时，创建了一个新的 Fragment，而其 first entry id 比已有的 Fragment 小，则会违反不变量。实际上，当此类情况出现时会进行检测以防止违反该不变量，此操作会根据规范记录下来，不会真的发生。否则就破坏了不变量。

违规诊断

模型检查器会同时检测 NoDivergenceBetweenWriterAndMetaData 以及 OnlyValidFragments 这两种不变量，并持续报告违规事件序列。

分析分布式系统的交互过程并非易事。下一节我们将把重心放到违反 NoDivergenceBetweenWriterAndMetaData 这一不变量上。

Writer-Metadata 分歧缺陷

我们在本系列上一篇文章详细讨论了 BookKeeper 复制协议，其中谈到了 leader fail-over 时 ledger fencing 的机制。Fencing 操作防止旧的 owner 执行写入操作以达到 Ack Quorum。这意味着可以同时存在两个 writer，均认为自身为 ledger 的 owner，但是只有一个能成功写入。

然而 TLA+ 规范表明上述 fencing 机制还不足以防止旧的 writer 提交后续的 entry。这说明，在一定的事件序列下，旧的 Bookie owner 可以在新 owner 达到最小 fenced bookie 数量时偷偷写入数据（当单个 fence 请求丢失或顺序重排时会发生这种情况）。

图 4. Writer 1 在 ledger 已关闭时，设法写入 bookie b1 以达到 Ack Quorum，最终 Entry 1000 丢失。

Writer 2 收到了足够的 NoSuchEntry 响应，认为 Entry 1000 没有成功提交，便能够在 Entry 999 时关闭 ledger。

这样就导致一个问题，在“足够”数量的 bookie 进入 fenced 状态后，writer 1 仍然有可能达到 Ack Quorum。更深入的分析请参考 GitHub 的相关 issue[1]。

分析分布式系统并非易事

不难理解为什么人们没法检测到这个问题。最初的想法看起来显而易见。

图 5. writer 对 ledger 进行 fence 以防止另一个 writer 写入（此例中 writer 为 Pulsar broker）

然而，用形式化模型就可以发现这个简单的机制是有缺陷的。一旦发现，那么解决方案就好说了。

修复方式也很简单：在 bookie 恢复期间，一旦某个 bookie 响应过恢复读取请求，就让它一直响应下去，其后无法变更。同理，一旦某个 bookie 告诉执行恢复的 writer 说它没有某个 entry，那么它在后面就不能再添加该 entry。我们可以通过让恢复读取也执行 fencing 操作来实现这点。这意味着一旦某次恢复读取表示 entry 或者 ledger 不存在，那么后续返回也始终如此。我们用这一新的逻辑更新了规范，然后违规就不再触发了。这次修复已被合并到了 master 分支，不久便会发布（译者注：本文写于 2021 年 6 月，该 PR 已在 2021 年 3 月得到合并）。

总结

分布式系统通常十分复杂，人们往往很难理清各种并发处理的交互过程。好在有形式化的方法为我们提供了有力的工具，借以弄清原理，以及检测难以发现的错误，而有些错误就算用很先进的测试手段也难以发现。

TLA+ 非常适合工程团队，因为它可能是最简单的规范语言，它能让一般的没有很强数理技巧的工程师变得高效。只要 2 到 3 周，大多数工程师就能熟练使用 TLA+ 并在实际系统中写一些规范了。

本文翻译自《Modelling and verifying the BookKeeper protocol (TLA+ Series Part 3)》，作者 Jack Vanlightly，Apache BookKeeper Committer。校对与整理：StreamNative
译者简介
李文奇，就职于微软 STCA，业余时间喜欢研究各类中间件技术及分布式系统。