InfoQ 播客: Caitie McCaffrey 谈工程有效性和验证分布式系统

本周的 InfoQ 播客内容是 QCon 主席 Wes Reiszt 和 Werner Schuster 与 Caitie McCaffrey 之间的谈话。Caitie McCaffrey 在 Twitter 的工程有效性团队工作，专注于分布式系统。他曾经就职于 343 Industries、微软游戏工作室和 HBO 电视网等，对于构建支撑娱乐内容的大型分布式服务和系统有丰富经验。Caitie McCaffrey 在这次 QCon 纽约大会上演讲的题目是“验证分布式系统”。

关键要点

• Twitter 的工程有效性团队主要任务是不断改进开发工具，要让程序员们工作更愉快，更高效。
• 如果仅仅因为性别而请人在你的会议上讲话，或者邀请人家加入你的团队，这种行为的害处远超大家想象。
• 没有什么约定俗成的办法来打造又好又成功的技术。
• 即使有时候没有时间做测试，也有别的办法来提高你对你的系统的信心。
• 运行单元测试的最大问题是它只是在测试你写死在测试用例中的那些输入值。

要点

工程有效性

• 1 分:24 秒 - Twitter 的工程有效性团队主要任务是不断改进开发工具，要让程序员们工作更愉快，更高效。
• 2 分:44 秒 - 团队在努力实现一些架构，这样就不必让每个团队都自己去解决那些分布式问题。为开发者们提供一些 API 和工具，这样大家就可以很容易的构建系统。
• 3 分:45 秒 - 挑战之一是我们用超时来做分布式系统中的失效检测，但有的任务一跑就是一个小时，没办法设置超时时间，所以就有很多不同的事情要做。对于用户要执行的有多个子任务的任务，我们使用了 SAGA 模式。SAGA 也是一种处理分布式事务的办法，它可以保证一个任务的所有子任务都正常运行。
• 6 分:01 秒 - 如果你是离线的，那所有东西都要在你断线时运行，并且要在你连上 VPn 或者网络时就立刻在后台进行身份认证，并且把构建等任务都跑得更快。

趋近多样性

• 7 分:30 秒 - 他们让我多说些，我想他们本意肯定是好的。但如果退后一步再多想一下，假如因为我是一位女士而被要求发言时，那好像就是在说：“你把这些事情全都做了吧，但我们只是因为你是个女的才找你的。”
• 8 分:35 秒 - 有很多奇怪的现象，就是说出来的话和本来要表达的意思是不一样的，但是这样的谈话却到处都在发生，这让大家实在感觉太不好了。有许多本意是好的东西却给人造成了意想不到的伤害，这就是其中之一。
• 11 分:05 秒 - 很多问题最终都归因于网络故障。人们会说，在技术上没有怎么怎么样的团队。但是看看 Helena Price 他们的 Techies 项目，他们的团队也是由各种不同背景的人组成的。Price 在旧金山也没怎么花力气招聘，就招到了这些人。

验证分布式系统

• 12 分:55 秒 - 由于各种原因，测试并不是我们团队很擅长的一项技能。
• 13 分:30 秒 - 有很多方法来提高你对你的代码的信心，也有很多事例证明做测试有时候带来的回报并不如你直观想像的那么多。
• 13 分:54 秒 - 我们人手有限，又要按时提交项目，那我们哪里有时间做测试呢？事实上是有别的办法来让你相信你的系统可以如愿运行的。
• 14 分:30 秒 - 我们都在构建分布式系统。我在谈的是单元集成测试，以及一些你要关注的而且可以获得最大价值回报的方面，就是基于属性的测试，它差不多是模型检验器和错误注入测试的工业版。它们中的每一个都有很多值得你去投资的内容。
• 16 分:30 秒 - 形式验证是非常有趣的，亚马逊用 TLA+ 来验证他们的核心架构内容，比如 S3。Koch 不太为人所知，你可以用它来写下你的描述，然后生成 Ocaml 代码。Diego Ongaro 刚刚发布了 Runway，也是一个形式描述工具。
• 18 分:33 秒 - 对这方面研究成果会是非常巨大的，因为这可以让我们把事情做得更好，而不必把过多时间花在测试、验证和调试上。

模型驱动开发

• 20 分:40 秒 - Leslie Lamport 写过一本关于 TLA+ 的书，书中提到在实现系统之前先做好设计是个非常好的想法。在你实现之前，你应该先把规范写出来，因为它会逼着你把整个事情从头到尾都想清楚。
• 21 分:00 秒 - 写规范就是形式验证的第一步，你可以用模型检验器来先跑一遍检查一下。做这件事是非常有用的，甚至不必再试着去证明它是正确的，因为许多的 BUG 在写规范的过程中就会被发现了。
• 21 分:30 秒 - 做这件事是有非常重大意义的，特别是处理很多非常复杂的系统和异步消息时，处理不同级别的一致性会更加困难。

类型理论

• 22 分:45 秒 - 如果你仍然想用和以前写代码一样的方式去写，那你可以先写一个顶层描述——跑一些东西就可以知道正确与否需要你有比较强的类型理论，或者是用某种编程语言写的类型系统。但象 Go、JavaScript 或 Python 等没有类型的语言是不属于我们现在讨论的范围之内的，要想它们也能运行一个形式方法检验器就可以检查错误，除非有的人正在为它们构造类型系统。

属性测试

• 24 分:58 秒 - 我觉得属性测试超级有用。QuickCheck 是 John Hughes 写的，它的思想就是你为你的系统定义一些属性，那你就可以通过这些属性的各种组合来构造复杂的测试用例。
• 25 分:38 秒 - 运行单元测试的最大问题是它只是在测试你写死在测试用例中的那些输入值。
• 26 分:06 秒 - 如果你用一个基于属性的测试工具来定义这些东西的话，它很象一个模型检验器，但它不会测试整个系统的所有状态。你不能说这样的系统就没问题了，但是它测到的内容肯定比单元测试多。
• 27 分:05 秒 - 你可以用这种方法发现许多隐藏得很深的 BUG，因为它可以产生非常多的输入，以及各种输入的组合。

错误注入

• 30 分:12 秒 - Kyle Kingsbury 的 Jepsen 是一个非常好的错误注入和分析工具。
• 30 分:35 秒 - 也有许多别的办法来注入错误，比如你把一个服务杀掉，再看看系统的反应怎么样。
• 31 分:09 秒 - 我的许多灵感都来自于 Peter Alvaro 关于错误注入的论文，或者说他的工具 Molly。

关于 QCon 大会

QCon 大会是由 InfoQ 主办的全球顶级技术盛会，由业内人士推动，专为在团队中影响软件创新的技术团队主管、架构师以及项目经理而设计。QCon 每年的七场大会分别在伦敦、纽约、旧金山、圣保罗、北京、上海和东京召开。QCon 旧金山大会已经举办到第十届，今年将于 2016 年 11 月 7-11 日举行，届时会有 100 多名业内专家作为演讲嘉宾，并有 1300 多名与会者以及 18 个涉及如今推动软件开发发展的专题追踪报道。想要了解更多详情，请参见 qconnewyork.com 网站。

阅读英文原文： The InfoQ Podcast: Caitie McCaffrey on Engineering Effectiveness and Verifying Distributed Systems