Skip to content

Research at St Andrews

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

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

Author(s)

Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn Gray, Ali Sezgin, Mark Batty, Peter Sewell

School/Research organisations

Abstract

Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store. In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and(to some degree) exposed at the C/C++ language level. A semantic foundation for software therefore has to address them.We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff. This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting. In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency.We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses, and prove the standard compilation scheme from C11 atomics to POWER remains sound.This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
Close

Details

Original languageEnglish
Title of host publicationProceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages
PublisherACM
Pages429-442
DOIs
StatePublished - 1 Jan 2017
EventPOPL'17 44th ACM SIGPLAN Symposium on Principles of Programming Languages - Université Pierre et Marie Curie, Jussieu, Paris, France
Duration: 15 Jan 201721 Jan 2017
Conference number: 44
http://conf.researchr.org/home/POPL-2017

Conference

ConferencePOPL'17 44th ACM SIGPLAN Symposium on Principles of Programming Languages
Abbreviated titlePOPL
CountryFrance
CityParis
Period15/01/1721/01/17
Internet address

    Research areas

  • Relaxed Memory Models, Mixed-size, Semantics, ISA

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. Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms

    Castro, D., Hammond, K. & Sarkar, S. 4 Sep 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. New York: ACM, p. 4-17

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

ID: 246489959