Memory Consistency and Program Transformations

TL;DR

This paper develops a formal framework to analyze how different memory consistency models affect the safety of program optimizations, aiming to guide the design of memory models that support safe, desired optimizations.

Contribution

It introduces a decomposition of optimizations into elementary effects and establishes a formal property to compare memory models for safe optimization transfer.

Findings

Proves a compositional property between Sequential Consistency and SC_{RR}.

Provides a foundation for designing memory models supporting safe optimizations.

Highlights the importance of formal methods in understanding memory semantics.

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.