This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Design Verification of the S3.mp Cache-Coherent Shared-Memory System
January 1998 (vol. 47 no. 1)
pp. 135-140

Abstract—This paper describes the methods used to formulate and validate the memory subsystem of the cache-coherent Sun Scalable Shared-memory MultiProcessor (S3.mp) at three levels of abstraction: the memory consistency model, the cache coherence protocol, and the implementation.

[1] S.V. Adve and K. Gharachorloo, "Shared Memory Consistency Models: A Tutorial," Computer, Dec. 1996, pp. 66-76.
[2] M. Brorsson, F. Dahlgren, H. Nilsson, and P. Stenström, "The CacheMire Test Bench_A Flexible and Effective Approach for Simulation of Multiprocessors," Proc. 26th Ann. Simulation Symp., pp. 41-49, 1993.
[3] L.M. Censier and P. Feautrier, "A New Solution to Coherence Problems in Multicache Systems," IEEE Trans. Computers, vol. 27, no. 12, pp. 1,112-1,118, Dec. 1978.
[4] S. Chandra, B. Richards, and J.R. Larus, "Teapot: Language Support for Writing Memory Coherence Protocols," Proc. SIGPLAN Conf. Programming Language Design and Implementation, May 1996.
[5] 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.
[6] M. Galles and E. Williams, "Performance Optimizations, Implementation, and Verification of the SGI Challenge Multiprocessor," Proc. 27th Ann. Hawaii Int'l Conf. System Sciences, 1994.
[7] C.N. Ip and D.L. Dill, "Verifying Systems with Replicated Components in Mur$\varphi,$" Proc. Int'l Conf. Computer-Aided Verification, 1996.
[8] D. Lenoski et al., "The directory-based cache coherence protocol for the dash multiprocessor," Proc. 17th Int'l Symp. Computer Architecture,Los Alamitos, Calif., pp. 148-159, 1990.
[9] D. Marr et al., "Multiprocessor Validation of the Pentium Pro Microprocessor," Computer, Vol. 29, No. 11, Nov. 1996, pp 47-53.
[10] T. Nipkow, "Formal Verification of Data Type Refinement—Theory and Practice," Lecture Notes in Computer Science, vol. 430, pp. 561-591. Springer-Verlag, May/June 1989.
[11] A. Nowatzyk, G. Aybay, M. Browne, E. Kelly, M. Parkin, B. Radke, and S. Vishin, "The S3.mp Scalable Shared Memory Multiprocessor," Proc. Int'l Conf. Parallel Processing, 1995.
[12] A. Nowatzyk, G. Aybay, M. Browne, E. Kelly, M. Parkin, B. Radke, and S. Vishin, "Exploiting Parallelism in Cache Coherency Protocol Engines," Proc. First Int'l EURO-PAR Conf., pp. 269-286, Aug. 1995.
[13] F. Pong and M. Dubois, "A New Approach for the Verification of Cache Coherence Protocols," IEEE Trans. Parallel and Distributed Systems, vol. 6, no. 8, pp. 773-787, Aug. 1995.
[14] F. Pong, A. Nowatzyk, G. Aybay, and M. Dubois, "Verifying Distributed Directory-based Cache Coherence Protocols: S3.mp, a Case Study," Proc. First Int'l EURO-PAR Conf., pp. 287-300, Aug. 1995.
[15] F. Pong and M. Dubois, “Verification Techniques for Cache Coherence Protocols,” ACM Computing Surveys, vol. 29, no. 1, pp. 82-126, Mar. 1997.
[16] F. Pong and M. Dubois, "A New Approach for the Verification of Cache Coherence Protocols," IEEE Trans. Parallel and Distributed Systems, vol. 6, no. 8, pp. 773-787, Aug. 1995.
[17] C. Scheurich, "Access Ordering and Coherence in Shared Memory Multiprocessors," PhD thesis, Univ. of Southern California, 1989.
[18] J.P. Singh, W.D. Weber, and A. Gupta, "SPLASH: Stanford Parallel Applications for Shared Memory," Proc. 19th Annual Int'l Symp. Computer Architecture, IEEE CS Press, Los Alamitos, Calif., May 1992, pp. 5-14.
[19] P. Stenström, "A Survey of Cache Coherence Scheme for Multiprocessors," Computer, vol. 23, no. 6, pp. 12-24, Jun.e 1990.
[20] D.L. Weaver and T. Germond, The Sparc Architecture Manual, Version 9, Prentice Hall, Englewood Cliffs, N.J., 1994.
[21] 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.

Index Terms:
Cache-coherent shared-memory multiprocessors, distributed directory-based protocols, formal verification, debugging.
Citation:
Fong Pong, Michael Browne, Günes Aybay, Andreas Nowatzyk, Michel Dubois, "Design Verification of the S3.mp Cache-Coherent Shared-Memory System," IEEE Transactions on Computers, vol. 47, no. 1, pp. 135-140, Jan. 1998, doi:10.1109/12.656100
Usage of this product signifies your acceptance of the Terms of Use.