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

doi:10.1145/3009837.3009839

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

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

17 Citations (Scopus)

18 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 language	English
Title of host publication	Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages (POPL 2017)
Editors	Matthew Fluet
Place of Publication	New York
Publisher	ACM
Pages	429-442
Number of pages	14
ISBN (Print)	9781450346603
DOIs	https://doi.org/10.1145/3009837.3009839
Publication status	Published - 1 Jan 2017
Event	POPL'17 44th ACM SIGPLAN Symposium on Principles of Programming Languages - Université Pierre et Marie Curie, Jussieu, Paris, France Duration: 15 Jan 2017 → 21 Jan 2017 Conference number: 44 http://conf.researchr.org/home/POPL-2017

Publication series

Name	ACM SIGPLAN Notices
Publisher	ACM
Number	1
Volume	52
ISSN (Print)	0362-1340
ISSN (Electronic)	1558-1160

Conference

Conference	POPL'17 44th ACM SIGPLAN Symposium on Principles of Programming Languages
Abbreviated title	POPL
Country/Territory	France
City	Paris
Period	15/01/17 → 21/01/17
Internet address	http://conf.researchr.org/home/POPL-2017

Keywords

Relaxed Memory Models
Mixed-size
Semantics
ISA

Access to Document

10.1145/3009837.3009839

Flur_2016_Mixed-size-POPL17_AAM
Copyright © 2016, the Author(s). This work has been made available online in accordance with the publisher’s policies. This is the author created, accepted version manuscript following peer review and may differ slightly from the final published version. The final published version of this work is available at https://doi.org/10.1145/3009837.3009839
Accepted author manuscript, 327 KB

Susmit Sarkar
- Susmit.Sarkarst-andrews.acuk
- School of Computer Science - Professor, Director of Research
Person: Academic

Cite this

Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K., Sezgin, A., Batty, M., & Sewell, P. (2017). Mixed-size concurrency: ARM, POWER, C/C++11, and SC. In M. Fluet (Ed.), Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages (POPL 2017) (pp. 429-442). (ACM SIGPLAN Notices; Vol. 52, No. 1). ACM. https://doi.org/10.1145/3009837.3009839

@inproceedings{5cf34b09afc34c1c81dd6cd0e11694ad,

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

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

keywords = "Relaxed Memory Models, Mixed-size, Semantics, ISA",

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

note = "This work was partly funded by the EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems, EP/K008528/1, EPSRC grant C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence EP/M027317/1 (Sarkar), an ARM iCASE award (Pulte), a Gates Cambridge Scholarship (Nienhuis). and ANR grant WMC (ANR-11-JS02-011, Maranget).; POPL'17 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL ; Conference date: 15-01-2017 Through 21-01-2017",

year = "2017",

month = jan,

day = "1",

doi = "10.1145/3009837.3009839",

language = "English",

isbn = "9781450346603",

series = "ACM SIGPLAN Notices",

publisher = "ACM",

number = "1",

pages = "429--442",

editor = "Matthew Fluet",

booktitle = "Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages (POPL 2017)",

address = "United States",

url = "http://conf.researchr.org/home/POPL-2017",

}

Flur, S, Sarkar, S, Pulte, C, Nienhuis, K, Maranget, L, Gray, K, Sezgin, A, Batty, M & Sewell, P 2017, Mixed-size concurrency: ARM, POWER, C/C++11, and SC. in M Fluet (ed.), Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages (POPL 2017). ACM SIGPLAN Notices, no. 1, vol. 52, ACM, New York, pp. 429-442, POPL'17 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Paris, France, 15/01/17. https://doi.org/10.1145/3009837.3009839

Mixed-size concurrency: ARM, POWER, C/C++11, and SC. / Flur, Shaked; Sarkar, Susmit; Pulte, Christopher et al.
Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages (POPL 2017). ed. / Matthew Fluet. New York: ACM, 2017. p. 429-442 (ACM SIGPLAN Notices; Vol. 52, No. 1).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Mixed-size concurrency

T2 - POPL'17 44th ACM SIGPLAN Symposium on Principles of Programming Languages

AU - Flur, Shaked

AU - Sarkar, Susmit

AU - Pulte, Christopher

AU - Nienhuis, Kyndylan

AU - Maranget, Luc

AU - Gray, Kathryn

AU - Sezgin, Ali

AU - Batty, Mark

AU - Sewell, Peter

N1 - Conference code: 44

PY - 2017/1/1

Y1 - 2017/1/1

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

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

KW - Relaxed Memory Models

KW - Mixed-size

KW - Semantics

KW - ISA

U2 - 10.1145/3009837.3009839

DO - 10.1145/3009837.3009839

M3 - Conference contribution

SN - 9781450346603

T3 - ACM SIGPLAN Notices

SP - 429

EP - 442

BT - Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages (POPL 2017)

A2 - Fluet, Matthew

PB - ACM

CY - New York

Y2 - 15 January 2017 through 21 January 2017

ER -

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Profiles

Susmit Sarkar

Cite this