This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol
June 2002 (vol. 13 no. 6)
pp. 556-578

In this paper, we develop a specification methodology that documents and specifies a cache coherence protocol in eight tables: the states, events, actions, and transitions of the cache and memory controllers. We then use this methodology to specify a detailed, modern three-state broadcast snooping protocol with an unordered data network and an ordered address network that allows arbitrary skew. We also present a detailed specification of a new protocol called Multicast Snooping and, in doing so, we better illustrate the utility of the table-based specification methodology. Finally, we demonstrate a technique for verification of the Multicast Snooping protocol, through the sketch of a manual proof that the specification satisfies a sequentially consistent memory model.

[1] D. Abts, D.J. Lilja, and S. Scott, “Toward Complexity-Effective Verification: A Case Study of the Cray SV2 Cache Coherence Protocol,” Proc. 27th Int'l Symp. Computer Architecture Workshop Complexity-Effective Design, June 2000.
[2] S.V. Adve, Designing Memory Consistency Models for Shared Memory Multiprocessors, doctoral dissertation, CS Dept., Univ. Wisconsin-Madison, Nov. 1993.
[3] Y. Afek, G. Brown, and M. Merritt, “Lazy Caching,” ACM Trans. Programming Languages and Systems, vol. 15, no. 1, pp. 182-205, Jan. 1993.
[4] H. Akhiani, D. Doligez, P. Harter, L. Lamport, J. Scheid, M. Tuttle, and Y. Yu, “Cache Coherence Verification with TLA+,” FM '99-Formal Methods, Volume II, 1999.
[5] 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.
[6] E.E. Bilir, R.M. Dickson, Y. Hu, M. Plakal, D.J. Sorin, M.D. Hilland, D.A. Wood, “Multicast Snooping: A New Coherence Method Using a Multicast Address Network,” Proc. 26th Ann. Int'l Symp. Computer Architecture, pp. 294-304, May 1999.
[7] A.E. Condon, M.D. Hill, M. Plakal, and D.J. Sorin, “Using Lamport Clocks to Reason About Relaxed Memory Models” Proc. Fifth IEEE Symp. High-Performance Computer Architecture, pp. 270-278, Jan. 1999.
[8] D.E. Culler and J.P. Singh, Parallel Computer Architecture: A Hardware/Software Approach. Morgan Kaufmann, 1999.
[9] A. Eiriksson, A. Silbey, S. Venkataraman, and M. Woodacre, “Origin System Design Methodology and Experience: 1M-Gate ASICs and Beyond,” Proc. COMPCON '97, 1997.
[10] A.T. Eiriksson and K.L. McMillan, “Using Formal Verification/Analysis Methods on the Critical Path in Systems Design: A Case Study,” Proc. Computer Aided Verification Conf., pp. 367-380, 1995.
[11] S.J. Frank, “Tightly Coupled Multiprocessor System Speeds Memory-access Times,” Electronics, vol. 57, no. 1, pp. 164-169, Jan. 1984.
[12] K. Gharachorloo, Memory Consistency Models for Shared Memory Multiprocessors, doctoral dissertation, Computer Systems Laboratory, Stanford University, Stanford Calif. Dec. 1995.
[13] R. Ghughal, A. Mokkedem, R. Nalumasu, and G. Gopalakrishnan, “Using `Test Model-Checking' to Verify the Runway-PA800 Memory Model,” Proc. 10th ACM Symp. Parallel Algorithms and Architectures, pp. 231-239, June 1998.
[14] P.B. Gibbons, M. Merritt, and K. Gharachorloo, “Proving Sequential Consistency of High-Performance Shared Memories,” Proc. Third ACM Symp. Parallel Algorithms and Architectures, pp. 292-303, July 1991.
[15] J. Hennessy and D. Patterson, Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1995.
[16] T.A. Henzinger, S. Qadeer, and S.K. Rajamani, “Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems,” Lecture Notes in Computer Science, pp. 301-315, 1999.
[17] M.D. Hill, A.E. Condon, M. Plakal, and D.J. Sorin, “A System-Level Specification Framework for I/O Architectures,” Proc. 11th ACM Symp. Parallel Algorithms and Architectures, pp. 138-147, June 1999.
[18] J.E. Hopcroft and J.D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Apr. 1979.
[19] S.D. Johnson, “A Tabular Language for System Design,” Proc. Fourth NASA Langley Formal Methods Workshop, Sept. 1997.
[20] L. Lamport, "Time, clocks and the ordering of events in a distributed system," Comm. ACM, vol. 21, no. 7, pp. 558-565, July 1978.
[21] L. Lamport, “How to Make a Multiprocessor Computer that Correctly Executes Multiprocess Programs,” IEEE Trans. Computers, vol. 28, no. 9, pp. 690-691, Sept. 1979.
[22] R. Nalumasu, R. Ghughal, A. Mokkedem, and G. Gopalakrishnan, “The `Test Model-checking' Approach to the Verification of Formal Memory Models of Multiprocessors,” Proc. Computer Aided Verification, 10th Int'l Conf., A.J. Hu and M.Y. Vardi, eds., pp. 464-476, June 1998.
[23] S. Park and D.L. Dill, “An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order),” Proc. Seventh ACM Symp. Parallel Algorithms and Architectures, pp. 34-41, July 1995.
[24] S. Park and D.L. Dill, “Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions,” Proc. Eighth ACM Symp. Parallel Algorithms and Architectures, pp. 288-296, June 1996.
[25] M. Plakal, D.J. Sorin, A.E. Condon, and M.D. Hill, “Lamport Clocks: Verifying a Directory Cache-Coherence Protocol,” Proc. 10th ACM Symp. Parallel Algorithms and Architectures, pp. 67-76, June 1998.
[26] F. Pong, M. Browne, A. Nowatzyk, and M. Dubois, “Design Verification of the S3.mp Cache-Coherent Shared-Memory System,” IEEE Trans. Computers, vol. 47, no. 1, pp. 135-140, Jan. 1998.
[27] F. Pong and M. Dubois, “Verification Techniques for Cache Coherence Protocols,” ACM Computing Surveys, vol. 29, no. 1, pp. 82-126, Mar. 1997.
[28] F. Pong and M. Dubois, “Formal Automatic Verification of Cache Coherence in Multiprocessors with Relaxed Memory Models,” IEEE Trans. Parallel and Distributed Systems, vol. 11, no. 9, pp. 989-1006, Sept. 2000.
[29] S. Qadeer, “On the Verification of Memory Models of Shared-Memory Multiprocessors,” Proc. Tutorial and Workshop on Formal Specification and Verification Methods for Shared Memory Systems, Oct. 2000.
[30] X. Shen and Arvind, “Specification of Memory Models and Design of Provably Correct Cache Coherence Protocols,” Group Memo 398, Mass. Inst. of Tech nology, June 1997.
[31] D.J. Sorin, M. Plakal, M.D. Hill, and A.E. Condon, “Lamport Clocks: Reasoning About Shared-Memory Correctness,” Technical Report CS-TR-1367, Univ. of Wisconsin-Madison, Mar. 1998.
[32] P. Sweazey and A.J. Smith, “A Class of Compatible Cache Consistency Protocols and their Support by the IEEE Futurebus,” Proc. 13th Ann. Int'l Symp. Computer Architecture, pp. 414-423, June 1986.
[33] D.A. Wood, G.A. Gibson, and R.H. Katz, “Verifying a Multiprocessor Cache Controller Using Random Test Generation,” IEEE Design and Test of Computers, Aug. 1990.
[34] Y. Yu and M. Tuttle, “Analyzing Cache Coherence with TLA+,” Proc. Tutorial and Workshop on Formal Specification and Verification Methods for Shared Memory Systems, Oct. 2000.

Index Terms:
Cache coherence, protocol specification, protocol verification, memory consistency, multicast snooping.
Citation:
Daniel J. Sorin, Manoj Plakal, Anne E. Condon, Mark D. Hill, Milo M.K. Martin, David A. Wood, "Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol," IEEE Transactions on Parallel and Distributed Systems, vol. 13, no. 6, pp. 556-578, June 2002, doi:10.1109/TPDS.2002.1011412
Usage of this product signifies your acceptance of the Terms of Use.