So many states, so little time: Verifying memory coherence in the Cray X1

Dennis Abts, Steve Scott, David J. Lilja

Research output: Chapter in Book/Report/Conference proceedingConference contribution

42 Scopus citations

Abstract

This paper investigates a complexity-effective technique for verifying a highly distributed directory-based cache coherence protocol. We develop a novel approach called "witness strings" that combines both formal and informal verification methods to expose design errors within the cache coherence protocol and its Verilog implementation. In this approach a formal execution trace is extracted during model checking of the architectural model and re-encoded to provide the input stimulus for a logic simulation of the corresponding Verilog implementation. This approach brings confidence to system architects that the logic implementation of the coherence protocol conforms to the architectural model. The feasibility of this approach is demonstrated by using it to verify the cache coherence protocol of the Cray X1. Using this approach we uncovered three architectural protocol errors and exposed several implementation errors by replaying the witness strings on the Verilog implementation.

Original languageEnglish (US)
Title of host publicationProceedings - International Parallel and Distributed Processing Symposium, IPDPS 2003
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)0769519261, 9780769519265
DOIs
StatePublished - Jan 1 2003
EventInternational Parallel and Distributed Processing Symposium, IPDPS 2003 - Nice, France
Duration: Apr 22 2003Apr 26 2003

Publication series

NameProceedings - International Parallel and Distributed Processing Symposium, IPDPS 2003

Other

OtherInternational Parallel and Distributed Processing Symposium, IPDPS 2003
CountryFrance
CityNice
Period4/22/034/26/03

Fingerprint Dive into the research topics of 'So many states, so little time: Verifying memory coherence in the Cray X1'. Together they form a unique fingerprint.

Cite this