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

Перейти к навигации Перейти к поиску
Строка 24: Строка 24:




История H определяет (нерефлексивный) частичный порядок <math>\to_H</math> для вызовов ее методов: m0 ! H m1, если событие результата m0 происходит раньше события вызова m1. Если история H является последовательной, то порядок H является полным.
История H определяет (нерефлексивный) частичный порядок <math>\to_H</math> для вызовов ее методов: <math>m_0 \to_H m_1</math>, если событие получения результата <math>m_0</math> происходит раньше события вызова <math>m_1</math>. Если история H является последовательной, то порядок H является полным.




Пусть H – история, а x – объект, такой, что Hjx содержит вызовы методов m0 и m1. Вызов m0 !x m1, если m0 предшествует m1 в H|x. Заметим, что !x – полный порядок.
Пусть H – история, а x – объект, такой, что Hjx содержит вызовы методов <math>m_0</math> и <math>m_1</math>. Вызов <math>m_o \to_x m_1</math>, если <math>m_0</math> предшествует <math>m_1</math> в H|x. Заметим, что <math>\to_x</math> – полный порядок.




Строка 33: Строка 33:




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


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


• L2 Если вызов метода m0 предшествует вызову метода m1 в H, то то же самое верно и в S.
(L2) Если вызов метода <math>m_0</math> предшествует вызову метода <math>m_1</math> в H, то то же самое верно и в S.




S называется линеаризацией H. (У одной истории может быть несколько линеаризаций). Неформально, расширение H до H0 отражает идею о том, что некоторые ожидающие вызовы могут произвести эффект, даже если их ответы еще не были возвращены вызывающему.
S называется ''линеаризацией'' H. (У одной истории может быть несколько линеаризаций). Неформально, расширение H до H' отражает идею о том, что некоторые ожидающие вызовы могут произвести эффект, даже если их ответы еще не были возвращены вызывающему.


== Основные результаты ==
== Основные результаты ==
4551

правка

Навигация