CAP-n-Coq. Часть 1. Определения CAP-теоремы

No subject appears to be more controversial to distributed systems engineers than the oft-quoted, oft-misunderstood CAP theorem. The CAP FAQ

— Сейчас я тебе объясню... — Объяснить я и сам могу, ты расскажи, что на самом деле происходит! (Из разговора политологов, но для CAP-теоремы подходит тоже)

— Давайте уже запишем CAP в Coq и посмотрим, что там на самом деле. (Я)

О CAP-теореме

В индустрии распределённых систем есть обычай: любое обсуждение архитектурных решений рано или поздно скатывается к теореме CAP (эдакий аналог закона Годвина).

Долгое время эта тема проходила мимо меня. Я иногда пробегал, конечно, взглядом по CAP-статьям, в том числе и на habr, но в силу кажущейся тривиальности предмета обсуждения "пробеганием" дело и заканчивалось. Дискуссия удивляла своей живучестью и кликбейтностью заголовков: "Всё, что вы не знали о CAP-теореме", "Мифы о CAP-теореме"... что тут обсуждать (казалось бы)?

Чем проще кажется концепция, тем опаснее попытка разобраться в ней досконально. И вот, как-то мне встретился один "шероховатый", непонятный момент... Ладно, "OK, Google": [1], [2], [3], [4], [5].

После чтения "исходников" причины "холиварности" дискуссии стали понятны:

• In this paper we survey some of the confusion about the meaning of CAP, including inconsistencies and ambiguities in its definitions, and we highlight some problems in its formalization [3].

• The problem lies in the open-ended definitions of CAP which are subject to interpretations [5].

Шероховатостей, однако, прибавилось. Кроме того, читая критиков, захотелось покритиковать и их.

Светлый путь

Затевая стартап по очередному "объяснению"/"пониманию" CAP-теоремы, я понимал, что нужно иметь key differentiators. Должно быть что-то ещё, какое-то иное value, помимо выпадов в адрес коллег по цеху и явления миру ещё одной комбинации слов на тему правильного понимания сути распределённой троицы.

Первая руководящая идея появилась быстро — формализовать теорему с помощью инструмента для разработки формальных доказательств Coq, так вроде ещё никто не делал. В таком виде построения приобретают вид "окончательной бумажки", то есть строгого вывода из чётко определённой аксиоматики. Формальное обоснование будет приведено в третьей части этого исследования, а во второй будет введение в Coq — краткое, но вполне достаточное для понимания.

Вторая руководящая идея связана с тем, что в доказательстве есть ошибка. Чтобы её понять, простить и исправить, потребуется немного коснуться теории графов.

С учётом этого, считаю, напрасным чтение не будет.

Поехали!

Содержание

• Gilbert & Lynch

• Определения

  • Linearizable Consistency (Atomic Data Objects)

  • Availability (Available Data Objects)

  • Partitioned Network

  • Partition Tolerance

• Промежуточное заключение

• Продолжение

• Список литературы

Gilbert & Lynch

Скажу пару слов про бессмертную статью Gilbert & Lynch, "Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services", 2002 [2].

Генеративный ИИ claude.ai делает на неё такой обзор:

Эта статья посвящена исследованию так называемой "гипотезы Брюера" о построении распределённых веб-сервисов. В ней математически доказывается, что невозможно одновременно обеспечить три желаемых свойства веб-сервисов:

1. Согласованность (consistency) - все операции выглядят так, будто выполняются атомарно.

2. Доступность (availability) - каждый запрос должен получить ответ.

3. Устойчивость к разделению (partition tolerance) - система должна продолжать работать при разделении сети на части.

Авторы доказывают это утверждение для асинхронной модели сети, а затем исследуют возможные компромиссные решения в частично синхронной модели, где можно получить любые два свойства из трёх. Они также предлагают более слабые определения согласованности, которые могут быть достигнуты вместе с доступностью и устойчивостью к разделению.

Это фундаментальный результат в теории распределённых систем, известный как теорема CAP (Consistency-Availability-Partition tolerance), который оказывает большое влияние на проектирование современных распределённых систем и баз данных.

