Parameterized verification of deadlock freedom in symmetric cache coherence protocols

An important problem in the verification of hardware protocols is that of proving deadlock freedom. We view deadlock freedom as the property that for all reachable states, there exists some path to a quiescent state, i.e. one wherein all resources of interest are free and thus all prior requests have been resolved. We establish a framework for showing this property in a class of symmetric parameterized systems. Our approach is based on a mixed abstraction system than includes both an over-approximate and an under-approximate transition relation. Model checking is employed to compute all states reachable through overapproximate transitions, and from each of these states finds a path of underapproximate transitions to a quiescent state. When this fails because the under-approximation is too strong, we provide techniques to suggest additional transitions that can be introduced to soundly weaken the under-approximation. This approach can be viewed as an extension of the well-known approach of guard strengthening for verifying state invariants of parameterized systems. We present proof of deadlock freedom of the German and FLASH cache-coherence protocols as case studies using a semi-automated heuristic tool that mitigates the human effort.