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

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

doi:10.23919/FMCAD.2017.8102242

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 proceeding › Conference contribution

Abstract / Description of output

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.

Original language	English
Title of host publication	The 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017)
Place of Publication	Vienna, Austria
Publisher	FMCAD Inc
Pages	60-67
Number of pages	8
ISBN (Print)	978-0-9835678-7-5
DOIs	https://doi.org/10.23919/FMCAD.2017.8102242
Publication status	Published - 2 Oct 2017
Event	17th Conference on Formal Methods in Computer-Aided Design - Vienna, Austria Duration: 2 Oct 2017 → 6 Oct 2017 https://www.cs.utexas.edu/~hunt/fmcad/FMCAD17/

Conference

Conference	17th Conference on Formal Methods in Computer-Aided Design
Abbreviated title	FMCAD 2017
Country/Territory	Austria
City	Vienna
Period	2/10/17 → 6/10/17
Internet address	https://www.cs.utexas.edu/~hunt/fmcad/FMCAD17/

Access to Document

10.23919/FMCAD.2017.8102242

paper-FMCAD-1Accepted author manuscript, 288 KB

Cite this

@inproceedings{0f61a19cd8b047a892c24ec4228afc0c,

title = "Verification of a lazy cache coherence protocol against a weak memory model",

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.",

author = "Christopher Banks and Marco Elver and Ruth Hoffmann and Susmit Sarkar and Paul Jackson and Vijay Nagarajan",

year = "2017",

month = oct,

day = "2",

doi = "10.23919/FMCAD.2017.8102242",

language = "English",

isbn = "978-0-9835678-7-5",

pages = "60--67",

booktitle = "The 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017)",

publisher = "FMCAD Inc",

note = "17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017 ; Conference date: 02-10-2017 Through 06-10-2017",

url = "https://www.cs.utexas.edu/~hunt/fmcad/FMCAD17/",

}

Banks, C, Elver, M, Hoffmann, R, Sarkar, S, Jackson, P & Nagarajan, V 2017, Verification of a lazy cache coherence protocol against a weak memory model. in The 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017). FMCAD Inc, Vienna, Austria, pp. 60-67, 17th Conference on Formal Methods in Computer-Aided Design, Vienna, Austria, 2/10/17. https://doi.org/10.23919/FMCAD.2017.8102242

TY - GEN

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

AU - Banks, Christopher

AU - Elver, Marco

AU - Hoffmann, Ruth

AU - Sarkar, Susmit

AU - Jackson, Paul

AU - Nagarajan, Vijay

PY - 2017/10/2

Y1 - 2017/10/2

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

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

UR - https://arxiv.org/abs/1705.08262

UR - http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/accepted/

U2 - 10.23919/FMCAD.2017.8102242

DO - 10.23919/FMCAD.2017.8102242

M3 - Conference contribution

SN - 978-0-9835678-7-5

SP - 60

EP - 67

BT - The 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017)

PB - FMCAD Inc

CY - Vienna, Austria

T2 - 17th Conference on Formal Methods in Computer-Aided Design

Y2 - 2 October 2017 through 6 October 2017

ER -

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

Abstract / Description of output

Conference

Access to Document

Other files and links

Fingerprint

C3- Scalable & Verified Shared Memory via Consistency-directed Cache Coherence

Paul Jackson

Cite this

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

Abstract / Description of output

Conference

Access to Document

Other files and links

Fingerprint

Projects

C3- Scalable & Verified Shared Memory via Consistency-directed Cache Coherence

Profiles

Paul Jackson

Cite this