On the implementation of a formal method for verification of scalable cache coherent systems

This article analyzes existing methods of verification of cache coherence protocols of scalable systems. Analyzed methods include model checking, deductive verification, methods that extend these two methods: compositional verification methods and abstraction-based methods. Based on the research literature, the paper describes a method of formal parameterized verification of safety properties of cache coherence protocols. The method is based on syntactical transformations of Promela models. First, a mathematical model (transition system) of cache coherence protocols is described. Second, the corresponding abstract model is presented according with the concrete model transformations. These transformations lead to abstract model that is independent of the number of processors in the system under verification. The paper proposes a design of a verification system for cache coherence protocols. The main part of the design is a Promela translator and abstract transformations subsystem that obtains an internal representation of a Promela model and modifies it according to the transformations. The article analyzes the method in terms of development and examination of the corresponding Promela model of the German cache coherence protocol. Examples of the syntactic transformations are shown. In order to demonstrate the method’s ability to find bugs, verification results of two buggy versions of the German protocol obtained from the literature are presented and analyzed. Drawbacks of the method are presented. In particular, the usage of a limited Promela subset leads to unnecessary complications and unnatural models. The paper discusses extension and automation of the method needed to adapt it to verification challenges of the Elbrus microprocessors.