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

Выполнение параллельной системы моделируется ''историей'' – конечной последовательностью событий ''вызова'' метода и ''ответа'' на него. ''Подыстория'' истории H представляет собой подпоследовательность событий H. Вызов метода записывается как <math> \langle x.m(a^*)A \rangle </math>, где <math>x</math> – объект, <math>m</math> – имя метода, <math>a^*</math> – последовательность аргументов, а <math>A</math> – поток. Ответ метода записывается как <math> \langle x: t(r^*)A \rangle </math>, где <math>t</math> – условие завершения, а <math>r^*</math> – последовательность значений результата.

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