Previous Page  7 / 18 Next Page
Information
Show Menu
Previous Page 7 / 18 Next Page
Page Background

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

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