Главная         Авторы   Статьи   Год проведения   Тематика   Организации        Конференция МЭС

Метод масштабируемой верификации PROMELA-моделей протоколов когерентности кэш-памяти
Авторы
	Камкин А.С.
	Буренков В.С.
Год публикации
	2016
УДК
	004.05
Аннотация
	В статье рассматривается метод масштабируемой верификации моделей протоколов когерентности кэш-памяти, описанных на языке PROMELA. Под масштабируемостью понимается независимость затрат на верификацию от размера модели (по сути, от числа процессоров в проверяемой системе). Метод состоит из трех этапов. Сначала PROMELA-спецификация протокола, выполненная для фиксированной конфигурации системы, обобщается до спецификации, параметризованной числом процессоров (для этого используются некоторые предположения об устройстве протокола и простые правила индукции). Затем выполняется построение абстрактной спецификации, независимой от числа процессоров (это делается путем синтаксических преобразований спецификации). Наконец, построенная абстрактная спецификация верифицируется инструментом SPIN обычным образом. Метод успешно применялся для верификации протоколов семейства MOSI, реализованных в вычислительных комплексах «Эльбрус».
Ключевые слова
	многоядерные микропроцессоры, мультипроцессоры с общей памятью, протоколы обеспечения когерентности кэш-памяти, проверка моделей, SPIN, PROMELA.
Ссылка на статью
	Камкин А.С., Буренков В.С. Метод масштабируемой верификации PROMELA-моделей протоколов когерентности кэш-памяти // Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС). 2016. № 2. С. 54-60.
Адрес статьи
	http://www.mes-conference.ru/data/year2016/pdf/D109.pdf