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

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

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

53

 

: ?

1

1

1

, |

( ( ))

0 ( )

,

, , , , , ,

, , , , , ,

g c x

i

i

k

i

n

i

n

l

l

g len c k

c v v

l

l

l

l

l

l

           

 

         

(2)

где

1

:

x v

   

и

2

:

k

c v v

     

.

2.2. Отправка значения

 

v dom c

по каналу

:

c

 

: !

1

1

1

, |

( ( ))

( ) ( )

,

, , , , , ,

, , , , , ,

g c v

i

i

k

i

n

i

n

l

l

g len c k cap c

c v v

l

l

l

l

l

l

           

         

(3)

где

1 2

:

.

k

c v v v v

    

Разработка моделей протоколов когерентности на языке

Promela

и опре-

деление ограничений для них.

Вопрос построения формальных моделей про-

токолов когерентности изучен в литературе недостаточно. Здесь использована

математическая модель протоколов когерентности в виде канальной системы, и

на основе практики верификации системы «Эльбрус-4С» определена структура

отдельных графов программ и изложены ограничения на используемые опера-

торы, выполнение которых необходимо для работы предлагаемого метода.

Рассмотрены протоколы когерентности, в которых исполнение запросов

происходит под управлением координатора. В микропроцессорах с архитекту-

рой «Эльбрус» координатором является системный коммутатор процессора, к

памяти которого происходит обращение (

home

-процессора).

В качестве математической модели протокола когерентности будем исполь-

зовать канальную систему

0

1

[

|

],

n

CS PG PG PG

где

0

PG

— граф программы,

соответствующий системному коммутатору

home

-процессора;

1

, ,

n

PG PG

идентичные графы программы, соответствующие контроллерам кэш-строки,

находящимся в кэшах верифицируемой системы. Каждый граф программы

определен над парой

,

i

i

Var Chan

так, что множества

i

Var

и

i

Chan

могут пере-

секаться. При этом

0

0

,

.

i

i

i n

i n

Var

Var Cha

Chan

n

 

 

Среди переменных из

Var

выделим множество подмножеств

| 0,

,

i

Vstate Var i

n

  

переменных, описывающих состояние процессов

,0

.

i

PG i n

 

При этом

0

.

i

i n

Vstate

 

 

Примерами переменных, входящих в

это подмножество, являются локальные переменные процесса

;

i

PG

переменная,

хранящая состояние кэш-строки в таком кэш-контроллере; переменная, храня-

щая признак получения ответа на снуп-запрос от процесса

.

i

PG

Определим ограничения на структуру графов

, 0

.

i

PG i n

 

Протоколы когерентности обладают свойством, согласно которому в один

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

В работе системного коммутатора

home

-процессора можно выделить последова-

тельность этапов, например, получение исходного запроса и его анализ, рассылка

когерентных и других служебных запросов по результатам анализа, сбор коге-