Architecting hierarchical coherence protocols for push-button parametric verification


Conference Paper

© 2017 Association for Computing Machinery. Recent work in formal verification theory and verification-aware design has sought to bridge the divide between the class of protocols architects want to design and the class of protocols that are verifiable with state of the art tools. Particularly, the recent Neo work in formal verification theory, for the first time, formalizes how to compose flat subprotocols with an arbitrary number of nodes into a hierarchy while maintaining correct behavior. However, it is unclear if this theory scales to realistic systems. Moreover, there is a diversity of systems architects would be interested in, to which it is not clear if the theory applies. In this paper, we show how the abstract Neo theory can be leveraged to design a realistic hierarchical coherence protocol. As such, we present the first realistic hierarchical coherence protocol verified with fully-automated (push-button) verification tools for all scales and tree configurations. We explore the practical limitations posed by both the theory and the verification tools in designing this verifiable hierarchical protocol. We experimentally evaluate our protocol, comparing it to more complex protocols that have optimizations prohibited by the theory and verification tool. Finally, we discuss how a variety of system configurations and protocols architects might be interested in can be adapted to the Neo theory, which we hope opens up the theory to future work in verificationaware protocol design.

Full Text

Duke Authors

Cited Authors

  • Matthews, O; Sorin, DJ

Published Date

  • October 14, 2017

Published In

Volume / Issue

  • Part F131207 /

Start / End Page

  • 477 - 489

International Standard Serial Number (ISSN)

  • 1072-4451

International Standard Book Number 13 (ISBN-13)

  • 9781450349529

Digital Object Identifier (DOI)

  • 10.1145/3123939.3123971

Citation Source

  • Scopus