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

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




Ответ ''соответствует'' обращению, если имена их объектов и потоков согласуются. ''Вызовом метода'' является пара, состоящая из обращения и следующего подходящего ответа. Обращение ''ожидает'' своего завершения в истории, если за ним не следует подходящий ответ. Если H – история, то ''complete''(H) – это подпоследовательность H, состоящая из всех соответствующих обращений и ответов. История H является ''последовательной'', если первым событием H является обращение, а за каждым обращением (кроме, возможно, последнего) немедленно следует подходящий ответ.
Ответ ''соответствует'' обращению, если имена их объектов и потоков согласуются. ''Вызовом метода'' является пара, состоящая из обращения и следующего подходящего ответа. Обращение ''ожидает'' своего завершения в истории, если за ним не следует соответствующий ответ. Если H – история, то ''complete''(H) – это подпоследовательность H, состоящая из всех соответствующих обращений и ответов. История H является ''последовательной'', если первым событием H является обращение, а за каждым обращением (кроме, возможно, последнего) немедленно следует соответствующий ответ.




Пусть H – история. ''Потоковая подыстория'' H|P представляет собой подпоследовательность событий в H с именем потока P. ''Объектовая подыстория'' H|x аналогично определяется для объекта x. Две истории H и H' ''эквивалентны'', если для каждого потока A выполняется H|A = H'|A. История H ''хорошо согласована'', если каждая потоковая подыстория H|A из H является последовательной. Обратите внимание, что подыстории потоков хорошо согласованной истории всегда последовательны, однако подыстории объектов не обязательно должны быть последовательными.
Пусть H – история. ''Потоковая подыстория'' H|P представляет собой подпоследовательность событий в H с именем потока P. ''Объектовая подыстория'' H|x аналогично определяется для объекта x. Две истории H и H' ''эквивалентны'', если для каждого потока A выполняется H|A = H'|A. История H ''хорошо согласована'', если каждая потоковая подыстория H|A из H является последовательной. Обратите внимание, что потоковые подыстории хорошо согласованной истории всегда последовательны, однако объектовые подыстории не обязательно должны быть последовательными.




Строка 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 является полным.
История H определяет (нерефлексивный) частичный порядок <math>\to_H</math> для вызовов ее методов: <math>m_0 \to_H m_1</math>, если событие получения результата <math>m_0</math> происходит раньше события обращения к <math>m_1</math>. Если история H является последовательной, то порядок H является полным.