Show simple item record

A Formal Framework for Designing Verifiable Protocols

dc.contributor.advisor Sorin, Daniel J
dc.contributor.author Matthews, Opeoluwa
dc.date.accessioned 2018-03-20T17:53:14Z
dc.date.available 2018-03-20T17:53:14Z
dc.date.issued 2017
dc.identifier.uri https://hdl.handle.net/10161/16236
dc.description.abstract <p>Protocols play critical roles in computer systems today, including managing resources, facilitating communication, and coordinating actions of components. It is highly desirable to formally verify protocols, to provide a mathematical guarantee that they behave correctly. Ideally, one would pass a model of a protocol into a formal verification tool, push a button, and the tool uncovers bugs or certifies that the protocol behaves correctly. Unfortunately, as a result of the state explosion problem, automated formal verification tools struggle to verify the increasingly complex protocols that appear in computer systems today.</p><p>We observe that design decisions have a significant impact on the scalability of verifying a protocol in a formal verification tool. Hence, we present a formal framework that guides architects in designing protocols specifically to be verifiable with state of the art formal verification tools. If architects design protocols to fit our framework, the protocols inherit scalable automated verification. Key to our framework is a modular approach to constructing protocols from pre-verified subprotocols. We formulate properties that can be proven in automated tools to hold on these subprotocols, guaranteeing that any arbitrary composition of the subprotocols behaves correctly. The result is that we can design complex hierarchical (tree) protocols that are formally verified, using fully automated tools, for any number of nodes or any configuration of the tree. Our framework is applicable to a large class of protocols, including power management, cache coherence, and distributed lock management protocols.</p><p>To demonstrate the efficacy of our framework, we design and verify a realistic hierarchical (tree) coherence protocol, using a fully automated tool to prove that it behaves correctly for any configuration of the tree. We identify certain protocol optimizations prohibited by our framework or the state of the art verification tools and we evaluate our verified protocol against unverifiable protocols that feature these optimizations. We find that these optimizations have a negligible impact on performance. We hope that our framework can be used to design a wide variety of protocols that are verifiable, high-performing, and architecturally flexible.</p>
dc.subject Computer engineering
dc.subject Cache Coherence
dc.subject Formal Verification
dc.subject Model Checking
dc.subject Parameterized verification
dc.subject Protocols
dc.subject Verification-aware architecture
dc.title A Formal Framework for Designing Verifiable Protocols
dc.type Dissertation
dc.department Electrical and Computer Engineering


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record