Today’s mobile, desktop, and server processors are heterogeneous, consisting not only of CPU’s 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 support 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” consistency 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.
Wed 21 JunDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 11:00 | PLDI: Memory Models & Program LogicsPLDI Research Papers at Cypress 1 Chair(s): Matthew J. Parkinson Azure Research, Microsoft, UK | ||
09:00 20mTalk | Compound Memory Models PLDI Research Papers Andrés Goens the University of Edinburgh, Soham Chakraborty TU Delft, Susmit Sarkar University of St. Andrews, Sukarn Agarwal University of Edinburgh, Nicolai Oswald NVIDIA, Vijay Nagarajan University of Edinburgh, UK DOI | ||
09:20 20mTalk | Putting Weak Memory in Order via a Promising Intermediate Representation PLDI Research Papers Sung-Hwan Lee Seoul National University, Minki Cho Seoul National University, Roy Margalit Tel Aviv University, Israel, Chung-Kil Hur Seoul National University, Ori Lahav Tel Aviv University DOI | ||
09:40 20mTalk | Optimal Reads-From Consistency Checking for C11-Style Memory Models PLDI Research Papers Hünkar Can Tunç Aarhus University, Parosh Aziz Abdulla Uppsala University, Sweden, Soham Chakraborty TU Delft, Shankaranarayanan Krishna IIT Bombay, India, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University DOI Pre-print | ||
10:00 20mTalk | VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A PLDI Research Papers Zongyuan Liu Aarhus University, Sergei Stepanenko Aarhus University, Jean Pichon-Pharabod Aarhus University, Amin Timany Aarhus University, Aslan Askarov Aarhus University, Lars Birkedal Aarhus University DOI | ||
10:20 20mTalk | Embedding Hindsight Reasoning in Separation Logic PLDI Research Papers DOI | ||
10:40 20mTalk | Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic PLDI Research Papers Ike Mulder Radboud University Nijmegen, Lukasz Czajka Heliax AG, Robbert Krebbers Radboud University Nijmegen DOI Pre-print | ||
