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

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

УДК 004.052.42

DOI: 10.18698/0236-3933-2017-1-49-66

МЕТОД ПОСТРОЕНИЯ АБСТРАКТНЫХ МОДЕЛЕЙ, ИСПОЛЬЗУЕМЫХ

ДЛЯ ВЕРИФИКАЦИИ ПРОТОКОЛОВ КОГЕРЕНТНОСТИ КЭШ-ПАМЯТИ

МАСШТАБИРУЕМЫХ СИСТЕМ

В.С. Буренков

vansburen@mail.ru

С.Р. Иванов

ivanovsr@bmstu.ru

МГТУ им. Н.Э. Баумана, Москва, Российская Федерация

Аннотация

Ключевые слова

Изложен новый подход к решению задачи верификации

протоколов когерентности кэш-памяти масштабируе-

мых микропроцессорных систем. Рассмотрена матема-

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

представляет собой отдельные группы устройств, рабо-

тающих в соответствии с протоколом, в виде графов

программ, а протокол в целом — в виде канальной

системы, из которой может быть получена и исследова-

на методом

Model checking

система переходов. Предло-

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

ности на языке

Promela

и сформулированы ограничения

на модели. Представлен метод построения абстрактных

моделей, позволяющий существенно уменьшить их

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

графов программ исходной модели, или на синтаксиче-

ских преобразованиях

Promela

-процессов. Приведено

математическое доказательство сохранения преобразо-

ваниями свойств-инвариантов. Результаты основаны на

практике верификации протокола сложной системы на

кристалле с архитектурой «Эльбрус»

Формальный метод, проверка

моделей, преобразование моделей,

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

кэш-памяти

Поступила в редакцию 19.04.2016

Введение.

Проблема верификации протоколов когерентности кэш-памяти яв-

ляется сложной и чрезвычайно актуальной в контексте проектирования много-

ядерных процессоров и многопроцессорных вычислительных систем с разделя-

емой памятью.

Не существует единого подхода к решению проблемы, способного адапти-

роваться к увеличению числа ядер в современных микропроцессорах. В насто-

ящей работе развиваются приведенные в статье [1] направления по разработке

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

масштабируемых систем. В основе предлагаемого метода лежит метод, основан-

ный на синтаксической абстракции и способный к масштабированию [2–4]. Од-

нако приведенное описание недостаточно полное, и отсутствует определение

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

ное применение метода.