Abstract

The cache coherence protocol is an important but notoriously complicated part of a multicore processor. Typical protocols are far too complicated to verify completely and thus industry relies on extensive testing in hopes of uncovering bugs. In this work, we propose a verification-aware approach to protocol design, in which we design scalable protocols such that they can be completely formally verified. We present three design methodologies that, if followed, facilitate verification of arbitrarily scaled protocols. Two of these methodologies are compatible with prior verification techniques, and the third is based on a new theoretical framework that we have developed. We discuss the impact of the constraints that must be followed, and we highlight possible future directions in verification-aware microarchitecture.

Daniel J. Sorin is the W.H. Gardner Jr. Professor of Electrical and Computer Engineering at Duke University. His research interests are in computer architecture, with a focus on fault tolerance, verification, and robotics. He is the author of “Fault Tolerant Computer Architecture” and a co-author of “A Primer on Memory Consistency and Cache Coherence.” He is the recipient of an NSF Career Award and Duke’s Imhoff Distinguished Teaching Award. He received a PhD in electrical and computer engineering from the University of Wisconsin—Madison.