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