6 / 18
В.С. Буренков, С.Р. Иванов
54
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
рентных ответов и подтверждений. Получение сообщений от других устройств
возможно только на определенных этапах. В связи с этим алгоритм работы си-
стемного коммутатора удобно представить в виде
Promela
-процесса, в котором
отношение предыдущий–следующий между операторами представляется есте-
ственным образом. В коде такие операторы располагаются друг за другом.
Защищенные команды, которыми помечены ребра графа
0
,
PG
строятся так,
что их защиты могут являться:
– логическими утверждениями относительно переменных
0
\
i n
v Var
,
i
Vstate
причем значение этих переменных получается либо непосредственно пу-
тем исполнения операции извлечения из канала, либо в ходе анализа извлеченного
со-общения;
–
логическими утверждениями относительно переменных
,
i
v Vstate
1
,
i n
значение которых устанавливается в процессе анализа принятых гра-
фом сообщений.
Работа кэш-контроллеров осуществляется по-другому. С одной стороны,
можно выделить ряд этапов, например, отправка исходного запроса, смена со-
стояния на переходное, прием снуп-запросов и других служебных запросов,
прием когерентных ответов, смена переходного состояния на основное. С дру-
гой стороны, относительный порядок осуществления таких этапов зачастую не
фиксирован, и одни и те же сообщения от других устройств могут обрабаты-
ваться в различных состояниях кэш-контроллера. В связи с этим структуру
процессов, представляющих кэш-контроллеры, удобно представить в виде бес-
конечного
do
-цикла из защищенных команд.
Защита команды графа
, 1
,
i
PG i n
может быть логическим утверждением
,
.
i
i
e Cond Var Chan
Предполагается использование логических утверждений
относительно каналов для возможности неблокирующего опроса состояния ка-
налов. Например, если действие команды включает в себя получение сообщения
по каналу
,
c
и это действие не должно быть заблокировано, то в защиту с по-
мощью конъюнкции добавляется условие
.
nempty c
Также любая защита мо-
жет являться тавтологией.
Оператор извлечения сообщения из канала
с
в графе
, 0
,
i
PG i n
имеет
вид
? ,
c x
где
\
.
i
j
j
x Var
Vstate
Множество каналов модели представлено тремя подмножествами.
1. Множество каналов
1
C
емкостью
,
n
в которые могут отправлять сообще-
ния графы
, 1
.
i
PG i n
Извлекать сообщения может только один процесс
, 0
,
i
PG i n
на определенном этапе выполнения запроса. Примеры таких ка-
налов: канал, посредством которого процессы, представляющие кэш-
контроллеры, передают исходные запросы процессу, представляющему систем-
ный коммутатор
home
-процессора; канал, по которому некоторому процессу
передаются когерентные ответы.