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

Christopher Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar, Paul Jackson, Vijay Nagarajan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 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.
Original languageEnglish
Title of host publicationProceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017)
EditorsDaryl Stewart, Georg Weissenbacher
PublisherFMCAD Inc
Pages60-67
ISBN (Print)9780983567875
Publication statusPublished - 2 Oct 2017
EventFormal Methods in Computer-Aided Design (FMCAD) - TU Wien, Vienna, Austria
Duration: 2 Oct 20176 Oct 2017
Conference number: 17
http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/

Conference

ConferenceFormal Methods in Computer-Aided Design (FMCAD)
Abbreviated titleFMCAD
Country/TerritoryAustria
CityVienna
Period2/10/176/10/17
Internet address

Fingerprint

Dive into the research topics of 'Verification of a lazy cache coherence protocol against a weak memory model'. Together they form a unique fingerprint.

Cite this