University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Designing Verifiable Cache Coherence Protocols

Designing Verifiable Cache Coherence Protocols

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dominic Mulligan.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity