Линеаризуемость

Линеаризуемость - условие корректности для параллельных объектов, формально определённое Морисом Херлихи и Дженнет Винг в 1990 году. Мартин Клеппманн называет формальное определение не самым простым для восприятия и неформально формулирует основную мысль please-stop-calling-databases-cp-or-ap:

Если операция B началась после успешного завершения операции A, то операция B должна видеть систему в том же состоянии, в каком она была по завершении операции A, или в более новом.

Именно это означает "consistency" в теореме CAP. К букве C в ACID это отношения не имеет.

Что она запрещает

Пример Клеппманна - финал чемпионата мира 2014 года. Алиса и Боб сидят в одной комнате. Как только объявляют итоговый счёт, Алиса обновляет страницу, видит результат и говорит Бобу. Боб тоже обновляет, его запрос попадает на отстающую реплику, и телефон показывает, что матч ещё идёт. Если бы они обновили страницу одновременно, разные ответы никого бы не удивили: никто из них точно не знает, когда именно сервер обработал каждый запрос. Но Боб отправил свой запрос уже после того, как услышал Алису, поэтому он ожидает результат не старше её, и устаревший ответ нарушает линеаризуемость.

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

Чем приходится платить

Чтобы множество копий выглядело как одна, нужна координация, а она обходится дорого. Самый наглядный пример Клеппманна: даже CPU не даёт линеаризуемого доступа к локальной RAM. На современных процессорах для этого требуется явная инструкция барьера памяти (за деталями он отсылает к модели x86-TSO авторства Сьюэлла и коллег). Даже проверка того, линеаризуема ли система, сложна; он указывает на инструмент проверки Knossos Кайла Кингсбери.

Поэтому системы намеренно от неё отказываются. Базы данных со snapshot isolation или MVCC сознательно нелинеаризуемы, потому что обеспечение линеаризуемости снизило бы возможный уровень параллелизма. ZooKeeper отдаёт чтения с того сервера, к которому подключён клиент: это быстро и нелинеаризуемо, но позволяет клиенту вызвать sync перед чтением, чтобы получить линеаризуемое чтение ценой производительности. При сетевом разделении вступает в силу аргумент CAP: реплицированная система должна либо пожертвовать линеаризуемостью, либо перестать отвечать на одной из сторон разделения.

Чем она не является

Сериализуемость - это гарантия относительно транзакций, а линеаризуемость - гарантия свежести отдельных операций; ни одна из них не влечёт за собой другую. Пример Клеппманна - serializable snapshot isolation в PostgreSQL, которая даёт сериализуемость, но не линеаризуемость. Кворумные чтения и записи с R + W > N иногда называют линеаризуемыми, но он предостерегает от того, чтобы полагаться на это: нестрогие кворумы (sloppy quorums) и read repair создают пограничные случаи, нарушающие условие кворума. Сам по себе лежащий в основе протокол консенсуса тоже не делает чтения линеаризуемыми - именно так обстоят дела в ZooKeeper.

Как её получают на практике

Системы, которым она нужна, направляют операции через механизм, фиксирующий их порядок. В meerkat-introduction линеаризуемость стоит на первом месте среди требований Cloudflare - так авторы сервисов могут рассуждать о кластере точно так же, как о локальной памяти в одном потоке. Meerkat пропускает чтения через свой лог консенсуса: реплика, предлагающая чтение в слоте, для которого уже принята запись, вынуждена узнать об этой записи и заново предложить чтение после неё, а реплика, которая не может связаться с большинством, завершает чтение ошибкой вместо отдачи устаревших данных. Там же отмечается, что Raft обеспечивает линеаризуемые чтения с лидера с помощью lease-механизма. Сами алгоритмы описаны в distributed-consensus.

На одной машине вопрос сводится к моделям памяти. В shared-memory-consistency-causality конструируется намеренно неудобный многопроцессорный компьютер, чтобы выяснить, какой порядок должны гарантировать атомарные инструкции. Спецификация cobaltc определяет отношение happens-before для своих потоков и прямо указывает, что это отношение не требует машинного барьера памяти для каждого ребра упорядочивания. art-of-multiprocessor-programming - классический учебник по линеаризуемости для параллельных структур данных.

Связи

• stop-calling-databases-cp-or-ap - аргументация Клеппманна о том, что CP и AP некорректно описывают реальные базы данных, основанная на строгости требования линеаризуемости в CAP
• ability-guarantee-tradeoff - линеаризуемость как гарантия, за которую платят параллелизмом или задержкой