Abstract
This paper presents the results for the verification of the S3.mp cache coherence protocol. The S3.mp protocol uses a distributed directory with limited number of pointers and hardware supported overflow handling that keeps processing nodes sharing a data block in a singly linked list. The complexity of the protocol is high and its validation is challenging because of the distributed algorithm used to maintain the linked lists and the non-FIFO network. We found several design errors, including an error which only appears in verification models of more than three processing nodes, which is very unlikely to be detected by intensive simulations. We believe that methods described in this paper are applicable to the verification of other linked list based protocols such as the IEEE Scalable Coherent Interface.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adve, S.V. and Hill, M.D., “Weak Ordering—A New Definition”, Proc. of the 17th Int'l Symposium on Computer Architecture, May 1990, pp.2–14.
Archibald, J., “The Cache Coherence Problem in Shared-Memory Multiprocessors”, Ph.D Dissertation, University of Washington, Feb. 1987.
Collier, W.W., Reasoning About Parallel Architectures, Prentice Hall, Englewood Cliffs, New Jersey.
Dill, D.L., Drexler, A.J., Hu, A.J. and Yang, C.H., “Protocol Verification as a Hardware Design Aid”, Int'l Conf. on Computer Design: VLSI in Computers and Processors, pp. 522–525, Oct. 1992.
Holzmann, G.J., “Algorithms for Automated Protocol Verification”, AT&T Technical Journal, Jan./Feb. 1990.
Ip, C.N. and Dill, D.L., “Better Verification Through Symmetry”, Proc. 11th Int'l Symp. on Computer Hardwae Description Languages and Their Applications, pp. 87–100, Apr. 1993.
James et al., “Scalable Coherent Interface”, IEEE Computer, June 90, Vol 23, No. 6, pp 71–82.
Lamport, L., “How to Make a Multiprocessor Computer that Correctly Executes Multiprocess Programs”, IEEE Trans. on Computers, Vol. C-28, No.9, Sept. 1979, pp.690–691.
Lenosky, D., et al., “The Directory-Based Cache Coherence Protocol for the DASH Multiprocessor”, Proc. of the 17th Int'l Symposium on Computer Architecture, June 1990, pp. 148–159.
McMillan, K.L. and Schwalbe, J., “Formal Verification of the Gigamax Cache Consistency Protocol”, Proc. of the ISSM Int'l Conf. on Parallel and Distributed Computing, Oct. 1991.
Nowaztyk, A. and Parkin, M., “The S3.mp Interconnection System and TIC Chip”, Hot Interconnects 1993.
Nowatzyk, A., Aybay, G., Browne, M., Kelly, E., Parkin, M., Radke, B. and Vishin, S., “The S3.mp Scalable Shared Memory Multiprocessor”, HICCS, 1994.
Pong, F. and Dubois, M., “The Verification of Cache Coherence Protocols”, Proc. of the 5th Annual Symp. on Parallel Algorithm and Architecture, pp.11–20, June 1993.
Pong, F. and Dubois, M., “Formal Verification of Complex Coherence Protocols Using Symbolic State Models”, Technical Report CENG-94-01, University of Southern California.
Sindhu, P.S., Frailong, J-M. and Cekleov, M., “Formal Specification of Memory Models”, In Dubois, M. and Thakkar, S., Editors. Scalable Shared Memory Multiprocessors. Kluwer, Norwell, MA, 1992.
Stenström, P., “A Survey of Cache Coherence Schemes for Multiprocessors”, IEEE Computer, Vol. 23, No. 6, pp. 12–24, June 1990.
The SPARC Architecture Manual, Version 9, Prentice Hall.
Thapar, M. and Delagi, B., “Stanford Distributed-Directory Protocol”, IEEE Computer, June 1990, pp. 78–80.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pong, F., Nowatzyk, A., Aybay, G., Dubois, M. (1995). Verifying distributed directory-based cache coherence protocols: S3.mp, a case study. In: Haridi, S., Ali, K., Magnusson, P. (eds) EURO-PAR '95 Parallel Processing. Euro-Par 1995. Lecture Notes in Computer Science, vol 966. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020472
Download citation
DOI: https://doi.org/10.1007/BFb0020472
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60247-7
Online ISBN: 978-3-540-44769-6
eBook Packages: Springer Book Archive