CAP теорема

Часто приходится слышать фразы вроде: "CAP теорема доказана" или: "Это не возможно из-за CAP теоремы". Я решил разобраться, что такое CAP теорема, и что доказано.

Высказывание Брювера

CAP теорема - это утверждение о работе распределенных БД. В 2000 году в своем докладе Брювер сформулировал это утверждение. Оно звучало примерно так.

Не существует распределенных баз данных, в которых бы одновременно выполнялись три свойства:

1. Согласованность (Consistency)
2. Доступность (Availability)
3. Устойчивость к разделению сети (Partition tolerance). То есть устойчивость к сбоям в сети.

Вообще говоря, правильно это высказывание называть чем-то вроде тезиса, но не теоремой уж точно. Так как в таком виде это высказывание не формализовано, я уже не говорю про доказательство. Но автор в своем докладе назвал это теоремой.

Формализация и доказательство

Далее вышла очень интересная статья в 2002 году, где высказывание Брювера было формализовано.

1. Под согласованностью подразумевалась атомарность. То есть, если завершилась какая-то операция записи, то операция чтения, которая следует за ней возвращает это новое значение или еще более новое.
2. Доступность. Если запрос поступает в узел, который не вышел из строя, то этот запрос будет корректно выполнен.
3. Устойчивость к разделению сети. Произвольное число сообщений внутри сети могут потеряться.

Далее, невозможность этих трех свойств одновременно была доказана для асинхронных сетей.

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

Доказательство самой CAP теоремы строится очень просто. Рассматривается сеть из двух узлов G1 и G2, между которыми пропала связь. В узел G1 идет запрос на запись, а затем в G2 на чтение. Если выполняется доступность, то будет получен ответ на запрос чтения, но получены будут старые данные, так как между узлами нет связи (не согласованные данные). То есть, либо свойство доступности не выполняется, либо согласованности.

Далее, авторы утверждают, что все же наши сети не совсем асинхронные и рассматривают менее пуританскую модель сети. И почти так же доказывается CAP теорема для частично-синхронной сети.

Частично-синхронная сеть - это модель сети, где каждый узел имеет синхронизированные часы, которые могут показывать разное время, но увеличивают (переключают) время одновременно. То есть каждый узел может узнать сколько времени прошло от одного события до другого и на всех узлах эта величина будет одинаковой. Также каждое сообщение или доставляется за определенное время Tmsg, либо теряется. А каждый узел обрабатывает каждое сообщение за время Tlocal.

Еще в статье обсуждаются компромиссы: либо выполняются два их трех требований, либо смягчаются требования.

Что инженеры?

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

Но если он пытается построить систему, удовлетворяющую условиям в смысле Брювера, но не в определении второй статьи, то это вполне может оказаться возможным. Так как Брювер не формализовал свое утверждение. То есть нельзя говорить, что CAP теорема доказана в том виде в котором ее высказал Брювер. 

Например, третье требование (разделение сети) в этой статье слишком строгое.  Действительно, если в сети теряется произвольное число пакетов, то сложно требовать от нее вообще какой-либо работы. Кстати, авторитет в строительстве баз данных Стоунбрейкер считает, что разделение сети происходит не чаще других ошибок.

Третье требование могло бы быть сформулировано вероятностно. Например, что вероятность отказа - функция от количества потерянных сообщений среди n подряд идущих во всей системе. И если эта функция O(min[1, 1 / e^(n/2)]), тогда системе устойчива к разделению сети. Где n - число узлов в системе. И это тоже будет формализацией теоремы Брювера.

То есть не доказано, что нельзя создать систему, в которой выполняются требования CA, а требование P выполняется с большой долей вероятности. А если построить такую систему, то можно будет забыть про CAP теорему.

Также CAP тезис может быть неверным в другой модели сети, отличной от сформулированных во второй статье.

Итог

Инженеры часто говорят, что CAP теорема доказана в том смысле, в котором ее сформулировал Брювер, но формализована и доказана немного другая теорема.

Доказанная же теорема, на мой взгляд, сформулирована так, как удобно математикам доказывать ее правоту, но не отражает реального положения дел в прикладном смысле. И не исключена возможность систем, которые в каком-то смысле опровергают исходный тезис Брювера.

Кстати, в следующем посте я расскажу об одной очень интересной распределенной системе.