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

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

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

Последовательная спецификация объекта представляет собой префиксно-замкнутое множество последовательных историй объекта, которое определяет легальные истории этого объекта. Последовательная история H является легальной, если каждая подыстория объекта легальна. Метод является полным, если он определен для каждого состояния объекта, в противном случае он является частичным. (Например, метод deq(), который блокирует пустую очередь, является частичным, а метод, отбрасывающий исключение – полным).

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