| 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.;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.;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. |
