Memory Consistency and Program Transformations
<|reference_start|>Memory Consistency and Program Transformations: 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.<|reference_end|>
@article{gopalakrishnan2024memory,
    title={Memory Consistency and Program Transformations},
    author={Akshay Gopalakrishnan (1), Clark Verbrugge (1), Mark Batty (2) ((1)
  McGill University, (2) University of Kent)},
    journal={arXiv preprint arXiv:2409.12013},
    year={2024},
    archivePrefix={arXiv},
    eprint={2409.12013},
    primaryClass={cs.PL}
}