Skip to content

Research at St Andrews

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

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

Author(s)

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

School/Research organisations

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

Details

Original languageEnglish
Title of host publicationProceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD)
PublisherACM
Pages60-67
ISBN (Electronic)9780983567875
StatePublished - 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
CountryAustria
CityVienna
Period2/10/176/10/17
Internet address

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Memory consistency models using constraints

    Akgün, Ö., Hoffmann, R. & Sarkar, S. 27 Aug 2018 The Seventeenth Workshop on Constraint Modelling and Reformulation (ModRef 2018), Proceedings. 16 p.

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

  2. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  3. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

    Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S. & Sewell, P. Jan 2018 Proceedings of the ACM on Programming Languages (POPL '18). New York: ACM, Vol. 2 Issue POPL, 29 p. 19

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

  4. Observations from parallelising three maximum common (Connected) subgraph algorithms

    Hoffmann, R., McCreesh, C., Ndiaye, S. N., Prosser, P., Reilly, C., Solnon, C. & Trimble, J. 2018 Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 15th International Conference, CPAIOR 2018, Delft, The Netherlands, June 26–29, 2018, Proceedings. van Hoeve, W-J. (ed.). Cham: Springer, p. 298-315 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10848)

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

  5. Strategy synthesis for autonomous agents using PRISM

    Giaquinta, R., Hoffmann, R., Ireland, M., Miller, A. & Norman, G. 2018 NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. Dutle, A., Muñoz, C. & Narkawicz, A. (eds.). Cham: Springer, p. 220-236 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10811)

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

ID: 250534181