На что тут можно обратить внимание. Первое — занятное употребление термина web service (это был, напомню, 2002 год), цитирую:

Most web services today attempt to provide strongly consistent data. There has been significant research designing ACID databases, and most of the new frameworks for building distributed web services depend on these databases. Interactions with web services...

Второе — мол, "авторы доказывают это утверждение". Как мы убедимся, это доказательство далеко не "железное" и, помимо прочего, содержит ошибку. Всё это мы непременно исправим.

Идём дальше.

Определения

Интерпретатор Coq очень злой. Он даже злее, чем компилятор Rust (если такое вообще может быть). Вода из формализуемого текста должна быть беспощадно и полностью выпарена, иначе даже записать формулировку теоремы не получится.

Linearizable Consistency (Atomic Data Objects)

Рассуждая про согласованность (consistency), Gilbert & Lynch упоминают термин linearizable и дают такие пояснения (здесь и далее выделение моё):

Atomic, or linearizable, consistency is the condition expected by most web services today. 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. This is equivalent to requiring requests of the distributed shared memory to act as if they were executing on a single node, responding to operations one at a time.

Это определение сложно формализовать. Кроме того, в таким виде его можно спутать с One Copy Serializability, согласно Yadav & Butler [7]:

The One Copy Serializability is the highest correctness criterion for replica control protocols... In order to achieve this correctness criterion, it is required that interleaved execution of transactions on replicas be equivalent to serial execution of those transactions on one copy of a database.

Или даже просто с Serializability [8]:

Informally, serializability means that transactions appear to have occurred in some total order.

Для распределённых систем это относительно слабые гарантии, которые допускают аномалии Immortal Write (Бессмертная Запись), Stale Read (Несвежее Чтение), Causal Reverse (Обратная Причинность). Подробнее см. Daniel Abadi [11] (краткий пересказ можно посмотреть в моей статье).

Более современное определение linearizable дано в [9], тут уже нет про "single node":

Linearizability is one of the strongest single-object consistency models, and implies that every operation appears to take place atomically, in some order, consistent with the real-time ordering of those operations: e.g., if operation A completes before operation B begins, then B should logically take effect after A.

Простыми словами — каждое чтение получает результат последней (в смысле real-time) записи.

Резюмируя: термин linearizable - понятный, но понимать его мы будет чуть по другому.

Availability (Available Data Objects)

Gilbert & Lynch в секции Available Data Objects так определяют свойство continuously available (которое потом называют availability):

For a distributed system to be continuously available, every request received by a non-failing node in the system must result in a response. That is, any algorithm used by the service must eventually terminate. In some ways this is a weak definition of availability: it puts no bound on how long the algorithm may run before terminating, and therefore allows unbounded computation. On the other hand, when qualified by the need for partition tolerance, this can be seen as a strong definition of availability: even when severe network failures occur, every request must terminate.

Иными словами, если узел не "сломался", то он должен в конечном итоге отвечать на запрос. Иначе система не является continuously available.

Именно это определение, к слову, побудило меня разобраться в теме более подробно. Что такое non-failing node? Может ли алгоритм пометить узел как failing? Таким же вопросом задаётся и Martin Kleppmann [3]:

If it is possible for the algorithm to declare nodes as failed (e.g. if a node may crash itself), then the availability property can be trivially satisfied: all nodes can be crashed, and thus no node is required to respond.

Если следовать такой трактовке, то возможно существование CAP-систем (там же):

Alternatively, if a minority of nodes is permanently partitioned from the majority, an algorithm could define the nodes in the minority partition as failed (by crashing them), while the majority partition continues implementing a linearizable register.

Т.е. тут произошло P, некоторые узлы помечены как failing, оставшееся majority обеспечивает A и C.

В работе "Inadequacies of CAP Theorem" [5] проблему решают несколько странным образом:

Availability ensures that every request is answered, even in the case of failures.

Резюме: имеется неприемлемая неоднозначность, которую мы разрешим путём отбрасывания из определения части non-failing node. Т.е. если система available, то все узлы должны (eventually, в конечном итоге) отвечать на запросы. Исключений нет.

Partitioned Network

Gilbert & Lynch приводят, в принципе, хорошее определение partitioned network:

