PVCoherence: Designing flat coherence protocols for scalable verification

Conference Paper

The goal of this work is to design cache coherence protocols with many cores that can be verified with state-of-the-art automated verification methodologies. In particular, we focus on flat (non-hierarchical) coherence protocols, and we use a mostly-automated methodology based on parametric verification (PV). We propose several design guidelines that architects should follow if they want to design protocols that can be parametrically verified. We experimentally evaluate performance, storage overhead, and scalability of a protocol verified with PV compared to a highly optimized protocol that cannot be verified with PV. © 2014 IEEE.

Full Text

Duke Authors

Cited Authors

  • Zhang, M; Bingham, JD; Erickson, J; Sorin, DJ

Published Date

  • 2014

Published In

Start / End Page

  • 392 - 403

Published By

International Standard Serial Number (ISSN)

  • 1530-0897

International Standard Book Number 13 (ISBN-13)

  • 9781479930975

Digital Object Identifier (DOI)

  • 10.1109/HPCA.2014.6835949