Сборники трудов ИСП РАН


Проверка параметризованных Promela-моделей протоколов когерентности памяти

В.C. Буренков (АО «МЦСТ», Москва, Россия)
А.C. Камкин (ИСП РАН, Москва, Россия)

Аннотация

В статье представлен метод масштабируемой верификации PROMELA-моделей протоколов обеспечения когерентности памяти. Под масштабируемостью понимается независимость затрат на верификацию (прежде всего, машинного времени и памяти) от числа процессоров в системе. Метод состоит из трех основных шагов. На первом шаге в модель протокола, созданную для определенной конфигурации системы (для конкретного числа процессоров), вводится параметр, представляющий число процессоров в системе. Для этого используются простые индуктивные правила, что возможно только при определенных допущениях на вид протокола. На втором шаге построенная параметризованная модель абстрагируется от числа процессоров. Для этого над присваиваниями, выражениями и коммуникационными действиями модели совершается ряд синтаксических преобразований. На третьем шаге полученная абстрактная модель верифицируется с помощью инструмента SPIN обычным образом. Помимо описания метода, в статье приводится доказательство его корректности: утверждается, что предложенная схема абстракции является консервативной в том смысле, что любой инвариант (свойство истинное во всех достижимых состояниях) абстрактной модели является инвариантом исходной модели (свойства-инварианты — это именно те свойства, которые представляют интерес при верификации протоколов обеспечения когерентности памяти). Предложенный метод был воплощен в прототипе инструмента, который разбирает код на языке PROMELA, строит дерево абстрактного синтаксиса, преобразует его по заданным правилам и отображает обратно в PROMELA код. Инструмент (и метод в целом) был успешно использован при верификации протоколов семейства MOSI, разработанных в АО «МЦСТ» и реализованных в вычислительных комплексах «Эльбрус».

Ключевые слова

многоядерные микропроцессоры, мультипроцессоры с разделяемой памятью, протоколы когерентности памяти, проверка моделей, SPIN, PROMELA

Издание

Труды Института системного программирования РАН, том 28, вып. 4, 2016, стр. 57-76.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(4)-4

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома