Promising 2.0: global optimizations in relaxed memory concurrency
- 11 June 2020
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
Abstract
For more than fifteen years, researchers have tried to support global optimizations in a usable semantics for a concurrent programming language, yet this task has been proven to be very difficult because of (1) the infamous “out of thin air” problem, and (2) the subtle interaction between global and thread-local optimizations. In this paper, we present a solution to this problem by redesigning a key component of the promising semantics (PS) of Kang et al. Our updated PS 2.0 model supports all the results known about the original PS model (i.e., thread-local optimizations, hardware mappings, DRF theorems), but additionally enables transformations based on global value-range analysis as well as register promotion (i.e., making accesses to a shared location local if the location is accessed by only one thread). PS 2.0 also resolves a problem with the compilation of relaxed RMWs to ARMv8, which required an unintended extra fence.Keywords
This publication has 13 references indexed in Scilit:
- A Formalization of Java's Concurrent Access ModesProceedings of the ACM on Programming Languages, 2019
- Bridging the gap between programming languages and hardware weak memory modelsProceedings of the ACM on Programming Languages, 2019
- Grounding thin-air reads with event structuresProceedings of the ACM on Programming Languages, 2019
- Evaluating Password Behavior at a Small UniversityJournal of Computer Science, 2019
- Repairing sequential consistency in C/C++11Published by Association for Computing Machinery (ACM) ,2017
- A promising semantics for relaxed-memory concurrencyPublished by Association for Computing Machinery (ACM) ,2017
- A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executionsPublished by Association for Computing Machinery (ACM) ,2016
- Library abstraction for C/C++ concurrencyPublished by Association for Computing Machinery (ACM) ,2013
- Mathematizing C++ concurrencyPublished by Association for Computing Machinery (ACM) ,2011
- The Java memory modelPublished by Association for Computing Machinery (ACM) ,2005