Проверка параметризованных Promela-моделей протоколов когерентности памяти
https://doi.org/10.15514/ISPRAS-2016-28(4)-4
Аннотация
Об авторах
В. С. БуренковРоссия
А. С. Камкин
Россия
Список литературы
1. Patterson D.A., Hennessy J.L. Computer Organization and Design: The Hardware/Software Interface. Morgan Kaufmann, 2013. 800 p.
2. Ким A.K., Перекатов В.И., Ермаков С.Г. Микропроцессоры и вычислительные комплексы семейства «Эльбрус». Спб.: Питер, 2013. 272 с.
3. Sorin D.J., Hill M.D., Wood D.A. A Primer on Memory Consistency and Cache Coherence. Morgan and Claypool, 2011, 195 p.
4. Камкин А.С., Петроченков М.В. Система поддержки верификации реализаций протоколов когерентности с использованием формальных методов. Вопросы радиоэлектроники. Серия ЭВТ, 2014, вып. 3, стр. 27-38.
5. Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT Press, 1999, 314 p.
6. Буренков В.С. Анализ применимости инструмента SPIN к верификации протоколов когерентности памяти. Вопросы радиоэлектроники. Серия ЭВТ, 2014. вып. 3, стр. 126-134.
7. Emerson E.A., Kahlon V. Exact and Efficient Verification of Parameterized Cache Coherence Protocols. Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, 2003, pp. 247-262.
8. Holzmann, G.J. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003, 608 p.
9. Park S., Dill D.L. Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. Annual ACM Symposium on Parallel Algorithms and Architectures, 1996, pp. 288-296.
10. Ip C.N., Dill D.L. Verifying Systems with Replicated Components in Murphi. International Conference on Computer Aided Verification, 1996, pp. 147-158.
11. Pnueli A., Xu J., Zuck L. Liveness with (0, 1, )-Counter Abstraction. International Conference on Computer Aided Verification, 2002, pp. 107-122.
12. Clarke E., Talupur M., Veith H. Environment Abstraction for Parameterized Verification. Verification, Model Checking, and Abstract Interpretation, 2006. LNCS, vol. 3855, pp. 126-141.
13. Clarke E., Talupur M., Veith H. Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 33-47.
14. McMillan K. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. Conference on Correct Hardware Design and Verification Methods, 2001, pp. 179-195.
15. Chou C.-T., Mannava P.K., Park S. A Simple Method for Parameterized Verification of Cache Coherence Protocols. Formal Methods in Computer-Aided Design, 2004. LNCS, vol. 3312, pp. 382-398.
16. Krstic S. Parameterized System Verification with Guard Strengthening and Parameter Abstraction. International Workshop on Automated Verification of Infinite-State Systems, 2005.
17. Talupur M., Tuttle M.R. Going with the Flow: , pp. 1-8.
18. O'Leary J., Talupur M., Tuttle M.R. Protocol Verification Using Flows: An Industrial Experience. Formal Methods in Computer-Aided Design, 2009, pp. 172-179.
Рецензия
Для цитирования:
Буренков В.С., Камкин А.С. Проверка параметризованных Promela-моделей протоколов когерентности памяти. Труды Института системного программирования РАН. 2016;28(4):57-76. https://doi.org/10.15514/ISPRAS-2016-28(4)-4
For citation:
Burenkov V.S., Kamkin A.S. Checking Parameterized Promela Models of Cache Coherence Protocols. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(4):57-76. https://doi.org/10.15514/ISPRAS-2016-28(4)-4