Skip to content

Research at St Andrews

Fences in weak memory models (extended version)

Research output: Contribution to journalArticle

Author(s)

Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell

School/Research organisations

Abstract

We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and by the visibility of inter- and intra-processor communications through memory (e.g. store atomicity relaxation). We prove results on the required behaviour and placement of memory fences to restore a given model (such as Sequential Consistency) from a weaker one. Based on this class of models we develop a tool, diy, that systematically and automatically generates and runs litmus tests. These tests can be used to explore the behaviour of processor implementations and the behaviour of models, and hence to compare the two against each other. We detail the results of experiments on Power and a model we base on them.

Close

Details

Original languageEnglish
Pages (from-to)170-205
Number of pages36
JournalFormal methods in system design
Volume40
Issue number2
DOIs
StatePublished - Apr 2012

    Research areas

  • Generic framework, Formal proofs, Testing tool, PowerPC, Weak memory models, Fences

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

  5. Mixed-size Concurrency: ARM, POWER, C/C++11, and SC

    Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K., Sezgin, A., Batty, M. & Sewell, P. 1 Jan 2017 Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages. ACM, p. 429-442

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

ID: 44376371