SPLASH 2026
Sat 3 - Fri 9 October 2026 Oakland, California, United States
co-located with SPLASH/ISSTA 2026

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.