不变性是一种更好的调试器?


来自Marc's Blog的文章:不变性是推理算法数据结构和分布式系统的强大工具。对于您设计或实现的任何复杂系统或算法,都值得考虑一组不变性。以这样的方式构建您的实现也是值得的,即使是全局不变性也可以轻松地以确定性和可重复的方式进行测试。

示例:系统设计
在使用 AWS Lambda 的容器加载系统时,我们需要确保在垃圾收集期间不会丢失块。这种高并发的大规模分布式系统可能非常难以推理,因此我们需要从一组不变量开始思考。正如我们在论文中所说:

过去的分布式垃圾回收经验告诉我们,这个问题既复杂(因为块引用树是动态变化的),又有独特的风险(因为这是我们系统中删除客户数据的唯一地方)。

尽管如此复杂,系统不变式却相对简单:

  • 所有新的数据块都被写入处于活动状态的根中。
  • 所有读取的数据块都在活动状态或已停用状态的根下。
  • 根以单调的方式在激活、退役、过期和删除状态中移动。它们永远不会在这个状态链中向后移动。
  • 只有被过期根引用的数据块才能被删除。
  • 只有当根的所有块都被删除后,根才能移动到已删除状态。

只要系统保留了这些不变式,即使面对任意的并发和规模,也不会丢失任何数据。这几个不变式比完整的系统实现更容易推理,把它们写下来后,我们就能提出一个清晰的形式论证,说明为什么这些不变式是足够的。

示例:分层导航HNSW
Hierarchical Navigable Small World Graphs(层次可导航小世界图)是一种流行的数据结构,用于在大量高维向量集上执行近似 K 最近邻搜索。HNSW 的核心概念并不难,但推理起来却比我们日常接触的大多数算法都要困难。向量的大尺寸、大数据和图连接的复杂性使得在调试器中对 HNSW 进行推理非常困难。

但是,通过对不变式的思考,我们可以发现许多实现上的错误。插入新元素后,数据结构中哪些事情必须为真?向下传递到搜索每一层的入口点集合必须符合哪些条件?

例如

  • 入口点必须出现在最高层。
  • 每一层都是上一层的子集2。节点不会随着层数的增加而消失。
  • 每个节点都可以从入口点的最高处进入。
  • 所有节点都出现在第 0 层。
  • 每一层大约比上一层大 e 倍。

其中一些不变式的测试成本相当高,比如最后一个需要 O(N log N) 的工作量。在生产实现中的每一步都断言这些不变式并不总是切实可行的,但在单元测试中测试这些不变式却非常实用。我的经验是,推理、列出并测试这样的不变量,是比通过接口测试更好的测试方法。

实例:Paxos
Paxos 是出了名的难以推理。我不会假装自己觉得它很容易,但我相信人们之所以费尽心思,是因为他们没有足够重视《Paxos 简明教程》的第 2.2 节。在这一节中,Lamport 逐步阐述了实现共识的一系列不变式。首先是一些不正确的变量:

P1.接受者必须接受它收到的第一个提议。

在确定正确的不变式之前,需要分层请求。值得注意的是,在这一发展过程中,不变式从可以在单个节点上轻松断言的东西,转变为整个系统的更大属性,而这种属性只能由某个无所不知的更高权力机构来真正断言。

在实际系统中,甚至在集成测试中,都很难实现这种全知全能。在像 TLA+ 的 TLC 这样的模型检查器中,这是很微不足道的,但这对真正的实现并没有多大帮助。全知断言全局不变式是确定性模拟测试(如动荡)所赋予的最强大能力之一。在模拟器中,你可以停止时间,检查不变式,然后确定性地向前滴答。这里的 "你 "指的是测试。与调试器不同,测试可以轻松实现自动化和重复性。它们还能检查人类永远无法在头脑中保持正确的东西。

比如 Paxos 的关键不变式:

P2c 。对于任意 v 和 n,如果发布了一个值为 v 且编号为 n 的提案,那么存在一个由大多数接受者组成的集合 S,该集合 S 要么 (a) S 中没有接受者接受过编号小于 n 的提案,要么 (b) v 是 S 中接受者接受的所有编号小于 n 的提案中编号最高的提案的值。

Multipaxos、Raft 以及几乎所有其他分布式协议都有类似的不变式。在我看来,对它们进行推理并自动测试是一种未得到充分重视的超级能力。

总结
事实证明,在编写密集的算法代码、捕获业务逻辑以及实现分布式系统时,它非常有用。这也是十年前TLA+强烈吸引我的原因之一。TLA+思考正确性的方式都是基于全局不变量。