Проблемы параметризованной верификации протоколов когерентности памяти
7
соответствующая информация (множество достижимых состояний)
получается путем проверки абстрактных моделей. Тем не менее, объ-
ем ручной работы по введению лемм остается существенным. Метод
был применен для верификации протокола FLASH.
Метод CMP.
В [5] предлагается метод, базирующийся на комби-
нации model checking и доказательства теорем, в частности, основан-
ный на идеях из [20]. Автор работы [21] формализует описание этого
метода, а также доказывает его корректность.
Метод [5], получивший название CMP (по фамилиям авторов —
Chou, Mannava, Park), принимает на вход описание симметричного
протокола для
N
процессоров, отношение переходов которого задано
с помощью набора правил (rules). Правило является защищенной ко-
мандой (guarded command), условие которой (защита) определяет,
будут ли выполняться действия, отраженные в команде.
Метод CMP основан на композиционных рассуждениях и состоит
из двух основных шагов: получения абстрактной модели (abstraction)
и ее уточнения (strengthening), которые итеративно применяются к
описанию протокола. Пусть задано свойство относительно двух про-
цессов
i
и
j
, которое должно выполняться на модели. Метод строит
абстрактную модель, в которой сохраняется описание двух процессов
(например, 1 и 2), а описание остальных процессов заменяется неде-
терминированным процессом Other. Такая замена правомерна, по-
скольку в симметричной системе истинность свойства для процессов 1,
2 подразумевает его истинность и для любой другой пары процессов.
Процедура абстракции может быть следующей. Каждое условие в
коде модели, затрагивающее процессоры 3, ...,
N
, заменяется на true,
false или недетерминированное булево значение. Каждое присваива-
ние переменных, соответствующих процессорам 3, ...,
N
, удаляется.
Абстракция свойства осуществляется похожим образом; любое усло-
вие, в которое входят процессоры 3, ...,
N
, заменяется на true, false
или недетерминированное булево значение.
Получаемая абстрактная модель является очень грубой из-за от-
сутствия ограничений на поведение процесса Other, и проверка вы-
полнения свойств на этой модели будет сопровождаться ложными
контрпримерами. Для устранения таких контрпримеров метод требует
от пользователя введения лемм (non-interference lemmas), или инвари-
антов. Инварианты представляют собой выражения, сформулирован-
ные в терминах переменных модели протокола. По результатам анали-
за трассы контрпримера, предоставленной инструментальным сред-
ством проверки моделей, определяется правило абстрактной модели,
вызвавшее ложный переход. Условия, отраженные в леммах, добав-
ляются в защиту найденного правила, тем самым ограничивая поведе-
ние процесса Other. Данный процесс повторяется итеративно, пока не
