This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A New Approach for the Verification of Cache Coherence Protocols
August 1995 (vol. 6 no. 8)
pp. 773-787

Abstract—In this paper, we introduce a cache protocol verification technique based on a symbolic state expansion procedure. A global Finite State Machine (FSM) model characterizing the protocol behavior is built and protocol verification becomes equivalent to finding whether or not the global FSM may enter erroneous states. In order to reduce the complexity of the state expansion process, all the caches in the same state are grouped into an equivalence class and the number of caches in the class is symbolically represented by a repetition constructor. This symbolic representation is partly justified by the symmetry and homogeneity of cache-based systems. However, the key idea behind the representation is to exploit a unique property of cache coherence protocols: the fact that protocol correctness is not dependent on the exact number of cached copies. Rather, symbolic states only need to keep track of whether the caches have 0, 1, or multiple copies. The resulting symbolic state expansion process only takes a few steps and verifies the protocol for any system size. Therefore, it is more efficient and reliable than current approaches.

The verification procedure is first applied to the verification of five existing protocols under the assumption of atomic protocol transitions. A simple snooping protocol on a split-transaction shared bus is also verified to illustrate the extension of our approach to protocols with nonatomic transitions.

[1] J. Archibald and J.L. Baer, "Cache Coherence Protocols: Evaluation Using a Multiprocessor Simulation Model," ACM Trans. Computer Systems, vol. 4, no. 4, Nov. 1986.
[2] J.-L. Baer and C. Girault,“A Petri Net model for a solution to the cache coherence problem,” Proc. First Conf. Supercomputing Systems, pp. 680-689, 1985.
[3] G.V. Bochmann,“Combining assertions and states for the validation of process communications,” Proc. IFIP, 1978.
[4] G.V. Bochmann and J. Gecsei,“A unified method for the specification and verification of protocols,” Proc. IFIP, 1977.
[5] G.V. Bochmann and C.A. Sunshine,“Formal methods in communication protocol design,” IEEE Trans. Comm., vol. 28, no. 4, pp. 624-631, Apr. 1980.
[6] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[7] L.M. Censier and P. Feautrier,“A new solution to coherence problems in multi-cache systems,” IEEE Trans. Computers, vol. 27, no. 12, pp. 1,112-1,118, Dec. 1978.
[8] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[9] E.M. Clarke, T. Filkorn, and S. Jha, “Exploiting Symmetries in Temporal Model Logic Model Checking,” Proc. CAV'93, C. Courcoubetis, ed., pp. 450–462, 1993.
[10] E.M. Clarke,O. Grumberg,H. Hiraishi,S. Jha,D.E. Long,K.L. McMillan,, and L.A. Ness,“Verification of the Futurebus+ cache coherence protocol,” Proc. Eleventh Int’l Symp. Computer Hardware Description Languages and Their Applications, Apr. 1993.
[11] O. Coudert,C. Berthet,, and J.C. Madre,“Verification of synchronous sequential machines based on symbolic execution,” LNCS: Automatic Verification Methods for Finite State Systems, J. Sifakis, ed., vol. 407, Springer-Verlag, June 1989, pp. 365-373.
[12] A.S. Danthine,“Protocol representation with finite-state models,” IEEE Trans. Comm., vol. 28, no. 4, pp. 632-642, Apr. 1980.
[13] A.J. Dill, D.L. Drexler, A.J. Hu, and C.H. Yang, “Protocol Verification as a Hardware Design Aid,” Proc. IEEE Int'l Conf. Computer Design: VLSI in Computers and Processors, 1992.
[14] E.A. Emerson and A.P. Sistla, "Symmetry and Modelchecking," Proc. Fifth Int'l Computer-Aided Verification Conf., Lecture Notes in Computer Science 697, pp. 463-478, Springer-Verlag, 1993.
[15] B.T. Hailpern,“Verifying concurrent processes using temporal logic,” Lecture Notes in Computer Science.New York: Springer-Verlag, 1982.
[16] G.J. Holzmann,“Algorithms for automated protocol verification,” AT&T Technical J., Jan./Feb. 1990.
[17] C.N. Ip and D.L. Dill,“Efficient verification of symmetric concurrent systems,” IEEE Int’l Conf. Computer Design: VLSI Computers and Processors, Oct. 1993.
[18] C.N. Ip and D.L. Dill,“Better verification through symmetry,” Proc. 11th Int’l Symp. Computer Hardware Description Languages and Their Applications, pp. 87-100, Apr. 1993.
[19] Y. Kakuda,Y. Wakahara,, and M. Norigoe,“An acyclic expansion algorithm for fast protocol verification,” IEEE Trans. Software Engineering, vol. 14, no. 8, pp. 1,059-1,070, Aug. 1988.
[20] P. Loewenstein and D.L. Dill,“Verification of a multiprocessor cache protocol using simulation relations and higher-order logic,” Proc. Second Int’l Conf. Computer-Aided Verification, pp. 302-311, Springer-Verlag, June 1990.
[21] J.-C. Madre and J.-P. Billon,“Proving circuit correctness using formal comparison between expected and extracted behavior,” Proc. 25th ACM/IEEE Design Automation Conf., pp. 205-210, 1988.
[22] K.L. McMillan and J. Schwalbe,“Formal verification of the Gigamax cache consistency protocol,” Proc. ISSM Int’l Conf. Parallel and Distributed Computing, Oct. 1991.
[23] A.K. Nanda and L.N. Bhuyan,“A formal specification and verification technique for cache coherence protocols,” Proc. 1992 Int’l Conf. Parallel Processing, pp. I-22-I-26, 1992.
[24] M. Paramarcos and J. Patel,“A low-overhead coherence solution for multiprocessors with private cache memories,” Proc. 11th Int’l Symp. Computer Architecture, pp. 348-354, June 1984.
[25] F. Pong and M. Dubois,“The verification of cache coherence protocols,” Proc. Fifth Ann. Symp. Parallel Algorithm and Architecture, pp. 11-20, June 1993.
[26] F. Pong,P. Stenström,, and M. Dubois,“An integrated methodology for the verification of directory-based cache protocols,” Proc. 1994 Int’l Conf. Parallel Processing, pp. I-158-I-165, 1994.
[27] F. Pong,A. Nowatzyk,G. Aybay,, and M. Dubois,“Verification of S3.mp-A case study of distributed directory-based cache coherence protocol,” EUROPAR’95. to appear.
[28] F. Pong,“Symbolic state model: A new approach for the verification of cache coherence protocols,” PhD dissertation, Dept of Electrical Engineering-Systems, Univ. of Southern California, Los Angeles, Aug. 1995.
[29] L. Rudolph and Z. Segall,“Dynamic decentralized cache schemes for mimd parallel processors,” Proc. Int’l Symp. Computer Architecture, pp. 340-347, 1984.
[30] P. Zafiropulo,C.H. West,H. Rudin,D.D. Cowan,, and D. Brand,“Towards analyzing and synthesizing protocols,” IEEE Trans. Comm., vol. 28, no. 4, pp. 651-660, Apr. 1980.

Index Terms:
Cache coherence protocol, formal verification, finite state machine, symbolic expansion, shared-memory multiprocessor.
Citation:
Fong Pong, Michel Dubois, "A New Approach for the Verification of Cache Coherence Protocols," IEEE Transactions on Parallel and Distributed Systems, vol. 6, no. 8, pp. 773-787, Aug. 1995, doi:10.1109/71.406955
Usage of this product signifies your acceptance of the Terms of Use.