Проблемы параметризованной верификации протоколов когерентности памяти
Опубликовано: 18.11.2013
Авторы: Буренков В.С., Иванов С.Р.
Опубликовано в выпуске: #11(23)/2013
DOI: 10.18698/2308-6033-2013-11-1013
Раздел: Информационные технологии
Проанализированы основные направления верификации протоколов когерентности и сопутствующие проблемы. Сформулирована проблема когерентности памяти, присущая мультипроцессорным системам, и кратко описаны аппаратные пути ее решения - протоколы когерентности. Рассмотрены методы верификации протоколов когерентности. Особое внимание уделено параметризованной верификации, призванной предоставить доказательство корректности протокола с любым числом агентов. Обозначены достоинства и недостатки существующих методов и определены направления дальнейшей работы по верификации протоколов, разработанных для микропроцессоров архитектуры "Эльбрус".
Литература
[1] Pong F., Dubois M. A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems, 1995, vol. 6, no. 8, pp. 773-787
[2] Буренков В.С. Метод перебора состояний для верификации протоколов когерентности памяти. Тр. 54-й науч. конф. МФТИ, 2011, с. 22, 23
[3] Pong F., Dubois M. Verification Techniques for Cache Coherence Protocols. ACM Computing Surveys, 1997, vol. 29, no. 1, pp. 82-126
[4] Clarke E., Grumberg O., Peled D. Model Checking. MIT Press, 1999, 314 p.
[5] Chou C., Mannava P., Park S. A Simple Method for Parameterized Verification of Cache Coherence Protocols. Formal Methods in Computer-Aided Design. 2004, vol. 3312, pp. 382-398
[6] Harrison J. Formal Methods at Intel - An Overview. Second NASA Formal Methods Symposium, 2010. URL: http://www.cl.cam.ac.uk/~jrh13/slides/nasa-14apr10/slides.pdf (дата обращения 09.11.2013)
[7] Буренков В.С. Инструмент верификации протокола когерентности памяти. Молодежный научно-технический вестник, 2013, № 1. URL: http://sntbul.bmstu.ru (дата обращения 09.11.2013)
[8] Буренков В.С. Анализ применимости инструмента Spin к верификации протоколов когерентности памяти. Вопросы радиоэлектроники, 2013, вып. 3, с. 126-134
[9] O’Leary J., Talupur M., Tuttle M. Protocol Verification Using Flows: An Industrial Experience. Formal Methods in Computer-Aided Design, 2009, pp. 172-179
[10] Clarke E., Talupur M., Veith H. Environment Abstraction for Parameterized Verification. Verification, Model Checking, and Abstract Interpretation, 2006, vol. 3855, pp. 126-141
[11] Talupur M. Abstraction Techniques for Parameterized Verification, Thesis ... PhD, 2006. URL: http://reports-archive.adm.cs.cmu.edu/anon/2006/CMU-CS-06-169.pdf (дата обращения 09.11.2013)
[12] Clarke E., Talupur M., Veith H. Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems, 2008, pp. 33-47
[13] Emerson A., Kahlon V. Reducing Model Checking of the Many to the Few. Automated Deduction, 2000, vol. 1831, pp. 236-254
[14] Emerson A., Kahlon V. Model Checking Large-Scale and Parameterized Resource Allocation Systems. Tools and Algorithms for the Construction and Analysis of Systems, 2002, vol. 2280, pp. 251-265
[15] Emerson A., Namjoshi K. Reasoning about Rings. Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1995, pp. 85-94
[16] Clarke E., Talupur M., Touili T., Veith H. Verification by Network Decomposition. CONCUR, 2004, vol. 3170, pp. 276-291
[17] Park S., Dill D. Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. Proceedings of the 8th annual ACM symposium on parallel algorithms and architectures, 1996, pp. 288-296
[18] Owre S., Rushby J., Shankar N. PVS: A prototype verification system. Automated Deduction, 1992, vol. 607, pp. 748-752
[19] Kuskin J., Ofelt D., Heinrich M., Heinlein J., Simoni R., Gharachorloo K., Chapin J., Nakahira D., Baxter J., Horowitz M., Gupta A., Rosenblum M., Hennessy J. The Stanford FLASH multiprocessor. ISCA Proceedings of the 21st annual international symposium on Computer architecture, 1994, pp. 302-313
[20] McMillan K. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 2001, pp. 179-195
[21] Krstic S. Parameterized System Verification with Guard Strengthening and Parameter Abstraction. Automated Verification of Infinite State Systems, 2005
[22] Talupur M., Tuttle M. Going with the Flow: Parameterized Verification Using Message Flows. Formal Methods in Computer-Aided Design, 2008, pp. 1-8
[23] Talupur M., Krstic S., O’Leary J., Tuttle M.R. Parametric Verification of Industrial Strength Cache Coherence Protocols. In Proc. Workshop on Design of Correct Circuits (DCC), 2008
[24] Bingham J. Automatic Non-interference Lemmas for Parameterized Model Checking. Formal Methods in Computer-Aided Design, 2008, pp. 77-85