SPLASH/ISSTA 2026 (series) / SPLASH 2026 (series) / OOPSLA /
RGSep under Release/Acquire Consistency
RGSep is a program logic for reasoning about the correctness of concurrent programs by combining separation logic and rely-guarantee reasoning. Although the logic was initially developed for sequential consistency, we show that in the absence of auxiliary variables, RGSep is also sound under the much weaker release-acquire (RA) consistency model, which is a well-behaved subset of the C++11 concurrency model. Our result provides another way to reason about RA programs, which is much simpler than using the state-of-the-art program logics that support weak memory consistency models.