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

12 / 18

В.С. Буренков, С.Р. Иванов
60 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
 
: ?
1
0 0
, | ( ( )) 0 ( ) ... ,
, , , , , , , , , , , ,
g c x
i i k
i
i n i n
l l g len c k c v v
rrc
l l l l l l 
           

            
(5)
где  
1 : x v     и  
2 : .
k c v v      
В процессе исполнения запроса только одно правило , 0 ,
i rrc i n   может по-
рождать переходы. В этих случаях изменение пометки обусловлено изменением
значения переменной x. Определим, какие значения может принимать x вследствие
применения правила , 0 .
i rrc i n   Для этого рассмотрим фрагмент вычисления
0 1 1 2 m m s s s    системы переходов . TS В таком случае переход 1 m m s s 
  получен
вследствие применения правила 1.
i concrete rrc Rulesr В моделях либо 0 i  (сообще-
ние извлекает процесс, представляющий системный коммутатор home-процессора),
либо 0 i  (сообщение извлекает процесс-запросчик с номером i ). Факт примене-
ния правила означает, что условие     0 len c k    выполнено. В свою очередь,
это позволяет записать   1 .
k c v v    Следовательно, из 1 , , m    находится k
членов, каждый из которых имеет вид .
i    Таким образом, после осуществления
перехода 1 ,
m m s s 
  переменная х будет принимать одно из значений из множества
X, всех ранее отправленных по каналу значений, причем 1 k v v является переста-
новкой этого множества.
Указанному множеству правил 1 concrete Rulesr в абстрактной модели соответ-
ствует множество правил  
1 , 1 , | 0 3,1 ,
abstract i i j Rulesr rra raa i j S      где
 
1 abs S dom c — число различных отправляемых значений в операторах
отправки сообщения, соответствующих операторам приема сообщения из
1 . c C Выбор правила из этого множества недетерминирован, т. е.
1 1 1 : concrete abstract Transr Rulesr Rulesr  — мультиотображение. Первый тип элемен-
тов этого множества имеет вид
  : ?
1
0 3 0 3
, | ( ( )) 0 ( ) ... ,
, , , , , , , , , , , ,
abs g c x
i i abs abs abs abs abs l
i
i abs abs i abs abs
l l g len c l c v v
rra
l l l l l l 
           

             
где  
1 :
abs abs x v     и  
'
2 :
abs abs l c v v      . Здесь l может принимать значе-
ния 1, 2.
Согласно абстрактным преобразованиям,
 
1 , 0 2,
i i Transr rrc rra i    
1 3 , 2 .
i Transr rrc rra i n  
Определим, какие значения при этом может принимать переменная x
в абстрактной модели в состоянии  
1 .
m f s  Рассмотрим фрагмент вычисле-
ния      
0 1 1 2 ( ) Α ( )Α Α ( )m m f s f s f s     системы переходов .
abs TS Здесь
   
Α : .
abs Act Act     Условие     0
abs len c l    может быть выполнено
только, если из    
1 Α , , Α m    было l членов, каждый из которых порожден