Оригинал
Telegram: book_cube
Оригинальный пост с разбором CAP теоремы.
Знаменитой CAP теореме уже больше 25 лет. Разберём, что это такое, зачем она нужна и как появилась. Про это есть отличная статья от Eric Brewer, автора теоремы, которую хотелось вспомнить, так как она хороша.
Фундамент
TCP протокол
Сетевые разделения и задержки напрямую влияют на CAP-компромиссы.
Формулировка теоремы
"The CAP theorem states that any networked shared-data system can have at most two of three desirable properties"
Эквивалентно наличию единой актуальной копии данных
Высокая доступность данных для обновлений
Устойчивость к сетевым разделениям
Фундамент
Модель OSI
Полезна для разбора сетевых слоёв и причин partition.
Визуализация CAP
Интерактивная CAP диаграмма
Нажмите на свойство или тип системы для изучения взаимосвязей
Атомарная или линеаризуемая консистентность
Ответ на каждый запрос
Устойчивость к сетевым разделениям
Типы систем
Важный нюанс
В реальных распределённых системах Partition Tolerance — это не опция, а необходимость. Сетевые разделения неизбежны, поэтому реальный выбор — между CP и AP стратегиями.
Презентация
PODC 2000
Оригинальная презентация Эрика Брюера на симпозиуме.
История появления
Осенью сформулирована CAP теорема
Опубликована в статье "Harvest, Yield, and Scalable Tolerant Systems" в ACM
Представлена на симпозиуме "Symposium on Principles of Distributed Computing"
Доказана формально (консистентность превратилась в линеаризуемость)
Связанная глава
DDIA
Детальный разбор консистентности и репликации в книге Клеппманна.
Распространённые заблуждения
Теорема пошла в массы и превратилась в упрощённое «выберите 2 из 3», что является сильным упрощением по трём причинам, которые указывает Эрик Брюер:
Редкость разделений
Из-за редкости partition нет смысла выбирать между C и A постоянно. Большую часть времени система может обеспечивать оба свойства.
Гранулярность решения
Решение о C или A принимается не единоразово для всей системы, а на уровне отдельных операций или типов данных. Разные части системы могут следовать разным стратегиям.
Непрерывный спектр
C, A, P — это не бинарные свойства, а скорее непрерывные. Availability варьируется от 0 до 100%, уровни консистентности тоже бывают разные, и даже partitions имеют нюансы.
Режим разделения (Partition Mode)
В отсутствии разделения системы мы можем обеспечивать и A, и C. Во время проблем нужен понятный алгоритм:
Определение
Обнаружение факта сетевого разделения
Переход
Явный переход в partition mode с ограничением операций
Восстановление
Процесс восстановления консистентности и компенсации ошибок
Связанная глава
Database Internals
Глубокое погружение в транзакции и уровни изоляции.
Связь с ACID и BASE
ACID
⚠️ Consistency в ACID — это про целостность данных относительно бизнес-правил, а не про CAP.
BASE
Первые два свойства помогают достигать доступности при разделении системы на части.
Роль задержки (Latency)
Latency отсутствует в классической формулировке, но неявно присутствует. Выполняя операцию в разделённой системе, мы должны принять решение:
Отменить операцию
Уменьшить доступность в пользу консистентности
Продолжить операцию
Принять риск неконсистентности данных
Ключевой инсайт
С прагматической точки зрения разделение — это ограничение по времени (таймаут). Чем жёстче time bounds, тем выше вероятность попадания в partition mode, даже при медленной сети без реального разделения.
Ключевые выводы
- Не существует глобального понятия partition — некоторые узлы могут его обнаружить, а другие нет
- Узлы, обнаружившие partition, входят в partition-mode — ту часть, где нужно выбирать между C и A
- Проектировщики выставляют time bounds для соответствия целевым скоростям ответа
- CAP — это не выбор «2 из 3», а управление компромиссами во время сетевых проблем
Связанные главы
Оригинал
Telegram: book_cube
Пост с разбором формального доказательства CAP теоремы.
Формальное доказательство CAP
В 2002 году Seth Gilbert и Nancy Lynch опубликовали whitepaper, в котором гипотеза Брюера стала формальной теоремой.
"It is impossible for a web service to provide the following three guarantees: consistency, availability, partition-tolerance"
Формализация свойств
1. Consistency (Линеаризуемость)
Авторы определяют консистентность как atomic data objects (линеаризуемая консистентность):
"Under this consistency guarantee, there must exist a total order on all operations such that each operation looks as if it were completed at a single instant."
Система ведёт себя так, как будто работает на одном узле, обрабатывая операции по одной.
2. Availability (Доступность)
Каждый запрос, попавший на несбойную ноду, должен получить ответ. Алгоритм должен завершаться (eventually terminate). Это слабое определение — нет верхней границы времени ответа. Но с позиции partition-tolerance это сильное определение — даже при сбоях в сети каждый запрос должен завершиться.
3. Partition-Tolerance
В сети может теряться произвольное количество сообщений между нодами:
"When a network is partitioned, all messages sent from nodes in one component of the partition to nodes in another component are lost."
Доказательство
1Теорема для асинхронных систем
Theorem 1:
It is impossible in the asynchronous network model to implement a read/write data object that guarantees Availability and Atomic consistency in all fair executions (including those in which messages are lost).
Доказательство методом от противного:
- Предположим, что такой алгоритм существует
- Представим систему из двух нод: G₁ и G₂
- Допустим, что все сообщения между G₁ и G₂ теряются (partition)
- Происходит запись в G₁
- Позже происходит чтение из G₂
- Чтение с G₂ не сможет вернуть значение, записанное в G₁
- Противоречие: нарушена либо консистентность, либо доступность
2Теорема для частично синхронных систем
Theorem 2:
It is impossible in the partially synchronous network model to implement a read/write data object that guarantees Availability and Atomic consistency in all executions (even those in which messages are lost).
В реальном мире используются частично синхронные системы — у нод есть часы для замера времени и таймаутов. Но даже в этом более мощном сетапе результат аналогичен: доказательство следует той же логике.
Примечание: Оставшаяся часть whitepaper посвящена Delayed-t consistency в частично синхронных системах — компромиссному подходу, ослабляющему требования консистентности.