文章探讨了如何利用Spin模型检查器复现AWS因DynamoDB自动DNS管理系统中的竞争条件导致的故障。作者基于AWS的事后分析报告，通过简化模型，重点研究了DNS规划器、执行器与Route 53服务间的并发交互问题，展示了形式化验证对发现复杂系统中微妙并发缺陷的价值。

标题：使用模型检查器复现AWS故障中的竞态条件

2025年10月30日

AWS发布了一份关于近期服务中断的事后分析报告[1]。像AWS这样的大型系统非常复杂，在这种规模下运行时难免会出现问题。不过，AWS在可靠性方面一直保持着令人印象深刻的记录。

报告中提到的竞态条件引起了我的注意。虽然不了解AWS内部架构的全部细节，但根据报告提供的信息和一些合理假设，我们可以尝试复现这个问题的简化版本。

作为一个小型实验，我们将使用模型检查器来探究这种竞态条件是如何发生的。虽然形式化验证不能预防所有故障，但它能帮助我们更清晰地思考正确性，并推理出那些微妙的并发错误。为此，我们选择使用Spin模型检查器及其Promela语言。

报告包含大量细节，但为简化起见，我们只关注竞态条件这一方面。该事件是由DynamoDB的自动化DNS管理系统中的一个缺陷触发的，涉及DNS规划器（DNS Planner）、DNS执行器（DNS Enactor）和Amazon Route 53服务三个组件。

DNS规划器创建DNS计划，而DNS执行器则寻找新的DNS计划并将其应用到Route 53服务。三个执行器在三个不同的可用区独立运行。

根据我的理解，DNS执行器的工作流程如下：它获取最新计划，在应用前执行一次性检查以确保该计划比之前应用的更新，然后应用该计划并启动清理过程。在清理过程中，它会识别并删除比当前应用计划早得多的旧计划。

通过事件报告中的细节，我们可以勾勒出可能导致竞态条件的交错执行场景：两个执行器并行运行——执行器2应用新计划并开始清理，而稍慢的执行器应用了一个旧计划使其成为活动计划。当执行器2完成清理时，它删除了这个活动计划，导致DNS条目消失。

让我们尝试用模型检查器揭示这种交错执行。在Promela中，我们可以将系统的每个部分建模为独立的进程。Spin会从初始状态开始，系统地应用每个可能的转换，探索所有交错执行以构建可达状态集[2]。它会检查每个状态下你的不变量是否成立，如果发现违反，则报告反例。

在我们的简化模型中，我们运行一个DNS规划器进程和两个并发的DNS执行器进程（AWS实际运行三个，此处做了抽象）。规划器生成计划，通过Promela通道将这些计划发送给执行器处理。

在每个DNS执行器中，我们跟踪系统状态的关键方面：执行器在currentplan中保存当前计划，用dnsvalid表示DNS健康状态，并在highestplanapplied中记录已应用的最高计划。为模拟活动计划被删除的情况，执行器的清理过程会检查currentplan是否等于被删除的计划，如果是，则将dnsvalid设为false。

我们通过设置不变量来发现竞态条件：一旦应用了更新的计划，DNS就绝不应该被删除。当用模型检查器运行这个不变量时，它报告了一个违反情况，并生成一个轨迹文件逐步展示系统如何进入错误状态。

轨迹文件显示：较快的执行器应用计划4并开始清理，删除了计划1和2但跳过了3；较慢的执行器随后应用计划3使其成为活动计划；当较快执行器再次清理时，它删除了计划3导致DNS失效。

在重新阅读事件报告后，我注意到："此外，由于活动计划被删除，系统处于不一致状态..."。这提示了一个直接的不变量：活动计划绝不能删除。用这个不变量运行模型检查器会产生与之前基本相同的反例。

要修复代码，我们需要以原子方式执行有问题的语句。你可以在随附的代码库[3]中找到存在竞态条件的版本和修复后的版本，以及交错执行轨迹。由于缺乏AWS内部设计细节，这个模型必然做了简化。如果有更多时间和上下文，当然可以构建更精确的版本。

（注：文中涉及的代码片段和图示链接已保留原意但未完整呈现，实际翻译时应确保技术术语的准确性和上下文一致性）

参考资料： 1. AWS事后分析报告 2. 并发工作原理可视化指南 3. 源代码仓库 4. Spin模型检查器

总结评论内容：

1. 对形式化方法应用的质疑

• 认为现实系统常需偏离"纯净"模型进行妥协(grogers) "Real world systems often have to deviate from the 'pure' version...you have to compromise" "当网络恢复时，这些调用开始成功，但现在的状态比你预想的要陈旧得多"

• 认为事后分析的价值有限(muglug) "this particular excercise is very hindsight-is-20/20" "这个不变量在事后看来很明显，但很难说是公理性的"

2. 对模型检查器适用性的讨论

• 认为问题过于简单不适合用模型检查器(mmiao) "it's a simple toctou problem.. Using model checker sounds weird" "模型检查器适合具有多状态和复杂转换的问题"

3. 其他观点

• 希望获得更多学习资源(tonetegeatinst) "Wish the author had an introduction to model checker article" "我还没有学习过这个，暂时不会花时间研究"

• 对分析材料不足的质疑(philipwhiuk) "It's not like they have anything other than the RCA" "我不太理解这样做的目的"