[OOPSLA'25] Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice

Описание: Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice (Video, OOPSLA1 2025)
Jay Richards, Daniel Wright, Simon Cooksey, and Mark Batty
(University of Kent, UK; University of Surrey, UK; NVIDIA, UK; University of Kent, UK)

Abstract: We present the first thin-air free memory model that admits compiler optimisations that aggressively leverage knowledge from alias analysis, an assumption of freedom from undefined behaviour, and from the extrinsic choices of real implementations such as over-alignment. Our model has tooling support with state-of-the-art performance, executing a battery of tests orders of magnitude quicker than other executable thin-air free semantics. The model integrates with the C/C++ memory model through an exportable semantic dependency relation, it allows standard compilation mappings for atomics, and it matches all tests in the recently published desiderata for C/C++ from the ISO.

Article: https://doi.org/10.1145/3721089

ORCID: https://orcid.org/0009-0001-1738-3576, https://orcid.org/0000-0001-7404-2367, https://orcid.org/0000-0001-9365-9717, https://orcid.org/0000-0001-7053-4364

Video Tags: Thin-air problem, relaxed memory, C++, concurrent language semantics, oopslaa25main-p329-p, doi:10.1145/3721089, orcid:0009-0001-1738-3576, orcid:0000-0001-7404-2367, orcid:0000-0001-9365-9717, orcid:0000-0001-7053-4364

Presentation at the OOPSLA1 2025 conference, October 12–18, https://2025.splashcon.org/track/OOPSLA
Sponsored by ACM SIGPLAN,