博士

やあ、ロボ子。今日はAWSの障害に関する事後分析を基にした、DynamoDBのDNS管理システムの競合状態をモデル検査器Spinで再現した実験について話すのじゃ。

ロボ子

博士、こんにちは。AWSでも障害が起こりうるのですね。でも、信頼性の高い記録があるのはさすがです。

博士

そうじゃな。今回の対象システムは、DNS Planner、DNS Enactor、そしてAmazon Route 53 serviceじゃ。DNS Plannerが計画を作成し、DNS Enactorがそれを適用するのじゃ。

ロボ子

DNS Enactorは3つの可用性ゾーンで独立して動作するのですね。具体的にはどのように動くのですか？

博士

まず、最新の計画を取得し、以前に適用されたものより新しいか確認する。そして計画を適用後、古い計画を削除するクリーンアッププロセスを実行するのじゃ。

ロボ子

なるほど。ここに競合状態が発生する可能性があるのですね。Enactor 2が新しい計画を適用してクリーンアップを開始し、Enactor 1が少し遅れて古い計画を適用すると...

博士

そう！Enactor 2がクリーンアップを完了し、Enactor 1が適用した計画を削除してしまうと、DNSエントリが消失してしまうのじゃ！

ロボ子

それが今回の障害の原因だったのですね。それをモデル検査器Spinで再現した、と。

博士

その通り。Spinを使って、システムの各部分をプロセスとしてモデル化し、Promela言語で記述したのじゃ。DNS PlannerとDNS Enactorをモデル化してな。

ロボ子

DNS Enactorの状態として、`current_plan`、`dns_valid`、`highest_plan_applied` があるのですね。そして、不変条件として「新しい計画が適用されたら、DNSを削除してはならない」を設定した、と。

博士

`ltl no_dns_deletion_on_regression` として記述したのじゃ。モデル検査器は不変条件の違反をちゃんと報告してくれたぞ。

ロボ子

素晴らしいですね！トレースファイルから、2つのEnactorが並行して動作し、一方が他方より遅れている場合に競合が発生することが分かったのですね。

博士

そうじゃ。問題のあるステートメントをアトミックに実行することで修正できたぞ。不変条件は正当性を確立するために非常に重要なのじゃ。

ロボ子

今回の教訓は、大規模システムにおける競合状態の発見と、モデル検査の有効性ですね。モデルは簡略化されているため、実際のシステムとのギャップがある可能性があるという点も重要ですね。

博士

その通りじゃ！今回の実験のリポジトリは [https://github.com/wyounas/aws-dns-outage-oct-2025-modeling/](https://github.com/wyounas/aws-dns-outage-oct-2025-modeling/) にあるから、ロボ子も見てみると良いぞ。

ロボ子

ありがとうございます、博士。確認してみます。

博士

しかし、ロボ子よ。モデル検査でバグが見つかったからといって、安心してはいけないぞ。なぜなら、バグはいつだって…

ロボ子

博士、まさか…

博士

バグはいつだって、君の隣にいるかもしれないからな！…なーんてな！