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

4 / 18

В.С. Буренков, С.Р. Иванов
52 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
Канальная система. Такая система CS над   , Var Chan состоит из графов
программы i PG над   , ,
i Var Chan где 1 i n   и 1 .
i i n Var Var
    Обозначение
 
1 .
n CS PG PG 
В языке Promela возможны два типа взаимодействия между процессами с
помощью каналов: 1) синхронная передача сообщения через канал нулевой ем-
кости; 2) асинхронная передача сообщения через канал ненулевой емкости. При
разработке моделей протоколов когерентности нет необходимости использо-
вать синхронную передачу сообщений, поэтому далее такой тип взаимодей-
ствия рассматриваться не будет.
Семантика канальной системы формализуется посредством системы пере-
ходов. Пусть  
1 n CS PG PG  — канальная система над   , . Var Chan Состоя-
ния соответствующей системы переходов   TS CS являются кортежами вида
1 , , , , ,
n l l    где i l — состояние графа i PG ,   Eval Var  — текущая интер-
претация переменных;   Eval Chan  — интерпретация каналов.
Пусть  
1 n CS PG PG  — канальная система над   , Var Chan , и
 
0, 0, , , , , , ,
i i i i i i i PG Loc Act Effect Loc g   1 . i n  
Системой переходов  , TS CS соответствующей данной канальной системе,
называется шестерка    
, , , , , , TS CS S Act I AP L   где
     
1 ;
n S Loc Loc Eval Var Eval Chan    
 
0 ,
i
i n Act Act
       — специальный символ, представляющий все комму-
никационные действия, при которых происходит обмен данными; переход 
определяется правилами, представленными ниже:
    
           1 0 0, 0 0, { , , , , | 0 : , | ;
n i i i I l l i n l Loc g
  
    0 , ;
i
i n AP Loc Cond Var Chan
        
         
1 1 , , , , , , { , | , | }.
n n L l l l l g Cond Var Chan g
Отметим, что в зависимости от интересующих свойств, в качестве пометок
может быть использовано любое подмножество указанного множества . AP
Перечислим правила, определяющие отношение переходов  системы
  . TS CS
1. Интерливинг для i Act  :
  :
1 1
, |
,
, , , , , , , , , , , ,
g
i i
i n i n
l l g
l l l l l l


    
          
(1)
где   , . Effect    
2. Асинхронная передача сообщения для   , 0. c Chan cap c 
2.1. Получение значения по каналу c и присваивание его переменной x: