Skip to content

Research at St Andrews

Memory consistency models using constraints

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

Abstract

Memory consistency models (MCMs) are at the heart of concurrent programming. They represent the behaviour of concurrent programs at the chip level. To test these models small program snippets called litmus test are generated, which show allowed or forbidden behaviour of different MCMs. This paper is showcasing the use of constraint programming to automate the generation and testing of litmus tests for memory consistency models. We produce a few exemplary case studies for two MCMs, namely Sequential Consistency and Total Store Order. These studies demonstrate the flexibility of constrains programming in this context and lay foundation to the direct verification of MCMs against the software facing cache coherence protocols.
Close

Details

Original languageEnglish
Title of host publicationThe Seventeenth Workshop on Constraint Modelling and Reformulation (ModRef 2018), Proceedings
Number of pages16
Publication statusPublished - 27 Aug 2018
Event24th International Conference on Principles and Practice of Constraint Programming (CP 2018) - Euratechnologies, Lille, France
Duration: 27 Aug 201831 Aug 2018
Conference number: 24
http://cp2018.a4cp.org/

Conference

Conference24th International Conference on Principles and Practice of Constraint Programming (CP 2018)
Abbreviated titleCP 2018
CountryFrance
CityLille
Period27/08/1831/08/18
Internet address

    Research areas

  • Memory consistency, Concurrent programming, Litmus tests, Constraints programming, Modelling

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

View graph of relations

Related by author

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

    Banks, C., Elver, M., Hoffmann, R., Sarkar, S., Jackson, P. & Nagarajan, V., 2 Oct 2017, Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD). ACM, p. 60-67

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

  2. Linking Scottish vital event records using family groups

    Akgün, Ö., Dearle, A., Kirby, G. N. C., Garrett, E., Dalton, T. S., Christen, P., Dibben, C. J. L. & Williamson, L. E. P., 25 Mar 2019, In : Historical Methods: a Journal of Quantitative and Interdisciplinary History. Latest articles, 17 p.

    Research output: Contribution to journalArticle

  3. Solving computational problems in the theory of word-representable graphs

    Akgün, Ö., Gent, I. P., Kitaev, S. & Zantema, H., 24 Feb 2019, In : Journal of Integer Sequences. 22, 2, 17 p., 19.2.5.

    Research output: Contribution to journalArticle

  4. How people visually represent discrete constraint problems

    Zhu, X., Nacenta, M., Akgün, Ö. & Nightingale, P. W., 24 Jan 2019, In : IEEE Transactions on Visualization and Computer Graphics. Early Access, p. 1-14 14 p.

    Research output: Contribution to journalArticle

  5. Cloud benchmarking for maximising performance of scientific applications

    Varghese, B., Akgun, O., Miguel, I. J., Thai, L. T. & Barker, A. D., 1 Jan 2019, In : IEEE Transactions on Cloud Computing. 7, 1, p. 170-182 13 p., 7553491.

    Research output: Contribution to journalArticle

ID: 255666320