PV1 Hemiolaframework for designing protocols without inconsistent interleavings

Application domain/field

Type of tool


Expected input

Single-cache-line protocol


Hemiola's domain-specific language

Expected output

? (depends on the analysis chosen: Coq proof, simulation or synthesis)


Hemiola is a framework embedded in Coq. It can be used to design protocols "that never experience inconsistent interleavings while handling transactions concurrently". It provides a domain-specific language for designing cache-coherence protocols. The framework seems to provide the following options:
Concurrency Framework Hardware Protocol Simulation Synthesis


- Repository: https://github.com/mit-plv/hemiola

Related papers

https://doi.org/10.1007/978-3-031-13188-2_16 (CAV 2022)

Last publication date

6 August 2022

Related tools

Rule-based hardware language: Bluespec

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.