Projects per year
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 |
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.Projects
- 1 Finished
-
C: Scalable Shared Memory: C3 Scalable Shared Memory via Consistency-directed Cache Coherence
Sarkar, S. (PI)
9/11/15 → 30/04/19
Project: Standard