Линеаризуемость: различия между версиями

Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за m1 и m2 вызовы методов разных объектов (переиндексировав их при необходимости). Пусть x – объект, связанный с m1. Ни один из m 2... m n не может быть вызовом метода x. Утверждение справедливо для m2 по построению. Пусть mi – первый вызов метода в m3; mn, связанный с x. Поскольку m,_i и mi не связаны по ! x, они должны быть связаны по ! H, поэтому ответ m,_i предшествует вызову mi. Вызов m2 предшествует ответу m,_i, поскольку в противном случае mi -1!H m2, что дает более короткий цикл m2 ■ ■ : ; m,_i. Наконец, ответ m1 предшествует вызову m2, поскольку m1 !H m2 по построению. Отсюда следует, что ответ на m1 предшествует вызову mi, следовательно, m1 !H mi, что дает более короткий цикл m\,mi,... , mn.

Поскольку mn не является вызовом метода x, а mn ! m1, из этого следует, что mn !H m1. Но m1 !H m2 по построению, а так как !H транзитивно, то mn !H m2, что дает более короткий цикл m2... ; mn, что дает противоречие. <math>\square</math>

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

'''Теорема 2. Пусть inv(m) – вызов полного метода. Если hx invPi является ожидающим вызовом в линеаризуемой истории H, то существует ответ hxresPi, такой, что история H-(xresP) линеаризуема.'''

Доказательство. Пусть S – любая линеаризация H. Если S включает ответ hx resPi на hx invPi, то доказательство тем самым завершается, так как S также является линеаризацией H ■ (x resPi. В противном случае hx invPi также не встречается в S, поскольку линеаризации, по определению, не включают ожидающих вызовов. Поскольку метод является полным, существует ответ hx resPi такой, что S0 = S-{x invP ■ (x res Pi является легальным. S0, однако, является линеаризацией H ■ (x resPi, и, следовательно, также является линеаризацией H. <math>\square</math>

Из этой теоремы следует, что линеаризуемость сама по себе никогда не приводит к блокировке потока с ожидающим вызовом полного метода. Конечно, блокировки (или даже взаимоблокировки) могут возникать как артефакты конкретных реализаций процесса линеаризации, но они не присущи самому свойству корректности. Данная теорема утверждает, что линеаризуемость является подходящим условием корректности для систем, в которых важны параллелизм и ответ в реальном времени. Альтернативные условия корректности, такие как сериализуемость [ ], не обладают этим свойством неблокируемости.

Свойство неблокируемости не исключает блокировку в ситуациях, когда она явно предполагается. Например, может быть разумным, чтобы поток, пытающийся произвести выгрузку из пустой очереди, блокировал ее, ожидая, пока другой поток не выгрузит элемент. Спецификация очереди отражает это намерение, делая спецификацию метода deq () частичной и оставляя его эффект неопределенным при применении к пустой очереди. Наиболее естественной параллельной интерпретацией частичной последовательной спецификации является простое ожидание, пока объект не достигнет состояния, в котором метод определен.

Последовательная согласованность [ ] представляет собой более слабое условие корректности, в котором выполняется требование L1, но не L2: вызовы методов должны происходить по одному в некотором последовательном порядке, но неперекрываюмиеся вызовы могут быть переупорядочены. Любая линеаризуемая история является последовательно согласованной, однако обратное неверно. Последовательная согласованность допускает больший параллелизм, но это не локальное свойство: система, состоящая из множества последовательно согласованных объектов, вовсе не обязательно сама является последовательно согласованной.

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

Ни сериализуемость, ни строгая сериализуемость не являются локальными свойствами. Если разные объекты сериализуют транзакции в разном порядке, то не может быть порядка сериализации, общего для всех объектов. Сериализуемость и строгая сериализуемость являются блокирующими свойствами: при определенных обстоятельствах транзакция может быть не в состоянии завершить ожидающий метод, не нарушая сериализуемости. Если несколько транзакций блокируют друг друга, возникает ситуация взаимоблокировки. Для таких транзакций необходимо выполнить откат и перезапуск, что подразумевает наличие дополнительных механизмов для этой цели.

Понятие линеаризуемости было предложено Херлихи и Винг [3], последовательной согласованности – Лампортом [4], а сериализуемости Эсвараном и коллегами [1].