A Technique for Parameterized Verification of Cache Coherence Protocols

This paper introduces a technique for scalable functional verification of cache coherence protocols that is based on the verification method, which was previously developed by the author. Scalability means that verification efforts do not depend on the model size (that is, the number of processors in the system under verification). The article presents an approach to the development of formal Promela models of cache coherence protocols and shows examples taken from the Elbrus-4C protocol model. The resulting formal models consist of language constructs that directly reflect the way protocol designers describe their developments. The paper describes the development of the tool, which is written in the C++ language with the Boost.Spirit library as parser generator. The tool automatically performs the syntactical transformations of Promela models. These transformations are part of the verification method. The procedure for refinement of the transformed models is presented. The refinement procedure is supposed to be used to eliminate spurious error messages. Finally, the overall verification technique is described. The technique has been successfully applied to verification of the MOSI protocol implemented in the Elbrus computer systems. Experimental results show that computer memory requirements for parameterized verification are negligible and the amount of manual work needed is acceptable.

multicore microprocessors, shared memory multiprocessors, cache coherence protocols, model checking, Spin, Promela

1. Patterson D.A., Hennessy J.L. Computer Organization and Design: The Hardware/Software Interface. Morgan Kaufmann, 2013. 800 p.

2. Sorin D.J., Hill M.D., Wood D.A. A Primer on Memory Consistency and Cache Coherence. Morgan and Claypool, 2011. 195 p.

3. Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT Press, 1999. 314 p.

4. Burenkov V.S. Analiz primenimosti instrumenta Spin k verifikacii protokolov kogerentnosti pamyati [An analysis of the Spin model checker applicability to cache coherence protocols verification]. Voprosy radioehlektroniki. Ser. EVT. Issues of Radioelectronics, the series EVT], 2014, issue. 3, pp. 126-134 (in Russian).

5. Burenkov V.S., Kamkin A.S. Checking Parameterized PROMELA Models of Cache Coherence Protocols. Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 4, 2016, pp. 57-76. DOI: 10.15514/ISPRAS-2016-28(4)-4

6. Burenkov V.S., Kamkin A.S. Metod masshtabiruemoi verifikacii PROMELA-modelei protocolov kogerentnosti kesh-pamyati [A Method for Scalable Verification of PROMELA Models of Cache Coherence Protocols]. Sb. trudov VII Vserossiiskoi nauchno-technicheskoi konferencii “Problemi razrabotki perspectivnih micro- i nanoelektronnih sistem” [Proceedings of the VII All-Russian Scientific and Technical Conference "Problems of Development of Advanced Micro- and Nanoelectronic Systems"]. 2016, part II, pp. 54-60 (in Russian).

7. Burenkov V.S., Kamkin A.S. Applying Parameterized Model Checking to Real-Life Cache Coherence Protocols. Proc. of IEEE East-West Design & Test Symposium. 2016. pp. 1-4.

8. Burenkov V.S., Ivanov S.R. Metod postroeniya abstraktnih modelei, ispolzuemih dlya verifikacii protocolov kogerentnosti kesh-pamyati [A Method for Construction of Abstract Models Used for Verification of Cache Coherence Protocols]. Vestnik MGTU im N.E. Baumana [Herald of the Bauman Moscow State Technical University], 2017, issue 1, pp. 49-66 (in Russian).

9. 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.

10. 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.

11. Krstic S. Parameterized System Verification with Guard Strengthening and Parameter Abstraction. International Workshop on Automated Verification of Infinite-State Systems, 2005.

12. Talupur M., Tuttle M.R. Going with the Flow: Parameterized Verification Using Message Flows. Formal Methods in Computer-Aided Design, 2008. pp. 1-8.

13. 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.

14. Baier C., Katoen J.-P. Principles of Model Checking. The MIT Press. 2008. 984 p.

15. de Guzman, J. Fastest numeric parsers in the world! http://boost-spirit.com/home/2014/09/03/fastest-numeric-parsers-in-the-world/.

16. Spin Version 6 – Promela Grammar. http://spinroot.com/spin/Man/grammar.html.

17. Holzmann, G. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley. 2004. 608 p.