PVCoherence: Designing flat coherence protocols for scalable verification
| Title | PVCoherence: Designing flat coherence protocols for scalable verification |
| Publication Type | Conference Paper |
| Year of Publication | 2014 |
| Authors | Meng Zhang, Bingham, J.D., Erickson, J., Sorin, D.J. |
| Conference Name | High Performance Computer Architecture (HPCA), 2014 IEEE 20th International Symposium on |
| Date Published | Feb |
| Keywords | automated verification methodology, cache coherence protocol, cache storage, Coherence, Concrete, flat coherence protocol, formal verification, Guidelines, Manuals, memory protocols, model checking, Parametric statistics, parametric verification, Protocols, PVCoherence, scalable verification, storage overhead |
| Abstract | 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. |
| URL | https://ieeexplore.ieee.org/document/6835949 |
| DOI | 10.1109/HPCA.2014.6835949 |
| Citation Key | 6835949 |