Checking Parameterized Promela Models of Cache Coherence Protocols
https://doi.org/10.15514/ISPRAS-2016-28(4)-4
Abstract
About the Authors
V. S. BurenkovRussian Federation
A. S. Kamkin
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