Verification of a lazy cache coherence protocol against a weak memory model

TL;DR

This paper verifies a lazy cache coherence protocol, TSO-CC, against the TSO memory model using a novel finite-state model and parameterisation, enabling scalable verification within a model checker.

Contribution

It introduces a weak simulation relation and a parameterisation technique for verifying TSO-CC against TSO for any number of processors.

Findings

Verification achieved within a model checker without external tools.

Scalable verification for unlimited processors.

Formal proof of TSO-CC's correctness against TSO.

Abstract

In this paper we verify a modern lazy cache coherence protocol, TSO-CC, against the memory consistency model it was designed for, TSO. We achieve this by first showing a weak simulation relation between TSO-CC (with a fixed number of processors) and a novel finite-state operational model which exhibits the laziness of TSO-CC and satisfies TSO. We then extend this by an existing parameterisation technique, allowing verification for an unlimited number of processors. The approach is executed entirely within a model checker, no external tool is required and very little in-depth knowledge of formal verification methods is required of the verifier.