Compound Memory Models

Journal Article (2023)
Author(s)

Andrés Goens (The University of Edinburgh)

Soham Chakraborty (TU Delft - Programming Languages)

Susmit Sarkar (University of St Andrews)

Sukarn Agarwal (The University of Edinburgh)

Nicolai Oswald (Nvidia Corporation)

Vijay Nagarajan (The University of Edinburgh)

Research Group
Programming Languages
Copyright
© 2023 Andrés Goens, S.S. Chakraborty, Susmit Sarkar, Sukarn Agarwal, Nicolai Oswald, Vijay Nagarajan
DOI related publication
https://doi.org/10.1145/3591267
More Info
expand_more
Publication Year
2023
Language
English
Copyright
© 2023 Andrés Goens, S.S. Chakraborty, Susmit Sarkar, Sukarn Agarwal, Nicolai Oswald, Vijay Nagarajan
Research Group
Programming Languages
Volume number
7
Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

Today's mobile, desktop, and server processors are heterogeneous, consisting not only of CPUs but also GPUs and other accelerators. Such heterogeneous processors are starting to expose a shared memory interface across these devices.Given that each of these individual devices typically supports a distinct instruction set architecture and a distinct memory consistency model, it is not clear what the memory consistency model of the heterogeneous machine should be. In this paper, we answer this question by formalizing "compound"memory models: we present a compositional operational model describing the resulting model when devices with distinct consistency models are fused together. We instantiate our model with the compound x86TSO/PTX model-a CPU enforcing x86TSO and a GPU enforcing the PTX model. A key result is that the x86TSO/PTX compound model retains compiler mappings from the language-based (scoped) C memory model. This means that threads mapped to the x86TSO device can continue to use the already proven C-To-x86TSO compiler mapping, and the same for PTX.