Download PDFOpen PDF in browser

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

EasyChair Preprint 8623

21 pagesDate: August 9, 2022

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@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}}
Download PDFOpen PDF in browser