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


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

School/Research organisations


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 languageEnglish
Title of host publicationProceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD)
ISBN (Electronic)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


ConferenceFormal Methods in Computer-Aided Design (FMCAD)
Abbreviated titleFMCAD
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. Sequential and parallel solution-biased search for subgraph algorithms

    Archibald, B., Dunlop, F., Hoffmann, R., McCreesh, C., Prosser, P. & Trimble, J., 2019, Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June 4–7, 2019, Proceedings. Rousseau, L-M. & Stergiou, K. (eds.). Cham: Springer, p. 20-38 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11494 LNCS).

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

  3. PatternClass Version 2.4.2: A permutation pattern class package (GAP package)

    Hoffmann, R., Linton, S. & Albert, M., 24 Jul 2018

    Research output: Non-textual formSoftware

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

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

ID: 250534181