When a network is partitioned, all messages sent from nodes in one component of the partition to nodes in another component are lost.

Т.е. вот у нас есть сеть, сеть разбита на части, из первой части сообщения во вторую не проходят.

Однако в дальнейшем авторы (зачем-то) используют другую модель, в которой не только сообщения из первой части во вторую не проходят, но и из второй в первую — тоже:

Assume that the network consists of at least two nodes. Thus it can be divided into two disjoint, non-empty sets: G1, G2. The basic idea of the proof is to assume that all messages between G1 and G2 are lost.
...
Further, assume that no messages from G1 are received in G2, and no messages from G2 are received in G1.
...
During alpha2 no messages from G2 are received in G1, and no messages from G1 are received in G2

Martin Kleppmann, критикуя, даёт такое определение [3]:

A network partition has long been defined as a communication failure in which the network is split into disjoint sub-networks, with no communication possible across sub-networks. This is a fairly narrow class of fault, but it does occur in practice, so it is worth studying.

Он же приводит такую иллюстрацию в [4]:

Т.е. вот, два датацентра, кабель перерублен, и сообщения из одного датацентра в другой не проходят. Из другого в один тоже.

Работа "Inadequacies..." [5] определяет partition так:

A partition is a split within the systems in a distributed system which leads to complete loss of communications between affected nodes.

При этом ссылка идёт на "Perspectives on the CAP Theorem" (Gilbert & Lynch, 2012) [10], где partitioned network описывают следующим образом:

Unlike the other two requirements, this property can be seen as a statement regarding the underlying system: communication among the servers is not reliable, and the servers may be partitioned into multiple groups that cannot communicate with each other.

Велика ли разница между этими моделями? Велика. Gilbert & Lynch в рассматриваемом доказательстве не используют данное ими же определение для partitioned network и не рассматривают случай asymmetric network partition, т.е. ситуацию, когда сообщения из одной части сети в другую проходят, а в обратную сторону — нет. И никто явно такую ситуацию не рассматривает, просто "рубят кабель", и всё.

Мы же поступим иначе и будем моделировать сеть как направленный (рёбра имеют направления) и потенциально циклический граф. Вершины — узлы сети, рёбра — возможность передачи сообщений от одного узла к другому. Возможность эта — направленная, т.е. если существует возможность A->B, то это не означает, что существует возможность B->A.

И вот тут у нас появляются такие штуки, как Strongly Connected Graph и Strongly Connected Component:

A directed graph is called strongly connected if there is a path in each direction between each pair of vertices of the graph. That is, a path exists from the first vertex in the pair to the second, and another path exists from the second vertex to the first.
...
a strongly connected component of a directed graph G is a subgraph that is strongly connected, and is maximal with this property: no additional edges or vertices from G can be included in the subgraph without breaking its property of being strongly connected.

Иными язычными словами:

• Ориентированный граф называется сильно связным, если для каждой пары вершин графа существует путь в обоих направлениях: то есть существует путь от первой вершины в паре ко второй и путь от второй вершины к первой.

• Компонента сильной связности направленного графа G — это подграф, который является сильно связным и максимальным по этому свойству: нельзя добавить ни одну вершину или ребро из G в подграф, не нарушив его свойство сильной связности.

Иногда лучше рисовать, чем говорить, и данный случай как раз такой. Пример графа с несколькими компонентами сильной связности:

Тут имеются три компонента сильной связности: [[a,b,e], [c,d,h], [f,g]], между которыми связь хоть и есть, но "это другое".

В чём тут проблема? Согласно подходу, принятому в доказательстве от Gilbert & Lynch и подхваченному последователями/критиками, такая сеть не является partitioned, и математически как бы доказано, что эта система может обеспечить C и A. Но ведь если записать какое-нибудь значение в узел f, то узлы a, b и e его не "увидят"...

Резюме: тут имеется серьёзная проблема, которую мы решим путём введения новой модели сети. Partitioned будем определять так: сеть фрагментирована, если она содержит более одного компонента сильной связности.

Partition Tolerance

Gilbert & Lynch явно не определяют термин Partition Tolerance, кое-что можно понять про fault-tolerance:

