Deadlock Verification of Cache Coherence Protocols and Communication Fabrics

Cache coherence plays a major role in manycore systems. The verification of deadlocks is a challenge in particular, because deadlock freedom is an emerging property. Formal methods often decouple verification of the protocol from verification of the communication interconnect. Modern communication fabrics, however, become more advanced and include a network topology, routing, arbitration, synchronization, and more. In this paper, an integrated approach is proposed that allows cross-layer verification of both the cache coherence protocol and the communication fabric all at once. An automated methodology for deriving cross-layer invariants is proposed. These invariants relate the state of the application-layer protocols to en route packets in the communication fabric. Using the invariants, we derive formal proofs of deadlock-freedom for two case studies: a directory-based MI protocol in a 2D mesh, and a ring-based snoopy protocol in a 2D torus. Additionally, we show that our methodology can be used to derive the smallest possible queue sizes that ensure absence of deadlocks. Our methodology is generally applicable and shows promising scalability.