Optimal Stateless Model Checking under the Release-Acquire Semantics

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson +1

We present a framework for the efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory…