Cache Coherence Protocol Verification using Ωmega

We verify some correctness properties of the DASH cache coherence protocol using Ωmega. Ωmega is a language with a rich type system featuring GADTs, type functions, and user-guided type checking rules. Cache coherence protocols have both safety properties and liveness properties. We show how to describe some of the safety properties of DASH cache coherence protocol in mega. Since liveness properties are not easily expressed by types, we investigate invariants sufficient to imply some of the liveness properties of concern, and assert those invariants as well in the type system of Ωmega. Using Ωmega, we can have both a working program and an automatically checked proof of its properties because Ωmega is both a programming language and a logic. Tightly coupled programs and their properties using types guides us both in the construction of the program and in strategies for modification that preserves the essential properties