Проблемы параметризованной верификации протоколов когерентности памяти
УДК 004.052.4
Проблемы параметризованной верификации
протоколов когерентности памяти
© В.С. Буренков, С.Р. Иванов
МГТУ им. <...> Н.Э. Баумана, Москва, 105005, Россия
Проанализированы основные направления верификации протоколов когерентности
и сопутствующие проблемы. <...> Сформулирована проблема когерентности памяти,
присущая мультипроцессорным системам, и кратко описаны аппаратные пути ее
решения — протоколы когерентности. <...> Особое внимание уделено параметризованной верификации, призванной предоставить доказательство корректности протокола с любым
числом агентов. <...> Обозначены достоинства и недостатки существующих методов
и определены направления дальнейшей работы по верификации протоколов, разработанных для микропроцессоров архитектуры «Эльбрус». <...> Ключевые слова: протокол когерентности памяти, верификация протоколов,
формальные методы, проверка модели, доказательство теорем. <...> Протоколы когерентности памяти современных вычислительных систем отличаются высоким уровнем сложности и колоссальной размерностью пространства состояний. <...> Существующие подходы к верификации, как правило, либо неприменимы к протоколам промышленного масштаба, либо требуют
огромного объема ручной работы. <...> Мультипроцессорная система с разделяемой памятью состоит из двух или
более независимых процессоров, каждый из которых выполняет либо
часть большой программы, либо независимую программу. <...> Для сокращения задержки на доступ к памяти каждый процессор снабжается локальной кэш-памятью. <...> Высокие уровни
производительности устройств с мультипроцессорной архитектурой
и разделяемой памятью обусловили строгую тенденцию к использо1 <...> В.С. Буренков, С.Р. Иванов
ванию именно этих архитектур в современных промышленно выпускаемых многоядерных процессорах. <...> Однако из-за оснащения каждого
процессора (ядра) локальной кэш-памятью возникает следующая задача — требуется <...>