Метод построения абстрактных моделей, используемых для верификации протоколов когерентности кэш-памяти масштабируемых систем

Метод построения абстрактных моделей, используемых для верификации протоколов…

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1

няется истиной. Если





2,1 2,2

C C c c





то

остается неизменным, иначе

заменяется истиной.

Абстрактные преобразования элементов множеств

Comm

Преобразо-

вания коммуникационных действий можно проводить различными способами.

Так, можно удалять только те операторы извлечения сообщений и соответству-

ющие им операторы отправки сообщений, которые не изменяют элементов

множества

Однако для возможности проведения верификации на практи-

ке необходимо ограничивать емкость каналов и их число небольшими значени-

ями (3–4), что приводит к удалению некоторых операторов, изменяющих состо-

яние переменных из множества

Соответственно, преобразование коммуникационных действий исходит из

следующих соображений. Если оператор приема сообщения не изменяет помет-

ку состояния, то его можно удалить, как и соответствующее множество опера-

торов отправки сообщений. Если удаляется оператор отправки сообщения,

такой, что соответствующий ему оператор приема сообщения изменяет помет-

ку, то необходимы дополнительные меры. Разработанные преобразования и

принятые меры приведены в таблице.

Преобразование коммуникационных действий

Оператор в исходной модели

Оператор в абстрактной модели

Для

c C



 





c v v dom c



! ,

c v

если оператор находится в графах

;



если оператор находится в графе

 





c x x Var dom x dom c





Недетерминированный выбор

Для

c C



 





c v v dom c



! ,

c v

если

2,1

c c



или

2,2

;

c c





если





2 2,1 2,2

c C c c



 





c x x Var dom x dom c





? ,

c x

если

2,1

c c



или

2,2

;

c c





если





2 2,1 2,2

c C c c



Для

c C



 





c v v dom c



c v

 





c x x Var dom x dom c





c x

Рассмотрим замену недетерминированным выбором. Если оператор

atomic

{

guard_abs -> c?x;

} находится в

то он заменяется оператором неде-

терминированного выбора

:: atomic { guard_abs -> c?x; }

:: atomic { m.opc = opc

;

m.id

= ABS; }

…

:: atomic { m.opc = opc

;

m.id

= ABS; }

fi;