Designing Verifiable Cache Coherence Protocols

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

• Daniel Sorin, Duke University
• Friday 10 November 2017, 13:00-14:00
• SS03, Computer Laboratory.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.