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

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

'''Теорема 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 () частичной и оставляя его эффект неопределенным при применении к пустой очереди. Наиболее естественной параллельной интерпретацией частичной последовательной спецификации является простое ожидание, пока объект не достигнет состояния, в котором метод определен.