7 / 18
Метод построения абстрактных моделей, используемых для верификации протоколов…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
55
2.
Множество каналов
2
2,1
2,
, ,
n
C c
c
емкостью
,
m
таких, что из кана-
ла
2,
, 1
,
i
c
i n
может извлекать сообщения только
,
i
PG
а отправлять сообщения
по этому каналу может только
0
.
PG
Примером канала из этого множества явля-
ется канал, по которому процесс, представляющий системный коммутатор
home
-
процессора, передает когерентный запрос процессу, представляющему кэш-
контроллер.
3. Множество каналов
3
,
C
по которым может отправлять сообщения только
один процесс в специфицированное «время» в ходе выполнения запроса. Для
каналов этого множества характерно соответствие каждому оператору приема
сообщения ровно одного оператора отправки сообщения. Примером канала из
этого множества является канал, по которому процесс-запросчик передает под-
тверждение о завершении операции процессу-координатору.
Сообщения, передаваемые по каналам, являются парами
,
,
m opc id
где
opc
не является номером процесса;
0, ,
id
n
— номер процесса
(например, идентификатор отправителя сообщения). Для обращения к первому
и второму элементам пары
m
запишем
.
m opc
и
. .
m id
Синтез совокупности преобразований, приводящих к получению аб-
страктной модели.
Проведем синтез совокупности преобразований.
Абстрактная модель протоколов когерентности.
Проверяемые свойства
протокола затрагивают не более двух кэшей. Поскольку все кэш-контроллеры
идентичны и взаимозаменяемы, не имеет значения, какие именно два индекса
графов
1
, ,
n
PG PG
рассматривать. Поэтому без потери общности будем пола-
гать, что рассматриваются графы
1
,
PG
2
,
PG
и все проверяемые свойства сфор-
мулированы только относительно части системы, определяемой этими графами.
В отсутствие свойств относительно графов
3
, ,
,
n
PG PG
с позиции графов
0 1 2
,
,
PG PG PG
конкретное значение индекса графов
3
, ,
n
PG PG
неважно.
Поэтому можем выполнить следующее консервативное преобразование си-
стемы
.
CS
Предполагается, что в исходной системе среди переменных
,
i
v Vstate
0
,
i n
хранящих информацию о других процессах, могут быть только перемен-
ные, хранящие номер процесса, т. е. переменные, областью определения которых
является множество
0,
,
.
n
В случае, когда полностью рассматривается только
состояние процессов
, 0 2,
i
PG i
важно сохранять точные значения лишь тогда,
когда это значение принадлежит множеству
0,1, 2 ;
все остальные значения не-
различимы и их можно представить некоторым абстрактным значением, не нахо-
дящимся в этом множестве. В связи с этим применим абстракцию типов данных.
Множества значений переменных
v Var
и каналов
c Chan
таких, что
0,
,
dom v
n
и
.
0,
,
,
dom c id
n
заменяются
0,1, 2,
abs
dom v
ABS
и
.
0,1, 2,
,
abs
dom c id
ABS
где
2
ABS
— некоторая константа. Для всех осталь-
ных случаев
,
abs
dom v dom v
abs
dom c
.
dom c
Далее под исходной систе-
мой будем понимать преобразованную таким способом систему
.
CS