В.С. Буренков, С.Р. Иванов
2
ванию именно этих архитектур в современных промышленно выпус-
каемых многоядерных процессорах. Однако из-за оснащения каждого
процессора (ядра) локальной кэш-памятью возникает следующая за-
дача — требуется обеспечить согласованность (когерентность) бло-
ков кэш-памяти различных процессоров.
В решении проблемы когерентности выделяются два подхода:
программный и аппаратный. В силу большей производительности
аппаратные механизмы, называемые
протоколами когерентности
кэш-памяти, нашли наиболее широкое применение.
Работу протокола когерентности можно кратко описать следую-
щим образом. Адресное пространство разделено на области, каждая
из которых принадлежит одному из процессоров, отвечающих за до-
ступ к ней (home-процессор). Получив от ядра исходную команду
считывания или записи в память, кэш-память отправляет соответ-
ствующий запрос в home-процессор. Home-процессор рассылает за-
просы, отслеживающие состояние кэшей других процессоров (снуп-
запросы), и, возможно, запросы в память. В случае необходимости
выдается ответ запросчику, производится запись или считывание
данных. Таким образом, home-процессор выполняет роль координа-
тора всех действий.
Постоянно растущая сложность мультипроцессорных систем с
разделяемой памятью находит свое отражение и в замысловатости
протоколов когерентности этих систем. Более того, для новых поко-
лений микропроцессоров характерно увеличение количества вычис-
лительных ядер в составе процессора. Это, в свою очередь, определя-
ет сложность проверки корректности протоколов и порождает необ-
ходимость методов верификации протоколов когерентности систем
с любым числом ядер (так называемой параметризованной верифи-
кации).
2. Верификация протоколов когерентности.
При верификации
протоколов когерентности важными являются два аспекта:
• правильность разработки самих протоколов;
• корректность аппаратной реализации этих протоколов, т. е.
RTL-описания микропроцессора.
Прежде чем проверять аппаратную реализацию, желательно удо-
стовериться в корректности самого протокола. Распространенная
практика — анализ протокола вручную, а затем проверка реализации
тестами со случайными воздействиями — не дает возможности гово-
рить о каких-либо гарантиях корректности как протокола, так и си-
стемы. Случайная природа тестовых последовательностей не обеспе-
чивает полное покрытие пространства состояний протокола, тем бо-
лее за приемлемое время. Несмотря на то что данные методы
позволяют найти большое количество ошибок, сложные ошибки, свя-
