Теория языков программирования
Model Checking
Amazon нашёл баг в DynamoDB который мог привести к потере данных - через TLA+ спецификацию. Этот баг не был бы найден тысячами unit тестов или code review. Model checking - единственный способ верификации concurrent систем с доказательством.
- **Amazon AWS**: TLA+ для верификации DynamoDB, S3, EBS. Найдено 16 critical bugs включая potential data loss в DynamoDB replication
- **Microsoft Azure**: model checking для Cosmos DB consensus protocol - Paxos вариации с формальной гарантией корректности
- **Intel**: Spin и model checking для верификации CPU cache coherency protocols. Ошибки в silicon невозможно исправить после производства
Темпоральная логика
Темпоральная логика расширяет классическую логику операторами времени: G (globally - всегда), F (finally - когда-нибудь), X (next - в следующем состоянии), U (until - пока не). Это язык для формального описания свойств системы.
Safety и liveness - дополняющие классы. Deadlock = нарушение safety (G(!deadlock)) и liveness (G(F(progress))). TLA+ разделяет invariants (safety) и temporal properties (liveness).
Что означает формула G(request -> F(response)) в темпоральной логике?
CTL - Computation Tree Logic
CTL (Computation Tree Logic) - разветвлённая темпоральная логика. Квантификаторы A (все пути) и E (существует путь) комбинируются с темпоральными операторами: AG, AF, AX, EU, AU, EG, EF, EX. Model checker проверяет CTL формулы за O(|M| * |phi|).
В чём разница между AGp и EGp?
LTL и SPIN
LTL (Linear Temporal Logic) - линейная темпоральная логика: рассматривает одну трассу (последовательность состояний). SPIN - model checker для LTL, использует Promela язык для описания concurrent систем.
Что происходит когда SPIN находит нарушение LTL свойства?
TLA+
TLA+ (Temporal Logic of Actions) - язык для формальной спецификации и верификации распределённых систем. Разработан Leslie Lamport (создатель Paxos). AWS, Microsoft, Intel используют TLA+ для верификации критических алгоритмов.
Amazon использовал TLA+ для верификации S3, DynamoDB, EBS. AWS blog: 'We have used TLA+ to find 16 bugs including a bug in DynamoDB replication that could cause data loss'. 7 из 10 найденных багов не были бы обнаружены code review.
Formal verification слишком сложна и академична для реальных проектов
AWS, Microsoft Azure, Intel CPU verification, Curiosity Mars Rover используют formal methods. TLA+ нашёл баги в DynamoDB, который поддерживает 10 триллионов запросов в день
Формальные методы дорогие для 100% кода, но критически важные для concurrency алгоритмов, протоколов консенсуса, криптографии. Цена ошибки в DynamoDB >> цена TLA+ спецификации
Что означает count' в TLA+?
Итоги
- **Темпоральная логика**: G (always), F (eventually), X (next), U (until). Два класса: safety (ничего плохого) и liveness (что-то хорошее)
- **CTL**: A (all paths) и E (exists path). AGp - invariant на всех путях. Model checking за O(|M|*|phi|)
- **SPIN + Promela**: concurrent системы + LTL свойства -> counterexample с конкретным сценарием ошибки
- **TLA+**: спецификация distributed систем. AWS использует для DynamoDB, S3. Нашёл баги которые code review не нашёл
Связанные темы
Model checking - часть формальной верификации:
- Property-based testing — Property testing - более лёгкий подход к верификации свойств без полного перебора
- Theorem provers — Proof assistants (Coq, Isabelle) дают более сильные гарантии, но требуют ручных доказательств
Вопросы для размышления
- Model checking страдает от state explosion: 10 boolean переменных = 2^10 состояний. Как symbolic model checking (BDD, SAT) решает эту проблему?
- TLA+ нашёл баги в AWS которые не нашёл code review. Что это говорит о границах традиционного code review для distributed systems?
- Paxos доказан правильным для consensus. Но реализации Paxos (Multi-Paxos, Raft) имеют баги. Почему формальная спецификация алгоритма не гарантирует корректность реализации?