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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

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

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

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

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

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

См. также[править | править код]

Примечания[править | править код]

Ссылки[править | править код]

  • 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].