Метод построения абстрактных моделей, используемых для верификации протоколов когерентности кэш-памяти масштабируемых систем

17 / 18

Метод построения абстрактных моделей, используемых для верификации протоколов…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1 65
Иванов Сергей Ростиславович — канд. техн. наук, доцент кафедры «Компьютерные
системы и сети» МГТУ им. Н.Э. Баумана (Российская Федерация, 105005, Москва,
2-я Бауманская ул., д. 5).
Просьба ссылаться на эту статью следующим образом:
Буренков В.С., Иванов С.Р. Метод построения абстрактных моделей, используемых для
верификации протоколов когерентности кэш-памяти масштабируемых систем // Вест-
ник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1. C. 49–66.
DOI: 10.18698/0236-3933-2017-1-49-66
METHOD OF CONSTRUCTING ABSTRACT MODELS FOR PROTOCOL
VERIFICATION OF CACHE COHERENCE IN SCALABLE SYSTEMS
V.S. Burenkov
S.R. Ivanov
Bauman Moscow State Technical University, Moscow, Russian Federation
Abstract Keywords
The article presents a novel approach to solving the verifica-
tion problem for cache coherence in scalable microprocessor
systems. The article examines a mathematical model of cache
coherence protocols. The model uses program graphs as an
abstraction for groups of devices operating in accordance
with a given cache coherence protocol. The whole protocol is
represented as a channel system that can be unfolded into a
transition system to be explored by model checking algo-
rithms. The paper proposes an approach to the construction
of Promela models of cache coherence protocols and defines
the limitations on models. The article presents a method for
constructing abstract models of cache coherence protocols
that produces models of significantly smaller size and there-
fore subjected to model checking. The method is based on
program graphs transformations, or, equivalently, on syntac-
tical transformations of Promela models. The paper contains
a mathematical proof of invariance preservation by the ab-
stract models. All the results are based on verification prac-
tice of a complex industrial Elbrus system-on-a-chip
Formal method, model checking,
model transformations, cache
coherence protocol
REFERENCES
[1] Burenkov V.S. An analysis of applicability of formal methods to verification of cache co-
herence protocols of scalable systems. Voprosy radioelektroniki [Questions of Radio-Electro-
nics], 2015, no. 3, pp. 105–117 (in Russ.).
[2] Chou C., Mannava P., Park S. A simple method for parameterized verification of cache
coherence protocols. Proc. “ Formal Methods in Computer-Aided Design”, 2004, pp. 382–398.
[3] Talupur M., Tuttle M. Going with the flow: Parameterized verification using message
flows. Proc. “ Formal Methods in Computer-Aided Design”, 2008, pp. 1–8.