В.С. Буренков, С.Р. Иванов
8
будет найден контрпример, проявляющийся и в исходном протоколе,
либо не будет доказана истинность проверяемого свойства.
В [22] доказывается, что метод CMP корректен для любого сим-
метричного протокола и любой консервативной процедуры аб-
стракции.
Основная сложность метода заключается в нахождении лемм.
В [5] отражен опыт применения метода к протоколам FLASH и Ger-
man. В [23] сообщается, что в Intel метод был применен к протоколу
когерентности, сложность которого на несколько порядков выше,
чем у протокола FLASH. В протоколе FLASH возможны 16 различ-
ных типов сообщений, а в протоколе Intel — 54. Верификация заняла
около месяца и потребовала 25 разработанных вручную лемм. До-
бавление лемм — трудоемкий процесс, занимающий много времени
и требующий глубокого понимания протокола. На этом этапе в Intel
были автоматизированы такие процессы, как составление исходной
абстракции и уточнение абстракции на основе предоставленных
лемм.
В [22] описан подход на основе потоков сообщений (message
flows), призванный сократить объем ручной работы при поиске инва-
риантов. Потоки сообщений — это последовательности сообщений,
пересылаемые между процессорами во время работы протокола.
Введенные в [22] потоки отражают линейный порядок событий, в ко-
торых участвуют два агента. В [9] сообщается, что такое определение
потоков, в частности принятие во внимание двух агентов, недоста-
точно для случая реальных протоколов когерентности, поскольку в
модели протокола, помимо кэшей и home-процессора, должен быть
отражен и контроллер памяти. Более того, некоторому событию мо-
гут предшествовать несколько других событий, что не может быть
зафиксировано линейными потоками, поэтому в [9] вводятся потоки
в виде ориентированных ациклических графов. Авторы предлагают
язык, позволяющий специфицировать события наряду с участниками.
Отслеживание активных потоков может привести к порождению
полезных лемм. Модель протокола должна быть написана так, чтобы
каждое правило соответствовало определенному событию, отражен-
ному в потоках. Тогда в модель могут быть добавлены вспомогатель-
ные переменные, позволяющие следить за состояниями потоков.
На основе значений этих переменных могут быть получены два
класса лемм: ограничения предшествования, устанавливающие порядок
срабатываний правил, и ограничения по конфликтам, запрещающие од-
ним потокам переходить в активное состояние, пока не завершатся дру-
гие. Заметим, что возможны и другие виды лемм, причем не все они
одинаково полезны. В связи с этим необходимо отыскивать такие клас-
сы, которые позволяют эффективно проводить верификацию.
