16 / 18
В.С. Буренков, С.Р. Иванов
64
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
перехода
1
,
m m
s
s
таких, что
1
,
m
m
L s
L s
в абстрактной системе существу-
ет переход
1
,
m
m
f s
f s
такой, что
1
1
.
abs
m
m
L f s
L s
Заключение.
Предложенные преобразования формальных моделей протоко-
лов когерентности памяти позволяют уменьшить число процессов верифицируе-
мой модели с большого числа до нескольких (в настоящей работе четырех). Син-
таксическая природа преобразований позволяет их автоматизировать, а всю работу
по созданию и анализу соответствующей системы переходов предоставить средству
автоматизированной проверки моделей
Spin
. Это позволяет использовать все реа-
лизованные в нем алгоритмы, включая множество алгоритмов оптимизации, с по-
мощью которых можно сократить число состояний исследуемой системы перехо-
дов.
Все приведенные особенности и ограничения моделей соответствуют разра-
ботанному авторами подходу к составлению моделей протоколов когерентности,
который позволил лаконично описать протокол когерентности системы «Эль-
брус-4С» и провести верификацию системы из трех ядер. Предложенные аб-
страктные преобразования позволяют сократить число процессов и размеры ис-
пользуемых структур данных так, что после устранения ложных контрпримеров,
размер полученной модели будет находиться в пределах от размера модели для
трех ядер до размера модели для четырех ядер, что позволит провести верифика-
цию. Автоматизация процесса получения абстрактных моделей, описанного в
настоящей работе, а также разработка метода уточнения абстрактной модели для
устранения ложных контрпримеров являются направлениями дальнейшей рабо-
ты и исследований.
ЛИТЕРАТУРА
1.
Буренков В.С.
Анализ применимости формальных методов к верификации протоко-
лов когерентности кэш-памяти масштабируемых систем // Вопросы радиоэлектроники.
2015. № 3. С. 105–117.
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. P. 382–398.
3.
Talupur M., Tuttle M.
Going with the flow: Parameterized verification using message
flows // Proc. Formal Methods in Computer-Aided Design. 2008. P. 1–8.
4.
O’Leary J., Talupur M., Tuttle M.
Protocol verification using flows: An industrial expe-
rience // Proc. Formal Methods in Computer-Aided Design. 2009. P. 172–179.
5.
Sorin D.J., Hill M.D., Wood D.A.
A primer on memory consistency and cache coherence.
San Rafael: Morgan & Claypool Publishers, 2012. 210 p.
6.
Baier C., Katoen J.-P.
Principles of model checking. Cambridge: MIT Press, 2008. 984 p.
7.
Holzmann G.
The spin model checker: Primer and reference manual. Boston: Addison-
Wesley Professional, 2003. 608 p.
Буренков Владимир Сергеевич
— аспирант кафедры «Компьютерные системы и сети»
МГТУ им. Н.Э. Баумана (Российская Федерация, 105005, Москва, 2-я Бауманская ул.,
д. 5).