4501
правка
Линеаризуемость: различия между версиями
Перейти к навигации
Перейти к поиску
→Нотация
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 24: | Строка 24: | ||
История H определяет (нерефлексивный) частичный порядок <math>\to_H</math> для вызовов ее методов: | История 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 содержит вызовы методов | Пусть 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 является линеаризуемой, если она может быть расширена (путем добавления некоторого, возможно, нулевого количества событий ответа) до истории | '''Определение 1'''. История H является ''линеаризуемой'', если она может быть расширена (путем добавления некоторого, возможно, нулевого количества событий ответа) до истории H' такой, что: | ||
• L1 complete( | • (L1) complete(H') эквивалентна легальной последовательной истории S; | ||
• L2 Если вызов метода | • (L2) Если вызов метода <math>m_0</math> предшествует вызову метода <math>m_1</math> в H, то то же самое верно и в S. | ||
S называется линеаризацией H. (У одной истории может быть несколько линеаризаций). Неформально, расширение H до | S называется ''линеаризацией'' H. (У одной истории может быть несколько линеаризаций). Неформально, расширение H до H' отражает идею о том, что некоторые ожидающие вызовы могут произвести эффект, даже если их ответы еще не были возвращены вызывающему. | ||
== Основные результаты == | == Основные результаты == | ||