On the Implementation of a Formal Method for Verification of Scalable Cache Coherent Systems
https://doi.org/10.15514/ISPRAS-2015-27(3)-13
Abstract
This article analyzes existing methods of verification of cache coherence protocols of scalable systems. Based on the research literature, the paper describes a method of formal parameterized verification of safety properties of cache coherence protocols. The paper proposes a design of a verification system for cache coherence protocols. The article analyzes the method in terms of development and examination of the corresponding Promela model of the German cache coherence protocol and discusses extension and automation of the method needed to adapt it to verification challenges of the Elbrus microprocessors.
About the Author
Vladimir Burenkov
Bauman Moscow State Technical University; MCST
Russian Federation
Russian Federation
References
1. Z. Manna, A. Pnueli, “The temporal logic of reactive and concurrent systems: specification,” Springer-Verlag, 427 pp., 1992.
2. E.M. Clarke, O. Grumberg, D. Peled, “Model checking,” MIT Press, 314 pp., 1999.
3. S. Park, D. Dill, “Verification of FLASH cache coherence protocol by aggregation of distributed transactions,” Proceedings of the 8th annual ACM symposium on parallel algorithms and architectures, pp. 288–296, 1996.
4. M. Talupur, “Abstraction Techniques for Parameterized Verification,” PhD Thesis, 2006.
5. E. Clarke, D. Long, K. McMillan, “Compositional model checking,” Proceedings of the fourth IEEE symposium on logic in computer science, 1989.
6. C. Chou, P. Mannava, S. Park, “A simple method for parameterized verification of cache coherence protocols,” Formal methods in computer-aided design, vol. 3312, pp. 382–398, 2004.
7. V. Burenkov, “Generator testov dlya verifikatsii protocola cogerentnosti kesh pamyati [A test generator for cache coherence protocol verification],” Voprosi radioelektroniki, seria EVT, 3, pp. 56–63, 2014.
8. G. Holzmann, “The Spin model checker: primer and reference manual,” Addison-Wesley Professional, 608 pp., 2003.
9. S. Krstic, “Parameterized system verification with guard strengthening and parameter abstraction,” Automated verification of infinite state systems, 2005.
10. A. Pnueli, S. Ruah, L. Zuck, “Automatic deductive verification with invisible invariants,” Tools and algorithms for the construction and analysis of systems, vol. 2031, pp. 82–97, 2001.
Review
For citations:
Burenkov V. On the Implementation of a Formal Method for Verification of Scalable Cache Coherent Systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(3):183-196. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(3)-13
Email this article 