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.