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

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

Как было показано, линеаризуемость является локальным и неблокируемым свойством. Локальность означает, что если доказана линеаризуемость операций для нескольких программ в отдельности (или для операций работающих с разными объектами одной программы), то программы вместе (операции вместе) также будут линеаризуемы. В линеаризуемой программе запущенные операции не требуют для своего завершения запуска других операций. Это свойство неблокируемости. Кроме того, линеаризуемость упрощает доказательство свойств программ, которые используют линеаризуемые операции, так как поведение линеаризуемой программы сводится к последовательным выполнениям.

Свойство линеаризуемости во многом сходно с такими свойствами как сериализуемость (англ. serializability), атомарность, последовательная согласованность (англ. sequential consistency). В отличие от них, линеаризуемость предполагает наличие спецификации, тогда как эти свойства накладывают ограничения только на саму программу. В некоторых источниках термин атомарность используется как синоним линеаризуемости, в других же означает самолинеаризуемость.

Часто под неформальным понятием потоковой безопасности (англ. thread-safety) понимают именно линеаризуемость.

Понятие линеаризуемости впервые появилось в статье Херлихи и Винг 1987 года как модель согласованности для систем с объектной организацией общей памяти. В отличие от всех остальных систем, здесь программы не могут напрямую использовать общие переменные, а только через специальные функции-методы (операции). Для этих систем линеаризуемость совпадает со строгой согласованностью.

Задача проверки линеаризуемости — это частный случай задачи функционального тестирования, в которой проверяется, удовлетворяет ли программа функциональным требованиям к ней, заданным в виде спецификации. Но в отличие от общего случая, здесь спецификация требуется только для последовательных выполнений.

Ссылки

• M. Herlihy и J. Wing, «Axioms for Concurrent Objects», Труды 14-го ACM SIGACT-SIGPLAN симпозиума по Принципам языков программирования (Январь 1987), стр. 13-26 [1].
• M. Herlihy, «A methodology for implementing highly concurrent data structures», Труды ACM SIGPLAN симпозиума по Принципам и практике параллельного программирования, 1990, стр. 197—206 [2].
• M. Herlihy и J. Wing «Linearizability: a correctness condition for concurrent objects», Труды ACM по Языкам программирования и системам, 1990, стр. 463—492 [3].