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

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

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

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

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017)
Editors	Daryl Stewart, Georg Weissenbacher
Publisher	FMCAD Inc
Pages	60-67
ISBN (Print)	9780983567875
Publication status	Published - 2 Oct 2017
Event	Formal Methods in Computer-Aided Design (FMCAD) - TU Wien, Vienna, Austria Duration: 2 Oct 2017 → 6 Oct 2017 Conference number: 17 http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/

Conference

Conference	Formal Methods in Computer-Aided Design (FMCAD)
Abbreviated title	FMCAD
Country/Territory	Austria
City	Vienna
Period	2/10/17 → 6/10/17
Internet address	http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/

Access to Document

FMCAD
Copyright © 2017, the Author(s) and FMCAD Inc. This work has been made available online in accordance with the publisher’s policies. This is the author created, accepted version manuscript following peer review and may differ slightly from the final published version.
Accepted author manuscript, 291 KB

https://dl.acm.org/citation.cfm?id=3168470

Cite this

@inproceedings{e54b2d29a2cd4588864d32a0b5dbcd41,

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

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

note = "Funding: EPSRC grant EP/M027317/1; Formal Methods in Computer-Aided Design (FMCAD), FMCAD ; Conference date: 02-10-2017 Through 06-10-2017",

year = "2017",

month = oct,

day = "2",

language = "English",

isbn = "9780983567875 ",

pages = "60--67",

editor = "Daryl Stewart and Georg Weissenbacher",

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

publisher = "FMCAD Inc",

url = "http://www.cs.utexas.edu/users/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 D Stewart & G Weissenbacher (eds), Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017). FMCAD Inc, pp. 60-67, Formal Methods in Computer-Aided Design (FMCAD), Vienna, Austria, 2/10/17. <https://dl.acm.org/citation.cfm?id=3168470>

Verification of a lazy cache coherence protocol against a weak memory model. / Banks, Christopher; Elver, Marco; Hoffmann, Ruth et al.
Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017). ed. / Daryl Stewart; Georg Weissenbacher. FMCAD Inc, 2017. p. 60-67.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

N1 - Conference code: 17

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

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

UR - https://www.scopus.com/pages/publications/85044646755

M3 - Conference contribution

SN - 9780983567875

SP - 60

EP - 67

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

A2 - Stewart, Daryl

A2 - Weissenbacher, Georg

PB - FMCAD Inc

T2 - Formal Methods in Computer-Aided Design (FMCAD)

Y2 - 2 October 2017 through 6 October 2017

ER -

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

Abstract

Conference

Access to Document

Other files and links

Fingerprint

C: Scalable Shared Memory: C3 Scalable Shared Memory via Consistency-directed Cache Coherence

Susmit Sarkar

Cite this

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

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Projects

C: Scalable Shared Memory: C3 Scalable Shared Memory via Consistency-directed Cache Coherence

Profiles

Susmit Sarkar

Cite this