Verification of a lazy cache coherence protocol against a weak memory model
Logic in Computer Science
2017-05-24 v1
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.
Cite
@article{arxiv.1705.08262,
title = {Verification of a lazy cache coherence protocol against a weak memory model},
author = {Christopher J. Banks and Marco Elver and Ruth Hoffmann and Susmit Sarkar and Paul Jackson and Vijay Nagarajan},
journal= {arXiv preprint arXiv:1705.08262},
year = {2017}
}
Comments
10 pages