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

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 unbounded 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.

I. Introduction

In parallel architectures with local caches, cached values can become stale. Therefore, it is imperative that the system guarantees shared memory correctness by ensuring that it correctly implements a memory consistency model (MCM)-the formal model that determines what value a read should return [1]. An integral component of enforcing an MCM is the cache coherence protocol (CCP), which is responsible for making writes visible to other caches in an order that is consistent with the MCM.