Posts

Showing posts from November, 2025

TLA+ Modeling of AWS outage DNS race condition

Image
On Oct 19–20, 2025, AWS’s N. Virginia region suffered a major DynamoDB outage triggered by a DNS automation defect that broke endpoint resolution. The issue cascaded into a region-wide failure lasting nearly a full day and disrupted many companies’ services. As with most large-scale outages, the “DNS automation defect” was only the trigger; deeper systemic fragilities ( see my post on the Metastable Failures in the Wild paper ) amplified the impact. This post focuses narrowly on the race condition at the core of the bug, which is best understood through TLA+ modeling. My TLA+ model builds on Waqas Younas’s Promela/Spin version . To get started quickly, I asked ChatGPT to translate his Promela model into TLA+, which turned out to be a helpful way to understand the system’s behavior, much more effective than reading the postmortem or prose descriptions of the race. The translation wasn’t perfect, but fixing it wasn’t hard. The translated model treated the enactor’s logic as a single atom...

Popular posts from this blog

Hints for Distributed Systems Design

My Time at MIT

Scalable OLTP in the Cloud: What’s the BIG DEAL?

Foundational distributed systems papers

Advice to the young

Learning about distributed systems: where to start?

Distributed Transactions at Scale in Amazon DynamoDB

Disaggregation: A New Architecture for Cloud Databases

Making database systems usable

Use of Time in Distributed Databases (part 1)