Сборники трудов ИСП РАН


Методика параметризованной верификации протоколов когерентности памяти

В.С. Буренков (МЦСТ, Москва, Россия)

Аннотация

В статье представлена методика масштабируемой функциональной верификации протоколов когерентности памяти, которая основана на методе верификации, который ранее был разработан автором статьи. Масштабируемость при верификации означает независимость работ по верификации от размера модели, то есть от количества процессоров верифицируемой системы.  В статье предложен подход к разработке формальных моделей протоколов когерентности памяти на языке Promela. Приведены примеры описаний, взятые из модели протокола когерентности памяти системы Эльбрус-4С. Результирующие формальные модели отражают представление протоколов когерентности памяти, используемое разработчиками таких протоколов – в виде множества взаимодействующих конечных автоматов. Описана разработка программного инструмента, написанного на языке С++ с использованием библиотеки Boost.Spirit в качестве генератора синтаксических анализаторов. Программный инструмент позволяет автоматизировать выполнение синтаксических преобразований Promela-моделей. Выполнение данных синтаксических преобразований происходит в соответствии с методом верификации. В статье представлена процедура уточнения модифицированных моделей, основанная на введении в модель вспомогательных переменных. Использовать эту процедуру предлагается в том случае, когда при верификации возникают ложные сообщения об ошибках, для устранения таких сообщений. Представлена методика верификации, которая состоит из следующих шагов: разработка исходной модели протокола когерентности памяти на языке Promela, автоматизированное преобразование данной модели согласно методу верификации, верификация модифицированной модели с помощью инструментального средства Spin, анализ отчета о верификации, сгенерированного инструментом Spin. Изложенная методика была успешно применена для верификации протокола когерентности памяти семейства MOSI, реализованного в микропроцессорной системе Эльбрус-4С. Экспериментальные результаты показали, что затраты процессорного времени и памяти на проведение параметризованной верификации незначительны, а требуемый объем ручной работы приемлем. Для уточнения модифицированной модели протокола системы Эльбрус-4С понадобилось ввести лишь две вспомогательные переменные.

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

многоядерные микропроцессоры; мультипроцессоры с разделяемой памятью; протоколы когерентности памяти; проверка моделей; Spin; Promela

Издание

Труды Института системного программирования РАН, том 29, вып. 4, 2017, стр. 231-246

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(4)-15

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома