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

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

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

8 Citations (Scopus)
15 Downloads (Pure)

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.

This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
Original languageEnglish
Title of host publicationProceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages (POPL 2017)
EditorsMatthew Fluet
Place of PublicationNew York
PublisherACM
Pages429-442
Number of pages14
ISBN (Print)9781450346603
DOIs
Publication statusPublished - 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

Publication series

NameACM SIGPLAN Notices
PublisherACM
Number1
Volume52
ISSN (Print)0362-1340
ISSN (Electronic)1558-1160

Conference

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

Keywords

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

Fingerprint

Dive into the research topics of 'Mixed-size concurrency: ARM, POWER, C/C++11, and SC'. Together they form a unique fingerprint.

Cite this