Hemiola: Structural Design and Proof of Cache-Coherence Protocols
A Coq framework for structural design and proof of hierarchical cache-coherence protocols
We've been developing a framework called Hemiola, a Coq framework to design and prove hierarchical cache-coherence protocols in a very structured way.
The key technique used for the proof is serializability; Hemiola as a proof framework guarantees that any cache-coherence protocols designed within the Hemiola DSL satisfy serializability by construction. Using serializability, most difficult invariant proofs can be done against a model where memory accesses come one-at-a-time.
If you would like to contact us about our work, please refer to our members below and reach out to one of the group leads directly.