PV1 ⊧ Hemiolaframework for designing protocols without inconsistent interleavings

Application domain/field

• Distributed systems
• Protocols
• Protocol design
• Proof assistant
• Hardware-description language
• Domain-specific language

Type of tool

Framework

Expected input

Single-cache-line protocol

Format:

Hemiola's domain-specific language

Expected output

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

Internals

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:

• Machine-check proofs with Coq
• Simulate a protocol
• Synthesize a protocol (by compiling the Hemiola program to Kami)