Hacker News Digest

AWS опубликовал отчет о недавнем сбое, связанном с race condition в системе управления DNS. Автор статьи воспроизвел упрощенную версию проблемы с помощью верификатора моделей Spin и языка Promela. В системе участвуют DNS Planner (создает планы) и три независимых DNS Enactor (применяют планы в разных зонах доступности). Race condition возникает, когда один Enactor применяет новый план и начинает очистку старых, в то время как другой, отставший, все еще обрабатывает более старый план. Когда первый Enactor завершает очистку, он удаляет этот "старый" план, который на самом деле еще активен, что приводит к исчезновению DNS-записей.

Используя Spin, автор смоделировал Planner и два параллельных Enactor. Каждый Enactor проверяет свежесть плана перед применением и отслеживает высший примененный план. Во время очистки он удаляет только значительно более старые версии, но если удаляемый план совпадает с текущим активным, это сбрасывает флаг dns_valid в false. Spin систематически проверял все возможные состояния системы и обнаружил последовательность действий, приводящую к race condition, подтвердив уязвимость.

• Пользователи обсуждают, что формальные методы (TLA+, Alloy и т.д.) могли бы предотвратить инцидент, если бы инвариант «не удалять активный план» был бы формализован и проверялся непрерывно.
• Обсуждается, что реальные системы часто отклоняются от «чистой» модели из-за компромиссов с производительностью и стоимостью хранения логов и т.д.
• Участники спора сходятся в том, что даже если бы формальные методы были бы применены, они бы не предотвратили бы ошибку, если бы не было процесса, который бы гарантировал, что модель и код синхронизированы.
• Некоторые комментаторы подчеркивают, что даже самые продвинутые инструменты не могут предотвратить ошибки, если нет культуры их использования и процессов, которые бы обеспечивали бы, что модель всегда актуальна.
• В конце концов, большинство соглашается, что самым важным является не наличие формальных методов, а культура их использования и процессов, которые бы гарантировали бы, что модель всегда отражает код.

В течение 19 и 20 октября 2025 года сервис Amazon DynamoDB в регионе Северной Вирджинии (us-east-1) столкнулся с серией сбоев, повлиявших на клиентов. Проблема началась 19 октября в 23:48 по тихоокеанскому времени и завершилась 20 октября в 14:20. Событие развивалось в три этапа. Сначала, до 2:40 утра 20 октября, клиенты испытывали повышенное количество ошибок API при обращении к DynamoDB. Во-вторых, с 5:30 утра до 14:09 20 октября, Network Load Balancer (NLB) испытывал повышенные ошибки подключения для некоторых балансировщиков. В-третьих, с 2:25 до 10:36 утра 20 октября, запуски новых экземпляров EC2 терпели неудачу, а те, что запустились, имели проблемы с подключением до 13:50.

Причиной инцидента стала редкая race condition в системе управления DNS DynamoDB. Эта система, ключевая для масштабируемости и отказоустойчивости DynamoDB, состоит из двух частей. DNS Planner создает планы обновления DNS на основе состояния пула серверов. DNS Enactor применяет эти планы, обновляя Route53 (систему DNS AWS). Обычно это работает надежно, но в данном случае два экземпляра DNS Enactor одновременно попытались обновить одну и ту же запись DNS, что привело к ее очистке. В результате, адрес dynamodb.us-east-1.amazonaws.com стал указывать в пустоту, и клиенты не могли установить соединение. Проблема была обнаружена и исправлена к 2:40 утра 20 октября, но вторичные эффекты привели к последующим инцидентам.

С 5:30 утра до 14:09 20 октября, Network Load Balancer (NLB) испытывал повышенные ошибки соединения для некоторых балансировщиков. Это было вызвано тем, что вторичный эффект инцидента DynamoDB привел к тому, что часть трафика NLB перенаправлялась на экземпляры, которые сами зависели от DynamoDB и стали недоступны. Это создавало каскадный эффект: пока DynamoDB был недоступен, часть трафика NLB терялась, что привело к ошибкам.

С 2:25 до 10:36 утра 20 октября, запуски новых экземпляров EC2 терпели неудачу. Это произошло потому, что сервис управления EC2 использует DynamoDB для хранения состояния, и когда DynamoDB был недоступен, он не мог создавать новые экземпляры. В 10:37 запуски возобновились, но до 13:50 некоторые экземпляры имели проблемы с сетью, так как они были созданы без полной конфигурации сети из-за race condition с NLB.

• AWS постмортем выглядит как маркетинговый документ, а не как техдок, что вызывает скепсис в честности их расследования.
• Сложность системы и отсутствие единого источника правды делает невозможным понять, действительно ли это была гонка условий или просто человеческая ошибка.
• Система, которая не может гарантировать согласованность DNS-записей, может быть сама по себе причиной сбоя.
• Похоже, что AWS не имеет четкого плана восстановления после сбоя, и их инструменты для этого зависят от самой системы, которую они пытаются восстановить.
• Постоянные сбои внутри AWS указывают на то, что их собственная инфраструктура неустойчива к сбоям, что вызывает вопросы о том, как они могли бы справиться с более серьезным инцидентом.