Method of Constructing Abstract Models for Protocol Verification of Cache Coherence in Scalable Systems

The article presents a novel approach to solving the verification problem for cache coherence in scalable microprocessor systems. The article examines a mathematical model of cache coherence protocols. The model uses program graphs as an abstraction for groups of devices operating in accordance with a given cache coherence protocol. The whole protocol is represented as a channel system that can be unfolded into a transition system to be explored by model checking algorithms. The paper proposes an approach to the construction of Promela models of cache coherence protocols and defines the limitations on models. The article presents a method for constructing abstract models of cache coherence protocols that produces models of significantly smaller size and therefore subjected to model checking. The method is based on program graphs transformations, or, equivalently, on syntactical transformations of Promela models. The paper contains a mathematical proof of invariance preservation by the abstract models. All the results are based on verification practice of a complex industrial Elbrus system-on-a-chip.

References

[1] Burenkov V.S. An analysis of applicability of formal methods to verification of cache coherence protocols of scalable systems. Voprosy radioelektroniki [Questions of Radio-Electronics], 2015, no. 3, pp. 105-117 (in Russ.).

[2] Chou C., Mannava P., Park S. A simple method for parameterized verification of cache coherence protocols. Proc. "Formal Methods in Computer-Aided Design", 2004, pp. 382-398.

[3] Talupur M., Tuttle M. Going with the flow: Parameterized verification using message flows. Proc. "Formal Methods in Computer-Aided Design", 2008, pp. 1-8.

[4] O’Leary J., Talupur M., Tuttle M. Protocol verification using flows: An industrial experience. Proc. "Formal Methods in Computer-Aided Design", 2009, pp. 172-179.

[5] Sorin D.J., Hill M.D., Wood D.A. A primer on memory consistency and cache coherence. San Rafael, Morgan & Claypool Publishers, 2012. 210 p.

[6] Baier C., Katoen J.-P. Principles of model checking. Cambridge, MIT Press, 2008. 984 p.

[7] Holzmann G. The spin model checker: Primer and reference manual. Boston, Addison-Wesley Professional, 2003. 608 p.