Date/Time
Date(s) - 26/09/2017
2:00 pm - 3:00 pm
Location
University of St Andrews
SICSA is pleased to welcome DVF Professor Daniel J Sorin from Duke University who will be giving a talk on “Designing Formally Verifiable Cache Coherence Protocols” on Tuesday 26 September at the University of St Andrews (Room 1.33A Jack Cole Building).
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. Rather than innovate in verification techniques, we use existing verification techniques and innovate in the design of the protocols. We present two design methodologies that, if followed, facilitate verification of arbitrarily scaled protocols. We discuss the impact of the constraints that must be followed, and we highlight possible future directions in verification-aware microarchitecture.
Bio:
Daniel J. Sorin is the Addy Professor of Electrical and Computer Engineering at Duke University. His research interests are in computer architecture, with a focus on fault tolerance, verification, and memory system design. 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 a SICSA Distinguished Visiting Fellowship, a National Science Foundation Career Award, and Duke’s Imhoff Distinguished Teaching Award. He received a PhD and MS in electrical and computer engineering from the University of Wisconsin, and he received a BSE in electrical engineering from Duke University.
The host of this Distinguished Visitor is Vijay Nagarajan and the contact for this talk is Professor Susmit Sarkar
