| 
Метод построения абстрактных моделей, используемых для верификации протоколов когерентности кэш-памяти масштабируемых систем
| Авторы: Буренков В.С., Иванов С.Р. | Опубликовано: 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.
