Checking Parameterized Promela Models of Cache Coherence Protocols
https://doi.org/10.15514/ISPRAS-2016-28(4)-4
Abstract
This paper introduces a method for scalable verification of cache coherence protocols described in the Promela language. Scalability means that resources spent on verification (first of all, machine time and memory) do not depend on the number of processors in the system under verification. The method is comprised of three main steps. First, a Promela model written for a certain configuration of the system is generalized to the model being parameterized with the number of processors. To do it, some assumptions on the protocol are used as well as simple induction rules. Second, the parameterized model is abstracted from the number of processors. It is done by syntactical transformations of the model assignments, expressions, and communication actions. Finally, the abstract model is verified with the Spin model checker in a usual way. The method description is accompanied by the proof of its correctness. It is stated that the suggested abstraction is conservative in a sense that every invariant (a property that is true in all reachable states) of the abstract model is an invariant of the original model (invariant properties are the properties of interest during verification of cache coherence protocols). The method has been automated by a tool prototype that, given a Promela model, parses the code, builds the abstract syntax tree, transforms it according to the rules, and maps it back to Promela. The tool (and the method in general) has been successfully applied to verification of the MOSI protocols implemented in the Elbrus computer systems.
About the Authors
V. S. Burenkov
JSC MCST
Russian Federation
Russian Federation
A. S. Kamkin
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. Patterson D.A., Hennessy J.L. Computer Organization and Design: The Hardware/Software Interface. Morgan Kaufmann, 2013. 800 p.
2. Kim A.K., Perekatov V.I., Ermakov S.G. Microprocessors and computer systems of the Elbrus familty. SPb.: Piter, 2013. 272 p. (in Russian).
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. Kamkin A.S., Petrochenkov M.V. A system to support formal methods-based verification of coherence protocol implementations. Voprosy radioehlektroniki. Ser. EVT. [Issues of radio electronics], 2014, issue 3, pp. 27-38 (in Russian).
5. Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT Press, 1999. 314 p.
6. Burenkov V.S. An analysis of the Spin model checker applicability to cache coherence protocols verification. Voprosy radioehlektroniki. Ser. EVT [Issues of radio electronics], 2014, issue 3, pp. 126-134 (in Russian).
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.
Review
For citations:
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
Email this article 