BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Designing Verifiable Cache Coherence Protocols - Daniel Sorin\, Du
 ke University
DTSTART:20171110T130000Z
DTEND:20171110T140000Z
UID:TALK73148@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:The cache coherence protocol is an important but notoriously\n
 complicated part of a multicore processor.  Typical protocols are far\ntoo
  complicated to verify completely and thus industry relies on\nextensive t
 esting in hopes of uncovering bugs.  In this work\, we\npropose a verifica
 tion-aware approach to protocol design\, in which we\ndesign scalable prot
 ocols such that they can be completely formally\nverified.  We present thr
 ee design methodologies that\, if followed\,\nfacilitate verification of a
 rbitrarily scaled protocols. Two of these\nmethodologies are compatible wi
 th prior verification techniques\, and\nthe third is based on a new theore
 tical framework that we have\ndeveloped.  We discuss the impact of the con
 straints that must be\nfollowed\, and we highlight possible future directi
 ons in\nverification-aware microarchitecture.\n\nDaniel J. Sorin is the W.
 H. Gardner Jr. Professor of Electrical and\nComputer Engineering at Duke U
 niversity.  His research interests are\nin computer architecture\, with a 
 focus on fault tolerance\,\nverification\, and robotics.  He is the author
  of "Fault Tolerant\nComputer Architecture" and a co-author of "A Primer o
 n Memory\nConsistency and Cache Coherence."  He is the recipient of an NSF
 \nCareer Award and Duke's Imhoff Distinguished Teaching Award.  He\nreceiv
 ed a PhD in electrical and computer engineering from the\nUniversity of Wi
 sconsin--Madison.\n
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR