Hemiola: a DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols

EasyChair Preprint 8623

Abstract

Cache-coherence protocols have been one of the greatest challenges in formal verification of hardware, due to their central complication of executing multiple memory-access transactions concurrently within a distributed message-passing system. In this paper, we introduce Harmony, a framework embedded in Coq that guides the user to design protocols that never experience inconsistent interleavings while handling transactions concurrently. The framework provides a DSL, where any protocol designed in the DSL always satisfies the serializability property, allowing a user to verify the protocol assuming that transactions are executed one-at-a-time. Harmony also provides a novel invariant proof method, for protocols designed in Harmony, that only requires considering execution histories without interleaved memory accesses. We used Harmony to design and prove hierarchical MSI and MESI protocols as case studies. We also demonstrated that the case-study protocols are hardware-synthesizable, by using a compilation/synthesis toolchain targeting FPGAs.

Keyphrases: Coq, Domain Specific Language, cache coherence, formal verification, hardware, proof assistants

@booklet{EasyChair:8623,
  author    = {Joonwon Choi and Adam Chlipala and Arvind},
  title     = {Hemiola: a DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols},
  howpublished = {EasyChair Preprint 8623},
  year      = {EasyChair, 2022}}