CSE
CSE
CSE CSE


CSE Seminar or Event

Architecting Formally Verifiable Systems Protocols

Luwa Matthews


Ph.D. Candidate
Duke University
 
Wednesday, January 11, 2017
12:00pm - 1:00pm
3725 BBB

Add to Google Calendar

About the Event

Model checking is the widely used technique for formally verifying protocols because it is simple and automated. Unfortunately, due to the well-known state explosion problem, model checkers can typically only verify an industrial-strength protocol for a small scale. This provides strong motivation for architects to design protocols specifically to enable their scalable verification.

To this end, we present a formal framework that enables architects to compose pre-verified protocols into hierarchies of arbitrary sizes and configurations such that the composite is guaranteed to behave correctly. To achieve this, we formalize a class of finite state machines such that, given the correctness of certain basic components, any member of this class behaves correctly for arbitrary scales. Membership in this class naturally lends itself to scalable automated proofs. We believe our framework is applicable to a wide range of protocols, including cache coherence, dynamic power management, and distributed lock management protocols. With completely automated tools, we use our framework to design and verify a hierarchical MESI coherence protocol correct for any arbitrary size or configuration, which we believe is the first such protocol.

Biography

Luwa Matthews is a Ph.D. Candidate in the department of Electrical and Computer Engineering at Duke University. He is in his fifth year and is advised by Professor Daniel Sorin. His research interests lie in the general area of computer architecture and, more specifically, verification-aware protocol design, including cache coherence, power management, and other systems protocols. He received his B.A. in Computer Science, Mathematics, and Physics from Luther College in May 2012 and his M.S. in Computer Science from Duke University in May 2015.

Additional Information

Sponsor(s): CSE

Open to: Public