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

5 / 18

Метод построения абстрактных моделей, используемых для верификации протоколов…
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-процессора можно выделить последова-
тельность этапов, например, получение исходного запроса и его анализ, рассылка
когерентных и других служебных запросов по результатам анализа, сбор коге-