Широкое использование методов поиска ошибок в устройствах, которые реализуют протоколы когерентности памяти, основанных на моделировании со случайными воздействиями, не обеспечивает 100%-ной полноты верификации. Некоторые ошибки могут проявиться лишь при возникновении длинных последовательностей событий, таких как кэш-промахи и прием сообщений различными частями системы. Поскольку число таких последовательностей является комбинаторным, вероятность их возникновения во время моделирования со случайными воздействиями резко уменьшается при увеличении их длины [1].
На проведение верификации, в ходе которой анализируются все достижимые состояния верифицируемой системы, нацелены формальные методы. В ходе формальной верификации проверяется соответствие абстрактной модели протокола его спецификации. В общем случае моделью протокола когерентности памяти является конечный автомат. В силу этого для верификации протокола может быть применен формальный метод model checking [2], в котором модель верифицируемой системы (структура Крипке) представляет собой вариант конечного автомата.
Верификация протокола когерентности «Эльбрус-2S» указанным методом была проведена с использованием инструментального средства Spin (Simple Promela Interpreter) [3], выполняющего проверку корректности взаимодействующих параллельных асинхронных процессов. Эта функция была особенно существенна, поскольку процессоры системы, протокол когерентности которой проверяется, работают параллельно и асинхронно по отношению друг к другу.
Подробнее… Загрузить файл (doc.)
Содержание:
Введение
1. Основные средства и алгоритмы верификации Spin
Теоретико-автоматный подход.
Процессы в Promela.
Параллелизм в Spin.
Проверка выполнимости свойств.
Поиск циклов в автомате.
Хранение векторов состояний.
Верификация «на лету».
2. Оптимизации Spin
Редукция частичных порядков.
Метод collapse.
Об эффекте техники с использованием минимального автомата.
3. Результаты верификации протокола когерентности «Эльбрус-2S»
Заключение
Литература