|
|
|
|
RI | Publications | Verifying Distributed Directory-based Cache Coherency Protocols: S3.mp, a Case Study
|
|
Text only 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
| Download [Help] |
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.
| 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.
| Notes |
Number of pages: 12
| Text Reference |
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.
| BibTeX Reference |
@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"
}