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

Перейти к навигации Перейти к поиску
мНет описания правки
Строка 33: Строка 33:




'''Определение 1'''. История H является линеаризуемой, если она может быть расширена (путем добавления некоторого, возможно, нулевого количества событий реакции) до истории H0 такой, что:
'''Определение 1'''. История H является линеаризуемой, если она может быть расширена (путем добавления некоторого, возможно, нулевого количества событий ответа) до истории H0 такой, что:


• L1 complete(H0) эквивалентна легальной последовательной истории S;
• L1 complete(H0) эквивалентна легальной последовательной истории S;
Строка 58: Строка 58:


Оказывается, что ! является частичным порядком. Очевидно, что ! транзитивен. Осталось показать, что ! антирефлексивен: для всех x утверждение x ! x ложно.
Оказывается, что ! является частичным порядком. Очевидно, что ! транзитивен. Осталось показать, что ! антирефлексивен: для всех x утверждение x ! x ложно.


Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов m0...: mn, такие, что m0 ! m1 ! - - - -> mn;mn ! m0, и каждая пара непосредственно связана с некоторым !x или ! H.
Продолжим доказательство от противного. Если наше предположение неверно, то существуют вызовы методов m0...: mn, такие, что m0 ! m1 ! - - - -> mn;mn ! m0, и каждая пара непосредственно связана с некоторым !x или ! H.
Строка 64: Строка 63:
Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом x. Поскольку -x является полным порядком, должны существовать два вызова метода m,_i и mi такие, что mi -1!H mi и mi !x mj-\, что противоречит линеаризуемости x.
Выберем цикл, длина которого минимальна. Предположим, что все вызовы метода связаны с одним и тем же объектом x. Поскольку -x является полным порядком, должны существовать два вызова метода m,_i и mi такие, что mi -1!H mi и mi !x mj-\, что противоречит линеаризуемости x.


 
Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за 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.
Поэтому цикл должен включать вызовы методов как минимум двух объектов. Обозначим за 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>
Поскольку mn не является вызовом метода x, а mn ! m1, из этого следует, что mn !H m1. Но m1 !H m2 по построению, а так как !H транзитивно, то mn !H m2, что дает более короткий цикл m2... ; mn, что дает противоречие. <math>\square</math>
Строка 78: Строка 76:




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




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




Источник — http://pco.iis.nsk.su/wega/index.php/Линеаризуемость