RGSep is a program logic for reasoning about the correctness of concurrent programs that combines rely-guarantee reasoning and separation logic. Initially, RGSep was developed for Sequential Consistency, where we assume threads to be operating in an interleaving fashion. We show that RGSep is actually 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 a simpler way to reason about RA programs than the state-of-the-art program logics that support weak memory consistency models.
About Ellen Arlt
Ellen Arlt is a third-year PhD student at MPI-SWS Kaiserslautern, Germany advised by Viktor Vafeiadis. She is working on Weak Memory and Program Logics. Her paper “RGSep under Release/Acquire Consistency” has been published in PACMPL (OOPSLA 2026).