When some nodes crash or some communication links fail, it is important that the service still perform as expected. One desirable fault-tolerance property is the ability to survive a network partitioning into multiple components.

Что такое survive не определено. Martin Kleppmann [3] определение Partition Tolerance "видит" вот в такой причудливой форме, констатируя неясность:

It is less clear what partition tolerance means. Gilbert and Lynch [25] define a system as partition-tolerant if it continues to satisfy the consistency and availability properties in the presence of a partition.

Далее Martin приводит ещё одно определение:

Fox and Brewer [24] define partition-resilience as "the system as whole can survive a partition between data replicas" (where survive is not defined).

Посетовав на избыточности и неоднозначности, автор заключает:

Thus, we can interpret partition tolerance as meaning "a network partition is among the faults that are assumed to be possible in the system."

Хорошие новости тут в том, что мы вообще не будем определять этот самый Partition Tolerance. Система может обладать двумя свойствами из трёх: A (availability), C (consistency) и P (partitioned), другого понимания P мы мыслить не будем.

Резюме: понятие Partition Tolerance не требуется.

Промежуточное заключение

В этой части мы рассмотрели определения CAP-свойств, которые приводят Gilbert & Lynch. Мы обнаружили, что да, критики правы — определения неоднозначны (мягко говоря). Неоднозначность эта как раз и приводит к множественным трактовкам и бесконечному "холивару".

Нам даже удалось найти ошибку в доказательстве Gilbert & Lynch.

Впрочем, нужно сказать, что в целом CAP-теорема сформулирована и доказана "почти верно". Мы лишь немного уподобимся сэру Исааку Ньютону, "встанем на плечи гигантов" и во второй части познакомимся с нотацией Coq, а в третьей — запишем в этой нотации CAP-теорему.

Продолжение

• CAP, Coq и Евклид

Список литературы

1. Eric A. Brewer. Towards robust distributed systems. Principles of Distributed Computing (Invited Talk), 2000. URL https://sites.cs.ucsb.edu/~rich/class/cs293b-cloud/papers/Brewer_podc_keynote_2000.pdf

2. Seth Gilbert and Nancy Lynch. Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services. ACM SIGACT News, 33(2):51–59, 2002. doi:10.1145/564585.564601. URL https://users.ece.cmu.edu/~adrian/731-sp04/readings/GL-cap.pdf

3. Martin Kleppmann. A Critique of the CAP Theorem. [Online], 2015. URL https://arxiv.org/pdf/1509.05393

4. Martin Kleppmann. Please stop calling databases CP or AP. [Online], 2015. URL https://martin.kleppmann.com/2015/05/11/please-stop-calling-databases-cp-or-ap.html

5. Omkar Patinge, Vineet Karkhanis, Amey Barapatre. Inadequacies of CAP Theorem. International Journal of Computer Applications (0975 – 8887) Volume 151 – No.10, October 2016. URL https://www.ijcaonline.org/archives/volume151/number10/patinge-2016-ijca-911921.pdf

6. D. Abadi. Problems with CAP, and Yahoo's little known NoSQL system. [Online], 2010. URL http://dbmsmusings.blogspot.com/2010/04/problems-with-cap-and-yahoos-little.html

7. D. Yadav and M. Butler, Rigorous Design of Fault-Tolerant Transactions for Replicated Database Systems using Event B. [Online], 2006. URL https://eprints.soton.ac.uk/262096/1/reft.pdfq

8. "Jepsen.io". Serializability. URL https://jepsen.io/consistency/models/serializable

9. "Jepsen.io". Linearizability. URL https://jepsen.io/consistency/models/linearizable

10. Seth Gilbert and Nancy Lynch. Perspectives on the CAP Theorem. 2012. URL https://groups.csail.mit.edu/tds/papers/Gilbert/Brewer2.pdf

11. Daniel Abadi. Correctness Anomalies Under Serializable Isolation. [Online], 2019. URL https://dbmsmusings.blogspot.com/2019/06/correctness-anomalies-under.html

12. Nancy Lynch. Distributed Algorithms. Morgan Kaufman, 1996. URL https://dl.acm.org/doi/pdf/10.5555/2821576