Graphics enhanced version of this site

Verifying Distributed Directory-based Cache Coherency Protocols: S3.mp, a Case Study
F. Pong, A. Nowatzyk, G. Aybay, and M. Dubois
EuroPar'95, August, 1995.

Jump to: Download | Abstract | Notes | Text Reference | BibTeX Reference

Adobe portable document format (pdf) [123 KB]
Compressed postscript (ps.gz) [49 KB]

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

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.

Number of pages: 12

F. Pong, A. Nowatzyk, G. Aybay, and M. Dubois, "Verifying Distributed Directory-based Cache Coherency Protocols: S3.mp, a Case Study," EuroPar'95, August, 1995.

@inproceedings{Pong_1995_4941,
   author = "F. Pong and Andreas Nowatzyk and G. Aybay and M. Dubois",
   title = "Verifying Distributed Directory-based Cache Coherency Protocols: S3.mp, a Case Study",
   booktitle = "EuroPar'95",
   month = "August",
   year = "1995"
}