Wed 21 Jun 2023 09:20 - 09:40 at Cypress 1 - PLDI: Memory Models & Program Logics Chair(s): Matthew J. Parkinson

We investigate the problem of developing an “in-order” shared-memory concurrency model for languages like C and C++, which executes instructions following their program order, and is thus more amenable to reasoning and verification compared to recent complex proposals with out-of-order execution. We demonstrate that it is possible to fully support non-atomic accesses in an in-order model in a way that validates all compiler optimizations that are performed in single-threaded code (including irrelevant load introduction). The key to doing so is to utilize the distinction between a source model (with catch-fire semantics) and an intermediate representation (IR) model (with undefined value for racy reads) and formally establish the soundness of mapping from source to IR. As for relaxed atomic accesses, an in-order model must forbid load-store reordering. We discuss the rather limited performance impact of this fact and present a pragmatic approach to this problem, which, in the long term, requires a new kind of hardware store instructions for implementing relaxed stores. The source and IR semantics proposed in this paper are based on recent versions of the promising semantics, and the correctness proofs of the mappings from the source to the IR and from the IR to Armv8 are mechanized in Coq. This work is the first to formally relate an in-order source model and an out-of-order IR model with the goal of having an in-order source semantics without any performance overhead for non-atomics.

Wed 21 Jun

Displayed 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

#pldi-wed-0900-memory-cypress Discord icon small YouTube icon small

09:00
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
Embedding Hindsight Reasoning in Separation Logic
PLDI Research Papers
Roland Meyer TU Braunschweig, Thomas Wies New York University, Sebastian Wolff New York University
DOI
10:40
20m
Talk
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