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

Линеаризуемость — это модель консистентности данных в распределённых системах и системах с общей памятью, которая гарантирует, что каждая операция (например, чтение или запись) становится видимой для всех остальных процессов системы в единый момент времени между её вызовом и завершением. Линеаризуемость является одной из самых строгих моделей согласованности, обеспечивающей поведение системы, эквивалентное последовательному выполнению операций на одном ядре (single-core sequential execution). Она впервые была формально определена Морисом Херлихи и Джингом Вингом в 1987 году.

История

Понятие линеаризуемости возникло в контексте развития теории распределённых вычислений и параллельных систем. В 1980-х годах с ростом популярности многопроцессорных архитектур и распределённых баз данных возникла необходимость в формальных критериях, позволяющих оценить корректность работы систем с одновременным доступом. До этого использовались модели последовательной консистентности (sequential consistency), предложенной Лесли Лампортом в 1979 году, которая требовала, чтобы результаты операций были такими же, как если бы они выполнялись в некотором порядке, но не гарантировала «мгновенности» видимости изменений.

В 1987 году Морис Херлихи и Джинг Винг опубликовали работу «Линеаризуемость: модель корректности для параллельных объектов» (Linearizability: A Correctness Condition for Concurrent Objects), в которой ввели строгое определение, основанное на понятии «истории» (history) — последовательности вызовов и возвратов операций. Линеаризуемость стала стандартом для верификации алгоритмов синхронизации и распределённых структур данных.

Формальное определение

Линеаризуемость определяется через историю выполнения системы, которая представляет собой множество событий, каждое из которых состоит из вызова операции (invocation) и возврата результата (response). Для каждой операции задаётся временной интервал между её началом и завершением. История считается линеаризуемой, если:

1. Существует последовательный порядок (линеаризация) всех завершённых операций, который согласуется с порядком их выполнения в реальном времени (то есть если операция A завершилась до начала операции B, то в линеаризации A должна предшествовать B).
2. Результаты операций в этом последовательном порядке соответствуют семантике используемого объекта (например, для регистра чтение возвращает последнее записанное значение).

Формально линеаризуемость требует, чтобы для любой истории можно было найти такую последовательность операций, которая:

• Сохраняет частичный порядок, заданный временными интервалами (non-overlapping интервалы не могут быть переставлены).
• Даёт тот же набор результатов, что и в исходной истории.

Свойства и отличия от других моделей

Линеаризуемость является локальным свойством: если каждый отдельный объект в системе линеаризуем, то вся система в целом также линеаризуема (свойство композициональности). Это отличает её от последовательной консистентности, которая не является композициональной.

Ключевые отличия линеаризуемости от других моделей согласованности:

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

Применение

Линеаризуемость широко используется в следующих областях:

Распределённые системы

В распределённых системах (например, в системах управления базами данных, распределённых файловых системах, блокчейнах) линеаризуемость обеспечивает согласованность данных при сбоях и параллельном доступе. Примеры систем, реализующих линеаризуемость:

• Apache ZooKeeper — распределённый координационный сервис, предоставляющий линеаризуемые операции над своими данными (znodes) через протокол Zab.
• etcd — распределённое хранилище ключ-значение, используемое в Kubernetes, реализует линеаризуемость через алгоритм консенсуса Raft.
• Google Spanner — глобально распределённая база данных, использующая TrueTime для обеспечения линеаризуемости на уровне транзакций.

Многопоточное программирование

В языках программирования (Java, C++, Go) линеаризуемость используется для построения потокобезопасных структур данных. Например, атомарные переменные (AtomicInteger в Java) гарантируют линеаризуемость операций чтения-записи. Блокировки (мьютексы, семафоры) также обеспечивают линеаризуемость критических секций.

Верификация и тестирование

Линеаризуемость является ключевым критерием при тестировании параллельных алгоритмов. Инструменты, такие как Lincheck (для Kotlin/Java) или TLA+ (формальная спецификация), позволяют проверять, удовлетворяет ли реализация заданной структуры данных условиям линеаризуемости.

Критика и ограничения

Несмотря на свою строгость, линеаризуемость имеет ряд недостатков:

• Производительность: обеспечение линеаризуемости требует синхронизации и обмена сообщениями между узлами, что увеличивает задержки и снижает пропускную способность. В распределённых системах это может приводить к значительным накладным расходам, особенно при высокой нагрузке.
• Сложность реализации: для достижения линеаризуемости в распределённой среде необходим алгоритм консенсуса (например, Paxos, Raft), который сам по себе сложен в реализации и отладке.
• Неприменимость для некоторых задач: в системах, где допустима временная несогласованность (например, в социальных сетях, кэширующих прокси), линеаризуемость избыточна и может быть заменена более слабыми моделями (причинная согласованность, eventual consistency).

Интересные факты

• Линеаризуемость является частным случаем более общего понятия «строгой согласованности» (strict consistency), которая требует, чтобы любая операция чтения возвращала результат последней записи в реальном времени. Однако строгая согласованность не учитывает временные интервалы операций — она предполагает, что запись становится видимой мгновенно, что невозможно в реальных системах. Линеаризуемость же учитывает задержки.
• В 2015 году группа исследователей из Microsoft и ETH Zurich доказала, что линеаризуемость не может быть реализована в асинхронных распределённых системах без использования синхронных предположений (например, часов или алгоритмов консенсуса). Это следует из теоремы FLP (Fischer, Lynch, Paterson), которая утверждает, что в асинхронной системе с возможностью сбоев невозможно достичь консенсуса.
• Термин «линеаризуемость» иногда путают с «линейностью» (linearizability) — последнее является англицизмом, но в русскоязычной литературе принято использовать именно «линеаризуемость».

Источники

• Herlihy, M., Wing, J. M. (1987). «Linearizability: A Correctness Condition for Concurrent Objects». ACM Transactions on Programming Languages and Systems.
• Lamport, L. (1979). «How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs». IEEE Transactions on Computers.
• Attiya, H., Welch, J. (2004). «Distributed Computing: Fundamentals, Simulations, and Advanced Topics». Wiley.
• Lynch, N. (1996). «Distributed Algorithms». Morgan Kaufmann.
• Официальная документация Apache ZooKeeper и etcd.