Hemiola: Structural Design and Proof of 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.