4551
правка
Линеаризуемость: различия между версиями
Материал из WEGA
→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 73: | Строка 73: | ||
'''Свойство неблокируемости''' | '''Свойство неблокируемости''' | ||
Линеаризуемость является неблокирующим свойством: ожидающий | Линеаризуемость является ''неблокирующим'' свойством: ожидающий вызов полного метода никогда не должен ждать завершения другого ожидающего вызова. | ||
'''Теорема 2. Пусть inv(m) – вызов полного метода. Если | '''Теорема 2. Пусть inv(m) – вызов полного метода. Если <math>\langle x \; invP \rangle</math> является ожидающим вызовом в линеаризуемой истории H, то существует ответ <math>\langle xresP \rangle</math>, такой, что история <math>H \cdot \langle x \; resP \rangle</math> линеаризуема.''' | ||
Доказательство. Пусть S – любая линеаризация H. Если S включает ответ | Доказательство. Пусть S – любая линеаризация H. Если S включает ответ <math>\langle x \; resP \rangle</math> на <math>\langle x \; invP \rangle</math>, то доказательство тем самым завершается, так как S также является линеаризацией <math>H \cdot \langle x \; resP \rangle</math>. В противном случае <math>\langle x \; invP \rangle</math> также не встречается в S, поскольку линеаризации, по определению, не включают ожидающих вызовов. Поскольку метод является полным, существует ответ <math>\langle x \; resP \rangle</math> такой, что <math>S' = S \cdot \langle x \; invP \rangle \cdot \langle x \; resP \rangle</math> является легальным. S', однако, является линеаризацией <math>H \cdot \langle x \; resP \rangle</math>, и, следовательно, также является линеаризацией H. <math>\square</math> | ||
Из этой теоремы следует, что линеаризуемость сама по себе никогда не приводит к блокировке потока с ожидающим вызовом полного метода. Конечно, блокировки (или даже взаимоблокировки) могут возникать как артефакты конкретных реализаций процесса линеаризации, но они не присущи самому свойству корректности. Данная теорема утверждает, что линеаризуемость является подходящим условием корректности для систем, в которых важны параллелизм и ответ в реальном времени. Альтернативные условия корректности, такие как сериализуемость [ ], не обладают этим свойством неблокируемости. | Из этой теоремы следует, что линеаризуемость сама по себе никогда не приводит к блокировке потока с ожидающим вызовом полного метода. Конечно, блокировки (или даже взаимоблокировки) могут возникать как артефакты конкретных реализаций процесса линеаризации, но они не присущи самому свойству корректности. Данная теорема утверждает, что линеаризуемость является подходящим условием корректности для систем, в которых важны параллелизм и ответ в реальном времени. Альтернативные условия корректности, такие как сериализуемость [1], не обладают этим свойством неблокируемости. | ||
Свойство неблокируемости не исключает блокировку в ситуациях, когда она явно предполагается. Например, может быть разумным, чтобы поток, пытающийся произвести выгрузку из пустой очереди, блокировал ее, ожидая, пока другой поток не выгрузит элемент. Спецификация очереди отражает это намерение, делая спецификацию метода deq () частичной и оставляя его эффект неопределенным при применении к пустой очереди. Наиболее естественной параллельной интерпретацией частичной последовательной спецификации является простое ожидание, пока объект не достигнет состояния, в котором метод определен. | Свойство неблокируемости не исключает блокировку в ситуациях, когда она явно предполагается. Например, может быть разумным, чтобы поток, пытающийся произвести выгрузку из пустой очереди, блокировал ее, ожидая, пока другой поток не выгрузит элемент. Спецификация очереди отражает это намерение, делая спецификацию метода deq() частичной и оставляя его эффект неопределенным при применении к пустой очереди. Наиболее естественной параллельной интерпретацией частичной последовательной спецификации является простое ожидание, пока объект не достигнет состояния, в котором метод определен. | ||
