PDF分布式系统的验证
提高系统正确性信心的实践指南
Caitie McCaffrey
Leslie Lamport，以其在分布式系统方面的开创性工作而闻名，曾说过：“分布式系统是指，即使你不知道存在的计算机发生故障，也可能导致你自己的计算机无法使用。” 鉴于这种黯淡的前景和大量可能的故障，你究竟该如何开始验证和确认你构建的分布式系统正在做正确的事情呢？
分布式系统难以构建和测试主要有两个原因：部分故障和异步性。异步性是指系统内排序和定时的不确定性；本质上，不存在“现在”。10 部分故障是指组件可能在途中发生故障，导致结果或数据不完整。
必须解决分布式系统的这两个现实问题才能创建正确的系统。 解决这些问题通常会导致复杂度很高的解决方案。 这反过来又增加了在设计、实现或操作中出现人为错误的可能性。 此外，异步性和部分故障的相互作用导致了极其庞大的故障状态空间。 由于分布式系统的复杂性和故障状态空间的庞大，测试和验证这些系统至关重要。 如果不明确地强制系统发生故障，那么就无法合理地相信它在故障模式下能够正确运行。
形式化验证
形式化验证是一组证明系统属性的方法。 一旦使用了这些方法，系统就会因其可证明的正确性而获得“金星”。
形式化规范语言
可以使用形式化方法（例如 TLA+ 和 Coq16）来验证单个系统和协议。 这些是形式化规范语言，允许用户设计、建模、记录和验证并发系统的正确性。 每个被测系统都需要定义程序、包括可能发生的故障类型的环境以及定义系统提供的保证的正确性规范。 借助这些工具，可以将系统声明为可证明的正确。
AWS（亚马逊网络服务）成功地使用 TLA+ 验证了其十多个核心基础设施组件，包括 S3（简单存储服务）。8 这导致发现了系统设计中的几个微妙错误，并使 AWS 能够进行积极的性能优化，而无需担心破坏现有行为。
关于形式化规范语言的典型抱怨是学习它们很困难，并且编写规范既乏味又耗时。 确实，虽然它们可以揭示令人讨厌的错误，但学习曲线陡峭且时间投入巨大。
模型检查
另一种形式化方法——模型检查，也可以确定系统是否可证明的正确。 模型检查器使用状态空间探索系统地枚举系统的路径。 一旦执行了所有路径，就可以说系统是正确的。 模型检查器的示例包括 Spin11、MoDIST14、TLC7 和 MaceMC6。
然而，考虑到系统可能经历的大量输入和故障模式，运行详尽的模型检查器非常耗时且耗费资源。
组合
如果可证明正确的组件彼此组合以创建可证明正确的系统，则可以克服对形式化验证方法的一些反对意见和成本。 然而，事实并非如此。 通常，组件是在不同的故障模型下验证的，而这些模型显然不能组合。 此外，每个组件的正确性规范不会组合在一起以创建结果系统的正确性规范。1 为了证明结果系统是可证明的正确的，必须创建新的正确性规范，并且必须重新运行测试。
为组件的每个组合创建新的正确性规范无法很好地扩展，尤其是在最近流行的面向微服务的架构中。 这种架构由从数十个到数千个不同的服务组成，并且在这种规模下编写正确性规范是不可行的。
野外验证
鉴于形式化验证成本高昂，并且无法生成可以组合成可证明正确的系统的组件而无需额外工作，人们可能会感到绝望，并声称问题似乎毫无希望，分布式系统很糟糕，而且我们无法拥有美好的事物。
然而，一切并非都失去了！ 你可以使用测试方法来大大提高你构建的系统是正确的信心。 虽然这些方法没有提供经过验证的可证明正确性的“金星”，但它们确实提供了“看起来非常合法”的“银星”。
监控
通常，监控被认为是验证和测试分布式系统的一种手段。 监控包括指标、日志、分布式跟踪系统（例如 Dapper12 和 Zipkin2）以及警报。 虽然监控系统和检测错误是运行任何成功服务的重要组成部分，并且对于调试故障是必要的，但这完全是一种被动的方法来验证分布式系统； 只有当代码进入生产环境并影响客户后才能发现错误。 所有这些工具都提供了对你的系统当前正在做什么与过去所做的事情的可见性。 监控只允许你观察，而不应成为验证分布式系统的唯一手段。
金丝雀发布
金丝雀发布新代码是一种越来越流行的“验证”代码是否工作的方式。 它使用一种部署模式，其中新代码逐步引入生产集群。 不是用新代码替换服务中的所有节点，而是将少数节点升级到新版本。 将金丝雀节点的指标和/或输出与运行旧版本的节点进行比较。 如果它们被认为是等效或更好，则可以将更多节点升级到金丝雀版本。 如果金丝雀节点的行为异常或出现故障，则会将它们回滚到旧版本。
金丝雀发布非常强大，并且大大限制了将新代码部署到活动集群的风险。 然而，它提供的保证是有限的。 如果金丝雀测试通过，你唯一拥有的保证是金丝雀版本在此时此刻的性能至少与旧版本一样好。 如果服务未处于峰值负载下，或者在金丝雀测试期间未发生网络分区，则不会获得有关金丝雀版本与旧版本相比在这些场景中的性能的信息。
金丝雀测试对于验证新版本在常见情况下是否按预期工作以及服务中是否没有发生此路径中的回归最有价值，但它不足以验证系统的正确性、容错能力和冗余性。
单元测试和集成测试
长期以来，工程师们一直在其测试库中包含单元测试和集成测试。 然而，由于人们普遍认为故障难以在线下产生，并且创建类似生产环境的测试环境既复杂又昂贵，因此这些测试通常在分布式系统中被跳过或未被重视。
在 2014 年的一项研究中，Yuan 等人15 认为这种传统观点是不真实的。 值得注意的是，该研究表明：
* 三个或更少的节点足以重现大多数故障。
* 测试错误处理代码本可以防止大多数灾难性故障。
* 非致命错误的错误处理是大多数灾难性故障的原因。
单元测试可以使用模拟来证明系统内部依赖关系并验证各种组件的交互。 此外，集成测试可以重用这些相同的测试，而无需模拟，以验证它们在实际环境中是否正确运行。
最低限度应采用单元测试和集成测试，重点关注错误处理、无法访问的节点、配置更改和集群成员身份更改。 Yuan 等人认为，这种测试可以以低成本完成，并且可以大大提高分布式系统的可靠性。
随机模型检查器
QuickCheck9 等库旨在提供基于属性的测试。 QuickCheck 允许用户指定有关程序或系统的属性。 然后，它生成可配置数量的随机输入并针对该输入测试系统。 如果属性对所有输入都成立，则系统通过测试； 否则，将返回一个反例。 虽然 QuickCheck 无法声明系统是可证明的正确的，但它通过探索其状态空间的大部分来帮助提高对系统正确性的信心。 QuickCheck 并非专门为测试分布式系统而设计，但它可以用于生成分布式系统的输入，Basho 就是这样做的，它使用它来发现和修复其分布式数据库 Riak 中的错误。13
故障注入
故障注入测试会导致或引入系统中的故障。 在分布式系统中，故障可能是消息丢失、网络分区，甚至整个数据中心的丢失。 故障注入测试强制这些故障发生，并允许工程师观察和测量被测系统的行为。 如果未发生故障，这并不能保证系统是正确的，因为尚未执行故障的整个状态空间。
游戏日。 2014 年 10 月，Stripe 通过运行故障注入测试发现了一个 Redis 错误。 在 Redis 集群中的主节点上运行 kill -9 的简单测试导致该集群中的所有数据丢失。 Stripe 将其在生产环境中运行受控故障注入测试的过程称为游戏日演习。4
Jepsen。 Kyle Kingsbury 编写了一个名为 Jepsen3 的故障注入工具，该工具模拟被测系统中的网络分区。 模拟结束后，分析操作和结果，以查看是否发生数据丢失以及是否维护了声明的一致性保证。 事实证明，Jepsen 是一种非常有价值的工具，它揭示了许多流行的系统（例如 MongoDB、Kafka、ElasticSearch、etcd 和 Cassandra）中的错误。
Netflix Simian Army。 Netflix Simian Army5 是一套故障注入工具。 最初的工具名为 Chaos Monkey，它随机终止在生产环境中运行的实例，从而将单节点故障注入到系统中。 Latency Monkey 注入网络延迟，这可能看起来像是消息延迟或整个服务不可用。 最后，Chaos Gorilla 模拟整个亚马逊可用区宕机。
正如 Yuan 等人15 指出的那样，分布式系统中的大多数灾难性错误都可以用三个或更少的节点重现。 这一发现表明，故障注入测试甚至不需要在生产环境中执行并影响客户才能发挥价值和发现错误。
再次强调，通过故障注入测试并不能保证系统是正确的，但这些测试确实大大提高了对系统在故障场景下能够正确运行的信心。 正如 Netflix 所说，“有了不断壮大的 Netflix Simian Army 在我们身边，不断测试我们对各种故障的弹性，我们对我们处理在生产环境中将遇到的不可避免的故障以及最大限度地减少或消除其对我们订阅者的影响的能力感到更加自信。”5
谱系驱动的故障注入
与构建分布式系统一样，测试分布式系统也是一个极具挑战性的问题，并且是一个正在进行的研究领域。 当前研究的一个例子是 Peter Alvaro 等人描述的谱系驱动的故障注入。1 谱系驱动的故障注入器不会像模型检查器那样详尽地探索故障空间，而是推理成功的输出以及可能发生的会改变这种情况的故障。 这大大减少了必须测试才能证明系统正确的故障状态空间。
结论
形式化方法可用于验证单个组件是可证明的正确的，但正确组件的组合不一定会产生正确的系统； 需要额外的验证来证明组合是正确的。 对于基础架构和容错协议的基本部分，形式化方法仍然有价值且值得投入时间。 形式化方法应继续在学术环境之外找到更广泛的应用。
行业中的验证通常包括单元测试、监控和金丝雀发布。 虽然这为系统的正确性提供了一些信心，但这还不够。 应该编写更详尽的单元测试和集成测试。 应使用随机模型检查器来测试状态空间的很大一部分子集。 此外，应更广泛地使用通过故障注入强制系统发生故障的方法。 即使是简单的测试，例如在主节点上运行 kill -9，也发现了灾难性错误。
高效地测试分布式系统并不是一个已解决的问题，但通过结合形式化验证、模型检查、故障注入、单元测试、金丝雀发布等，你可以获得更高的系统正确性信心。
致谢
我要感谢那些提供反馈的人，包括 Peter Alvaro、Kyle Kingsbury、Chris Meiklejohn、Flavio Percoco、Alex Rasmussen、Ines Sombra、Nathan Taylor 和 Alvaro Videla。
参考文献
1. Alvaro, P., Rosen, J., Hellerstein, J. M. 2015. 谱系驱动的故障注入; http://www.cs.berkeley.edu/~palvaro/molly.pdf。
2. Aniszczyk, C. 2012. 使用 Zipkin 进行分布式系统跟踪; https://blog.twitter.com/2012/distributed-systems-tracing-with-zipkin。
3. Aphyr. Jepsen; https://aphyr.com/tags/Jepsen。
4. Hedlund, M. 2014. Stripe 的游戏日演习：从“kill -9”中学习; https://stripe.com/blog/game-day-exercises-at-stripe。
5. Izrailevsky, Y., Tseitlin, A. 2011. Netflix Simian Army; http://techblog.netflix.com/2011/07/netflix-simian-army.html。
6. Killian, C., Anderson, J. W., Jhala, R., Vahdat, A. 2006. 生存，死亡和关键过渡：在系统代码中查找活性错误; http://www.macesystems.org/papers/MaceMC_TR.pdf。
7. Lamport, L., Yu, Y. 2011. TLC—TLA+ 模型检查器; http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html。
8. Newcomb, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M. 2014. 亚马逊网络服务如何使用形式化方法。 2015. 美国计算机协会通讯 58(4): 68-73; http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext。
9. QuickCheck; https://hackage.haskell.org/package/QuickCheck。
10. Sheehy, J. 2015. 没有“现在”。 13(3); https://queue.org.cn/detail.cfm?id=2745385。
11. Spin; http://spinroot.com/spin/whatispin.html。
12. Sigelman, B. H., Barroso, L. S., Burrows, M., Stephenson, P., Plakal, M., Beaver, D., Jaspan, S., Shanbhag, C. 2010. Dapper，一种大规模分布式系统跟踪基础设施; http://research.google.com/pubs/pub36356.html。
13. Thompson, A. 2012. 为乐趣和盈利而 QuickChecking poolboy; http://basho.com/posts/technical/quickchecking-poolboy-for-fun-and-profit/。
14. Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., Zhou, L. 2009. MoDist：透明地模型检查未修改的分布式系统; https://www.usenix.org/legacy/events/nsdi09/tech/full_papers/yang/yang_html/index.html。
15. Yuan, D., Luo, Y., Zhuang, X., Rodrigues, G. R., Zhao, X., Zhang, Y., Jain, P. U., Stumm, M. 2014. 简单的测试可以防止大多数关键故障：对分布式数据密集型系统中生产故障的分析; https://www.usenix.org/conference/osdi14/technical-sessions/presentation/yuan。
16. Wilcox, J. R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M. D., Anderson, T. 2015. Verdi：用于实现和形式化验证分布式系统的框架。 SIGPLAN 2015 年编程语言设计与实现会议论文集: 357-368; https://homes.cs.washington.edu/~mernst/pubs/verify-distsystem-pldi2015-abstract.html。
Caitie McCaffrey 是一位后端专家和分布式系统大师。 她是 Twitter 的可观测性技术主管。 在此之前，她职业生涯的大部分时间都在 343 Industries、Microsoft Game Studios 和 HBO 构建为娱乐业提供支持的服务和系统。 她曾参与过几款视频游戏的开发，包括 Gears of War 2、Gears of War 3、Halo 4 和 Halo 5。 McCaffrey 拥有康奈尔大学计算机科学学位。 她在 CaitieM.com 上维护一个博客，并经常在 Twitter @Caitie 上讨论技术和娱乐。
最初发表于 Queue 杂志第 13 卷，第 9 期—
在 数字图书馆 中评论本文
更多相关文章
Martin Kleppmann, Alastair R. Beresford, Boerge Svingen - 在线事件处理
跨异构存储技术对分布式事务的支持要么不存在，要么在操作和性能特性方面表现不佳。 相比之下，OLEP 越来越多地用于在这些设置中提供良好的性能和强大的 一致性保证。 在数据系统中，日志通常用作内部实现细节。 OLEP 方法有所不同：它使用事件日志而不是事务作为数据管理的主要应用程序编程模型。 传统数据库仍然被使用，但它们的写入来自日志，而不是直接来自应用程序。 使用 OLEP 不仅仅是开发人员的实用主义，而且它还提供了许多优势。
Andrew Leung, Andrew Spyker, Tim Bozarth - Titus：将容器引入 Netflix 云
我们相信我们的方法使 Netflix 能够快速采用容器并从中受益。 虽然细节可能是 Netflix 特有的，但通过与现有基础设施集成并与合适的早期采用者合作来提供低摩擦容器采用的方法，对于任何希望采用容器的组织来说，都可能是一种成功的策略。
Marius Eriksen - 大规模函数式编程
现代服务器软件在开发和操作方面要求很高：它必须在所有时间和所有地点都可用； 它必须在毫秒内回复用户请求； 它必须快速响应容量需求； 它必须处理大量数据和更多的流量； 它必须快速适应不断变化的产品需求； 在许多情况下，它必须容纳一个大型工程组织，其众多工程师就像一个又大又乱的厨房里的厨师。
Philip Maddox - 测试分布式系统
分布式系统可能尤其难以编程，原因有很多。 它们可能难以设计、难以管理，而且最重要的是，难以测试。 即使在最佳情况下，测试普通系统也可能很困难，而且无论测试人员多么勤奋，仍然可能会出现错误。 现在，将所有标准问题乘以在多个可能都在不同操作系统上的多个框上运行的多种语言编写的多个进程，并且可能会发生真正的灾难。
© 保留所有权利。