Проблемы параметризованной верификации протоколов когерентности памяти
9
В [9] сообщается о параметризованной верификации протокола
LCP (Larrabee coherence protocol), разработанного в Intel и имеющего
около 50 различных типов сообщений. На модели, описанной на язы-
ке Murphi, проверялось выполнение свойства безопасности (если в
системе есть кэш с эксклюзивным доступом к данным, то никакой
другой кэш не имеет доступа к этим данным) и свойств, определяю-
щих согласованность между списком кэшей с доступом к данным,
который хранится в справочнике home-процессора, и реальным набо-
ром кэшей с таким доступом.
Авторами [9] был разработан инструмент, принимающий на вход
параметризованное описание протокола на Murphi и описание пото-
ков в отдельном файле. Инструмент строит промежуточное пред-
ставление Murphi-описания в виде абстрактного синтаксического де-
рева. Операции абстракции и уточнения далее выполняются над этим
представлением. Инструмент автоматически строит леммы на основе
потоков и добавляет их к защитам подходящих правил (правило, чья
защита находится в инварианте потока, модифицируется этим инвари-
антом). Авторы отмечают использование 15 потоков, полученных из
документов на протокол и породивших 36 лемм, 25 из которых разра-
ботаны на основе ограничений предшествования, а остальные — на
основе ограничений по конфликтам. Еще 5 лемм пришлось добавить
вручную. Таким образом, предложенный метод позволил намного
сократить объем ручной работы, выполненной при верификации по-
хожего протокола [23].
В [24] предлагается подход к полной автоматизации процесса по-
лучения лемм, основанный на бинарных решающих диаграммах. Од-
нако отсутствие масштабируемости этого подхода является камнем
преткновения.
Заключение.
Достоинства метода model checking — полная ав-
томатизация и порождение контрпримеров, позволяющих отыскивать
источники ошибок, — делают его наиболее удобным формальным
методом верификации протоколов когерентности памяти. Однако ме-
тод подвержен проблеме комбинаторного «взрыва числа состояний»,
а потому может быть применен лишь к системам с тремя-четырьмя
процессорными ядрами.
Ключ к решению проблемы видится в комбинации методов, ос-
нованных на model checking, с методами, основанными на доказа-
тельстве теорем.
Наиболее интересным из упомянутых в литературе представляет-
ся метод CMP, дополненный средствами автоматизации получения
необходимых для его работы лемм. Предполагается применить дан-
ный метод к протоколам микропроцессоров архитектуры «Эльбрус»,
предварительно разрешив ряд проблем. В литературе нет детального
