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

13 / 18

Метод построения абстрактных моделей, используемых для верификации протоколов…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1 61
действием ! c v и имеет вид   Α ,
i    для некоторого 1 . i m   Рассмотрим, как
  Α i  связан с .
i  Для случая отправки сообщения по каналу 1 c C множество
правил исходной системы  
1 |1 ,
concrete i Ruless rsc i n    где
 
: !
1
0 0
, | ( ( )) ( ) ( ) ... ,
, , , , , , , , , , , ,
g c v
i i k
i
i n i n
l l g len c k cap c c v v
rsc
l l l l l l

           

           
(6)
где  
1 2 : .
k c v v v v     
Множество правил абстрактной системы  
1 |1 2 ,
abstract i Ruless rsa i    где
    : !
1
0 3 0 3
, ( ) ( ) ( ) ...
, , , , , , , , , , , ,
abs g c v
i i abs abs abs abs abs abs l
i
i abs abs i abs abs
l l g len c l cap c c v v
rsa
l l l l l l 
           

             
где  
'
1 2 : ,
abs abs l c v v v v        2.
abs cap c 
В соответствии с преобразованиями абстракции отображение
1 1 1 : concrete abstract Transs Ruless Ruless  определено так, что  
1 ,
i i Transs rsc rsa
1, 2, i   
1 , 2.
i Transs rsc i    Следовательно,   Α ,   если соответствующая
метка порождена действиями ! c v процессов 1 2, , PG PG и  
Α    в противном
случае. Таким образом, переменная x может принимать только те значения из
множества , X которые были отправлены процессами 1 PG и 2 . PG
Все остальные случаи в абстрактной модели представлены оставшимися
элементами рассматриваемого множества правил, которые имеют вид
  : . : , . :
,
. : , . :
0 3 0 3
, | .
, , , , , , , , , , , ,
abs g x opc v x id ABS
i i abs abs abs
i j
x opc v x id ABS
i abs abs i abs abs
l l g
raa
l l l l l l
 
 
    

             


Здесь   :
abs abs x v     ; v принимает все возможные значения из
  . ,
abs dom x opc которые в исходной системе могут быть отправлены по каналу
c процессами , 2 .
r PG r n 
Мультиотображение 1 Transr определено следующим образом, как следует из
абстрактных преобразований. Пусть 0 ; i n   , t i если 0 2,i   3, t  если
2 . i n   Тогда  
1 ,
i t Transr rrc rra если значение 1 v было записано графом 1 PG
или графом 2 ; PG    
1 , 1 |1
i t j Transr rrc raa j S    , если значение 1 v не было за-
писано ни 1 PG , ни 2 . PG
Покажем, что, если посылка правила системы CS выполнима, то посылка
соответствующего правила системы abs CS также выполнима.
Случай а. Правило исходной системы — 1 .
i concrete rrc Rulesr Правило аб-
страктной системы — ,
t rra где , t i если 0 2,i   3, t  если 2 . i n  