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

В.С. Буренков, С.Р. Иванов

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1

Решаемую в этой работе задачу можно сформулировать следующим образом.

Дано неформальное описание протокола когерентности наподобие

MOSI

[5], обес-

печивающего согласованность данных в

блоках кэш-памяти, каждый из которых

принадлежит отдельному процессорному ядру. Сформулирована спецификация

протокола когерентности в виде множества свойств-инвариантов, запрещающих

определенные комбинации состояний кэш-строки в кэшах системы. Необходимо

разработать метод, проверяющий соответствие протокола данному множеству

свойств при любом числе





кэшей.

Синтез математической модели для представления протоколов когерент-

ности.

Проведем синтез математической модели.

Модель протоколов когерентности.

Язык описания моделей

Promela

предла-

гает абстракции, представляющие группы устройств, работающих в соответствии с

протоколом когерентности (

процессы

, являющиеся конечными автоматами), и их

асинхронное взаимодействие (

каналы

, являющиеся

FIFO-

очередями). В связи с

этим математическая модель протоколов когерентности, используемая в настоя-

щей работе, основана на формальной семантике

Promela

-моделей и базируется на

модели, применяемой в работе [6].

Модель состоит из нескольких уровней.

Promela

-процессам соответствуют

графы программ. Асинхронная композиция графов программ описывается ка-

нальной системой. Путем «развертывания» канальной системы получается си-

стема переходов — стандартная модель аппаратных и программных систем.

Система переходов.

Системой переходов

называется шестерка





, , ,

, ,

TS S Act

I AP L





где

— множество состояний;

Act

— множество дей-

ствий;

S Act S

  

— отношение переходов;

I S



— множество начальных

состояний;

— множество атомарных высказываний;

L S



— функция

пометок. Для краткости под обозначением

s s





будем понимать





, ,

s s

 

Если осуществляемое действие в таком контексте неважно, запишем

s s

 

Граф программы.

Поведение процессов описывается с помощью операто-

ров языка

Promela

. Множество всех переменных модели будем обозначать через

Var

множество каналов модели —

Chan

Обозначим через

 

dom x

тип переменной

а через

 

dom c

— тип перемен-

ных, которые могут быть переданы через канал

Емкость канала

— максималь-

ное число сообщений, которое он способен хранить, — обозначим через

 

cap c

Интерпретацией



переменных называется отображение, ставящее в соот-

ветствие каждой переменной

v Var



значение

 

v dom v

 

Через





v r

 

обозначим интерпретацию переменных, присваивающую значение

перемен-

ной

и оставляющую все остальные переменные неизменными. Обозначим

через





Eval Var

множество интерпретаций переменных.

Интерпретация



каналов — отображение, ставящее в соответствие каждо-

му каналу

c Chan



последовательность

 

c dom c

 

такую, что

 





len c

 

 

cap c



где

 

len



— длина последовательности;

— звезда Клини.

Запись