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

8 / 18

В.С. Буренков, С.Р. Иванов
56 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
В соответствии с предлагаемым методом после проведения абстракции ти-
пов данных осуществляется замена исходной модели 0 1 [ | ]
n CS PG PG PG 
моделью 0 1 2 3 [ | ],
abs CS PG PG PG PG в которой изначально графы , 0 3,
i PG i 
являются графами , 0 3,
i PG i  исходной системы . CS
Пометим множество состояний системы переходов  
abs abs TS TS CS и ис-
ходной системы так, чтобы пометка полностью отражала состояние графов
, 0 2,
i PG i  исходной системы  , TS CS а также состояние графов , 2,
i PG i 
непосредственно используемое при модификации состояния графов
, 0 2.
i PG i 
Сделаем пояснения. В графах программ , 2 ,
i PG i n  могут быть перемен-
ные 2 ,
i i n v Vstate
    которые непосредственно участвуют в изменении значе-
ний переменных из 0 2 .
i
i Vstate
   Обозначим множество таких переменных
через loc V , 2 .
loc i
i n V Vstate
    Значения таких переменных модифицируются
операциями извлечения сообщения из канала 1 , c C например,
// 2 message i
i n Vstate
   
coh_answers_chan ? message;
//   0 2 ack _ list i
i Vstate
    , если 1, 2
ack_list ] = false;
В ходе исполнения исходного запроса релевантны значения таких переменных
только одного процесса. Введем такое множество переменных ,
loca V что его эле-
менты всегда находятся во взаимно-однозначном соответствии с рассмотренными
локальными переменными того из процессов, который проводит модификацию
переменных из 0 2 i
i Vstate
   : loca i V Vstate для некоторого 2 . i n  
Следовательно, в качестве пометок состояний абстрактной  
abs TS и исход-
ной  TS систем будем использовать множество   ,
AP AP Cond V где AP V 
0 2 .
i loca
i Vstate V
 
  
Последующая модификация графов программ , 0 3,
i PG i  осуществляется
путем синтаксических преобразований, описанных ниже.
Абстрактные преобразования элементов множеств .
i Act Множество
выражений ограничим множеством  
, . Cond Var Chan Преобразования при-
сваиваний приведены ниже (символ  означает отсутствие действия).
1. Оператор в исходной модели     , . v val v Var val dom v  
2. Оператор в абстрактной модели 0,1,2 , если ;
i
i v val v Vstate
    , если 
2 .
i
i n v Vstate
   
Других операторов присваивания нет.
Преобразование выражений ( , ) ( , ) v c Cond V C осуществляется следующим
образом. Если 0,1,2 ,
i loc
i V Vstate V
    то v остается неизменным, иначе v заме-