使用正确方法获得对系统正确性和弹性的信心

## 视频 <video src="https://dev-media.amazoncloud.cn/30-LibaiGenerate/31-LiBaiRebrandingVideo/ARC315-Gain_confidence_in_system_correctness___resilience_with_formal_methods-LBrebrandingWCaptionCN.mp4" class="bytemdVideo" controls="controls"></video> ## 导读 分布式应用程序、系统和服务很难设计和测试。形式化方法能够早期发现设计错误，这些错误可以逃脱设计评审和自动测试的障碍，但最终只能在生产中被发现。加入本论坛，了解亚马逊云科技如何使用 P（一种用于分布式系统的形式化建模和分析的开源、基于状态机的编程语言），推理其服务（例如 [Amazon S3](https://aws.amazon.com/cn/s3/?trk=cndc-detail) 和 [Amazon DynamoDB](https://aws.amazon.com/cn/dynamodb/?trk=cndc-detail)）的正确性。了解开发人员和架构师如何为自己的应用程序使用 P，以便在开发过程的早期发现错误，并提高开发人员的速度。 ## 演讲精华 <font color = "grey">以下是小编为您整理的本次演讲的精华，共2000字，阅读时间大约是10分钟。如果您想进一步了解演讲内容或者观看演讲全文，请观看演讲完整视频或者下面的演讲原文。</font> 主题为“运用形式化方法提升系统正确性与弹性信心”的会议，由亚马逊云科技的首席工程师Ankush Desai和高级解决方案架构师Vikas Chandra共同主持。Desai首先表达了对re:Invent会议时间的歉意，并向观众表示感谢。他表示期待探讨如何通过形式化方法提高复杂分布式系统的正确性和弹性信心。 Desai预料到听众在听到“形式化方法”这一术语时可能会产生质疑，因为这种方法通常与密集的数学证明和定理联系在一起。然而，他承诺此次演讲将提供一个轻松的介绍，不涉及过多数学内容，使即使在正确性推理极为困难的分布式系统中，人们也能够轻松理解和应用这些方法。 Desai希望传递的关键信息是，经过严格的形式化过程会带来诸多益处。在构建涉及多个服务跨网络协调的复杂分布式系统时，精心设计、规范编写和检查的迭代循环符合优秀的设计原则，并在长期内提高开发人员的效率。 形式化方法主要包括编写系统行为精确的数学规范以及正式验证实现是否满足这些规范的技巧。Desai用一个简单的定义来说明——任何编写正规规范并检查其是否符合的过程都可视为形式化方法。统一的主题是抽象思考和代码层级之上的推理。 Desai进行了一次非正式的投票，以了解观众在过去实际操作中是否有使用过形式化方法的体验。由于这个词对不同人来说代表不同的技巧，因此只有少数人举手。有些人认为使用逻辑进行数学证明是形式化方法，而另一些人可能认为将代码与指定属性和不变量进行测试是轻量级的形式化方法。 根据Ankush的看法，关键是在合适的抽象层次上编写和检查规范。对于分布式系统设计，这意味着关注对正确性至关重要的方面，同时忽略较低级别的细节，如性能优化或特定的实现结构。例如，他建议通过在伪代码原型中删除或注释代码来分析其是否违反面向客户的规范，或者只是影响非功能方面，如吞吐量。" "Ankush强调，仅仅思考是不够的——目标是将分布式系统设计精确地写下来，并严格检查与所需规范的对齐情况。随着设计通过迭代演变，应在实施之前在每个阶段重复应用此过程以建立信心。这激发了对自动化框架（如P）的需求，该框架可以在复杂分布式系统模型中实现全面的规格检查。" "P是亚马逊云科技为正式推理分布式系统而创建的开源编程框架。它提供了一种基于高级状态机的语言来建模分布式系统组件以及它们的作为通信状态机的交互。开发者可以用P表达正式的规范，以捕捉必须克服故障时保持的完整性要求和相关属性，如顺序、原子性和一致性等。然后，P的检查工具会详尽地探索所建模的分布式系统的所有可能行为，并在设计中形式验证规范始终得到满足。这在开发过程中起到了额外的严格的安全护栏作用，补充了测试。在实施后期发现逻辑错误非常昂贵，所以形式方法有助于在设计阶段本身消除微妙的缺陷。" "Ankush解释了如何在构建分布式系统的亚马逊云科技团队中使用P来分析协议和服务，然后在实施之前进行检查。例如，[Amazon S3](https://aws.amazon.com/cn/s3/?trk=cndc-detail)团队在使用P建模和检查时，确保在从最终一致系统过渡到强一致系统时，S3的数据一致性保证是强大的。 P帮助构建和验证涉及存储服务、元数据存储等组件之间复杂协调逻辑的模型，从而在S3中实现高一致性。经过详细的正式分析后，发现了许多测试中遗漏的案例错误。这使得S3团队在对协议设计充满信心之前，能够在最终的生产线编码之前进行深入的研究。 Ankush将P检查器视为一个引擎，它会系统性地探讨分布式系统模型的所有可能行为，考虑到所有可能的事件序列、消息交错和故障等情况。对于每个可达的系统状态，P检查器都会断言期望的规格和不变式是否成立。尽管详细的状态空间分析对大型实际系统似乎不可行，但P分析引擎中的数学抽象技术使得这一目标得以实现。 关键在于P能够通过在高抽象级别上推理系统模型来尽早发现潜在的漏洞。这使得它比传统的压力测试、故障注入等方法更为有效，因为后者通常关注的是实现代码。Ankush解释了亚马逊云科技是如何将P的形式化建模和分析集成到分布式系统的标准开发流程中的。这样可以在设计甚至开始编码之前就主动发现设计错误。 为了说明P建模的概念，Ankush展示了一个经典的两阶段提交协议的简单示例，该协议通常用于分布式事务处理。他描述了协调器和参与者组件如何可以被自然地建模为通过表示请求和响应的事件进行通信的状态机。全局规格也被作为观察事件的系统状态机在P中进行建模，并断言关键的不变式，如原子性——交易只有在所有参与者达成一致后才能提交。 测试用例模拟了各种情况，如协调器故障，以检查协议模型是否在任何条件下都遵守不变式。如果检测到违反，P检查器会提供详细的反例执行轨迹以帮助调试设计缺陷。Ankush通过展示在P中建模的示例协调器和规范状态机的熟悉命令式编程语言风格来强调P的优势。 安库什随后与亚马逊云科技的高级解决方案架构师维卡斯·钱德拉展开讨论，探讨如何运用P（Process Improvement）理论来验证任务关键型工作负载。维卡斯首先介绍了他在为客户设计关键银行、交易和保险应用程序时所扮演的角色。他强调，在设计审查过程中，客户经常会提出四个主要问题：一是在编程前确认设计方案能否正常运行；二是确保亚马逊云科技体系结构选项符合系统需求；三是通过混沌工程学技术检验系统在面临组件故障时的恢复能力；四是验证系统在极端情况下如全区域断电等情况下的生存能力和可用性。 维卡斯向安库什请教，如果在设计阶段就采用P对分布式系统进行建模，是否可以提前解决这些问题，而无需在实施后进行大量测试。尽管维卡斯过去并没有正式方法的实践经验，他还是愿意分享如何将P运用到分析常见的交易处理用例的过程中。他从一个包含五个组件的普通交易系统模型开始：接收器、预处理器、业务逻辑处理器、后处理器和传输器。这些组件被建模为在容器中运行并通过[Amazon SQS](https://aws.amazon.com/cn/sqs/?trk=cndc-detail)队列相互作用的微服务。 维卡斯解释道，P模型将分布式系统视为协作状态机，它们通过交换代表请求、响应、失败等事件来进行交流。队列、容器、数据库等状态机能够忠实捕捉来自独立并行执行的异步交互和复杂故障模式。 一个关键目标是确保从源生成的交易记录被可靠地准确地仅发送一次，并通过多级管道按顺序处理。P规范通过观察事件来检查测试用例的数千次迭代中关键的恒定条件是否成立。这种方法比有限的手动测试更能反映实际情况。 维卡斯展示了队列状态机如何根据事件在健康和故障状态之间转换，从而相应地影响发送/接收行为。这种设计真实地模拟了实践中发生的临时队列故障。类似地，状态机精确地代表了其他组件（如容器和数据库）的故障模式。 使用P建模交易处理管道后，维卡斯执行了一个正常条件的测试用例——发布10,000个记录，每个迭代有1,000个记录，所有状态机都处于良好状态。P检查器验证了在10,000次迭代中，顺序和仅发送一次的恒定条件得到满足，这增强了在设计正常条件下正确工作的信心。 接下来，运行一个混乱工程测试用例，其中注入随机的状态机故障，系统恢复，并发布新记录。P验证了在数千次迭代中，故障前后记录的有序处理。少数失败的迭代指出了与重复记录相关的恢复错误，通过添加去重逻辑解决了这些问题。 第三个测试用例锻炼了主从被动故障转移场景，即在主要区域完全中断的情况下，跨主区域和辅助区域进行活跃被动故障转移。P验证了在切换到辅助区域时，连续的交易处理过程。维卡斯解释了这些测试如何主动发现故障模式，并指导亚马逊云科技上弹性微服务的设计。 维卡斯分享了应用P的关键收获： 1. P易于使用，开发者只需要主流编程经验，不需要特殊的数学技能。 2. 在P中建模分布式系统非常快——交易处理系统模型只花了两周时间就创建好了。 P能够检测到了一些微妙的、难以重现的错误，这些错误在测试中可能很少出现——每100次运行中只有1次。简而言之，通过对数千次迭代进行规范检查和混沌测试，P实现了严格的设计时验证。这为我们投入全面实施前系统的正确性提供了信心。P与正式方法相辅相成，加速了在亚马逊云科技上构建健壮的分布式应用程序的速度。 根据亚马逊云科技团队多年来使用形式化建模的经验，Ankush分享了一些见解： 1. 建模过程作为一种“思考工具”，强迫设计师提前彻底回答关键问题： - 组件是如何相互作用以实现系统目标的？ - 必须始终保持的关键端到端不变数和规格是什么？ - 在保持正确性的情况下，系统设计可以容忍哪些序列和组合失败？ 2. 仅抽象思考就能发现许多逻辑错误，但仍有必要进行彻底的正式分析来揭示罕见的角落案例错误。 3. 总的来说，将正式方法融入开发过程可以通过在设计编码之前进行快速设计迭代和优化来提高开发者生产力。 最后，Ankush重申了像P这样的框架对于在亚马逊云科技上正确构建分布式系统的重要性。迄今为止，基于积极的体验，亚马逊云科技将继续将形式化验证方法更深入地整合到内部开发过程中。 Ankush邀请与会者采用GitHub上的开源P框架，以便对亚马逊云科技上的关键分布式工作负载充满信心。他表示愿意与客户更紧密地合作，将形式化验证方法应用于他们的需求。 这个在re:Invent上举行的热闹会议以一种易于理解的方式介绍了形式化建模和分析的概念，并展示了对于复杂分布式系统设计的优势。P框架通过规范、详尽检查和混沌测试对系统模型进行有条理的验证。通过尽早揭示细微错误，P帮助开发人员在亚马逊云科技的云计算基础设施上高效地构建可靠的分布式应用程序。 **下面是一些演讲现场的精彩瞬间：** Ankush Desai和Bea对如何通过形式化方法提高系统正确性和恢复力充满信心。  他们强调在开发过程中及早发现逻辑错误的重要性，以减少成本和努力。  他们讨论了可用于证明系统正确性的不同级别的形式验证，包括从手动证明到模型检查和基于属性的自动测试等自动化技术。  在设计复杂系统时，需要关注适当的抽象层次。  演讲者解释了检查器如何探索所有可能的交织来查找分布式系统中违反不变量的行为。  他们还分享了实现微服务中依赖关系失败时的快速故障以及在恢复失败依赖关系时需要明确恢复的关键见解。  ## 总结 安库什·德赛（Ankush Desai）和比阿（Bea）探讨了如何通过运用形式化方法来提高系统正确性和可靠性。据安库什介绍，构建分布式系统充满挑战，因为众多组件需要完美协作。通过采用编写规范并检验系统行为是否符合规范的形式化方法，可以在早期阶段发现并纠正错误。P框架能够创建系统组件的状态机模型，明确所需属性，并系统化地检查所有可能的行为是否满足规格。例如，亚马逊云科技（Amazon Web Services）已将此应用于其S3服务等产品中，以检测协议中的错误。 比阿分享了P如何助力交易处理系统的验证。她以队列、容器和数据库作为传递事件的状态机进行建模。测试案例涵盖了正常处理、混沌工程故障以及故障切换等场景，以检查记录交付是否具有不变性。这揭示了潜在的失败情景和可改进的设计方案。 核心收获在于P为设计师和测试人员等各类利益相关者提供了严格的验证手段，同时提高了开发人员的效率，因为他们可以在设计中不断迭代和承担风险。形式化方法带来了诸多益处，而P作为一个优秀的开源框架，正是开始实践它们的绝佳选择。 ## 演讲原文 ## 想了解更多精彩完整内容吗？立即访问re:Invent 官网中文网站！ [2023亚马逊云科技re:Invent全球大会 - 官方网站](https://webinar.amazoncloud.cn/reInvent2023/?s=8739&smid=19458 "2023亚马逊云科技re:Invent全球大会 - 官方网站") [点击此处](https://aws.amazon.com/cn/new/?trk=6dd7cc20-6afa-4abf-9359-2d6976ff9600&trk=cndc-detail "点击此处")，一键获取亚马逊云科技全球最新产品/服务资讯！ [点击此处](https://www.amazonaws.cn/new/?trk=2ab098aa-0793-48b1-85e6-a9d261bd8cd4&trk=cndc-detail "点击此处")，一键获取亚马逊云科技中国区最新产品/服务资讯！ ## 即刻注册亚马逊云科技账户，开启云端之旅！ [【免费】亚马逊云科技“100 余种核心云服务产品免费试用”](https://aws.amazon.com/cn/campaigns/freecenter/?trk=f079813d-3a13-4a50-b67b-e31d930f36a4&sc_channel=el&trk=cndc-detail "【免费】亚马逊云科技“100 余种核心云服务产品免费试用“") [【免费】亚马逊云科技中国区“40 余种核心云服务产品免费试用”](https://www.amazonaws.cn/campaign/CloudService/?trk=2cdb6245-f491-42bc-b931-c1693fe92be1&sc_channel=el&trk=cndc-detail "【免费】亚马逊云科技中国区“40 余种核心云服务产品免费试用“")