Memory Consistency and Program Transformations

TL;DR

The paper tackles the problem of safely applying compiler optimizations in the presence of memory-consistency models by formalizing optimizations as transformations on execution traces. It introduces pre-traces and candidate executions to conservatively approximate program behavior and decomposes optimizations into elementary transformation-effects that act on these traces. A central contribution is the Complete property, which guarantees that safety of transformations is preserved when moving from a base memory model to a weaker one, enabling portable optimizations across models. The authors demonstrate practicality by deriving SC_{RR} from SC and proving its Complete status for a broad class of transformation-effects, and they discuss extending the framework to include rmw and fences, as well as addressing write-elimination. The approach provides a principled methodology for memory-model design centered on the optimizations programmers want to perform, with potential implications for language and compiler ecosystems.

Abstract

A memory consistency model specifies the allowed behaviors of shared memory concurrent programs. At the language level, these models are known to have a non-trivial impact on the safety of program optimizations, limiting the ability to rearrange/refactor code without introducing new behaviors. Existing programming language memory models try to address this by permitting more (relaxed/weak) concurrent behaviors but are still unable to allow all the desired optimizations. A core problem is that weaker consistency models may also render optimizations unsafe, a conclusion that goes against the intuition of them allowing more behaviors. This exposes an open problem of the compositional interaction between memory consistency semantics and optimizations: which parts of the semantics correspond to allowing/disallowing which set of optimizations is unclear. In this work, we establish a formal foundation suitable enough to understand this compositional nature, decomposing optimizations into a finite set of elementary effects on program execution traces, over which aspects of safety can be assessed. We use this decomposition to identify a desirable compositional property (complete) that would guarantee the safety of optimizations from one memory model to another. We showcase its practicality by proving such a property between Sequential Consistency (SC) and $SC_{RR}$, the latter allowing independent read-read reordering over $SC$. Our work potentially paves way to a new design methodology of programming-language memory models, one that places emphasis on the optimizations desired to be performed.

Figures (27)

• Figure 1: Code motion equivalent to performing two adjacent memory access reordering (effect 1 followed by effect 2).
• Figure 2: Code motion equivalent to reordering (effect 1) and introduction (effect 2) for two different execution traces.
• Figure 3: The store buffering (SB) litmus test showcasing an allowed (green box) and forbidden (red box) outcome under SC.
• Figure 4: Different optimizations routinely performed by compilers today.
• Figure 5: The forbidden outcome $a=0 \ \wedge \ b=0$ permitted under SC after constant propagation, setting $b=0$.

Theorems & Definitions (58)

• Remark 1
• definition 1
• definition 2
• Remark 2
• definition 3
• definition 4
• Remark 3
• definition 5
• definition 6
• Remark 4