Проблемы параметризованной верификации протоколов когерентности памяти

Проанализированы основные направления верификации протоколов когерентности и сопутствующие проблемы. Сформулирована проблема когерентности памяти, присущая мультипроцессорным системам, и кратко описаны аппаратные пути ее решения — протоколы когерентности. Рассмотрены методы верификации протоколов когерентности. Особое внимание уделено параметризованной верификации, призванной предоставить доказательство корректности протокола с любым числом агентов. Обозначены достоинства и недостатки существующих методов и определены направления дальнейшей работы по верификации протоколов, разработанных для микропроцессоров архитектуры «Эльбрус».

Авторы

Буренков В.С.

Тэги

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

Тематические рубрики

Общий отдел

Предметные рубрики

В этом же номере:

Выбор средств защиты информации, обрабатываемой в информационных системах персональных данных, Использование радиуса устойчивости оптимизационных задач для скрытия и проверки корректности информации, ...

Резюме по документу**

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

** - вычисляется автоматически, возможны погрешности

Похожие документы:

Похожие документы из РУАЭСТ
|
Похожие документы из Руконт

Проблемы параметризованной верификации протоколов когерентности памяти

Помощь:

Участники: