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