|

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

Авторы: Буренков В.С., Иванов С.Р. Опубликовано: 14.02.2017
Опубликовано в выпуске: #1(112)/2017  
DOI: 10.18698/0236-3933-2017-1-49-66

 
Раздел: Информатика, вычислительная техника и управление | Рубрика: Теоретическая информатика, кибернетика  
Ключевые слова: формальный метод, проверка моделей, преобразование моделей, протокол когерентности кэш-памяти

Изложен новый подход к решению задачи верификации протоколов когерентности кэш-памяти масштабируемых микропроцессорных систем. Рассмотрена математическая модель протоколов когерентности. Модель представляет собой отдельные группы устройств, работающих в соответствии с протоколом, в виде графов программ, а протокол в целом - в виде канальной системы, из которой может быть получена и исследована методом Model checking система переходов. Предложен подход к описанию моделей протоколов когерентности на языке Promela и сформулированы ограничения на модели. Представлен метод построения абстрактных моделей, позволяющий существенно уменьшить их размер и базирующийся на преобразованиях отдельных графов программ исходной модели, или на синтаксических преобразованиях Promela-процессов. Приведено математическое доказательство сохранения преобразованиями свойств-инвариантов. Результаты основаны на практике верификации протокола сложной системы на кристалле с архитектурой "Эльбрус".

Литература

[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 experience // 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.